[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: TLC reports error (undefined identifier), but it's defined...

Hi Johan,

I have trimmed down your file into the following MVCE.
---------------------------- MODULE WorkspaceLock ---------------------------
EXTENDS Integers
Init == /\ locks = 0
Tick == /\ locks' = 1
Next == CHOOSE n \in 1..3: Tick
\* Next == Tick \* this works
Spec == Init /\ [][Next]_<<locks>>


So it seems to me, within the context of CHOOSE, we cannot assign new state value to a variable.

I didn't find backup words in =specifying systems= though.

On Sunday, 2 February 2020 01:03:27 UTC+8, Johan Persson wrote:
I have a similar issue with a simple specification for an exclusive workspace lock:

In evaluation, the identifier locks is either undefined or not an operator.
line 20, col 12 to line 20, col 16 of module WorkspaceLock

I cannot for the life of me figure out what is incorrect. Anyone got any ideas?

/ Johan

On Monday, June 10, 2019 at 6:18:13 PM UTC+2, Marko Schuetz-Schmuck wrote:
Dear All,

I'm trying to use TLC, but I'm getting the error:

In evaluation, the identifier chan is either undefined or not an

Channel is the module from Specifying Systems.

I don't see what's wrong with my specs. Any hints?

Best regards,


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/95d2813a-510c-4aec-9ede-c27c2cd41eb1%40googlegroups.com.