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

[Shiyao MA <i@xxxxxxxxx>]

Hi Johan,

I have trimmed down your file into the following MVCE.

---------------------------- MODULE WorkspaceLock ---------------------------
EXTENDS Integers
VARIABLES locks
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
operator.

Channel is the module from Specifying Systems.

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

Best regards,

Marko

-- 
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.