TLC reports error (undefined identifier), but it's defined...

79 views
Skip to first unread message

Marko Schuetz-Schmuck

unread,
Jun 10, 2019, 12:18:13 PM6/10/19
to tlaplus
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

signature.asc
Test.tla
Synchronizer.tla

Stephan Merz

unread,
Jun 10, 2019, 12:36:54 PM6/10/19
to tla...@googlegroups.com
TLC evaluates expressions from left to right, and your initial condition includes TypeInvariant as the first conjunct. I presume that CH!TypeInvariant accesses the variable chan in a way that TLC cannot interpret as an initialization. I expect that the error disappears if you redefine

Init ==
/\ CH!Init
/\ SYNC!Init
/\ TypeInvariant

In fact, I imagine that you don't have to include the full TypeInvariant at all in the initial condition, but only the first three conjuncts that serve as initializations of the variables received, rVar, and sVar.

Stephan
> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/877e9t2z45.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
> For more options, visit https://groups.google.com/d/optout.
> ---------------------------- MODULE Test ----------------------------
> CONSTANT SomeValues
> VARIABLES received, chan, rVar, sVar, threadAWaiting, threadBWaiting
>
> vars == <<received, rVar, sVar, chan, threadAWaiting, threadBWaiting>>
>
> CH == INSTANCE Channel WITH Data <- SomeValues
> SYNC == INSTANCE Synchronizer
>
> TypeInvariant ==
> /\ received \in SomeValues
> /\ rVar \in SomeValues
> /\ sVar \in SomeValues
> /\ CH!TypeInvariant
>
> Init ==
> /\ TypeInvariant
> /\ CH!Init
> /\ SYNC!Init
>
> thread1Send ==
> \E d \in SomeValues: CH!Send(d)
>
> thread1Other ==
> /\ sVar' \in SomeValues
>
> thread1 == thread1Send \/ thread1Other
>
> thread2Receive ==
> CH!Rcv
>
> thread2Other ==
> /\ rVar' \in SomeValues
>
> thread2 == thread2Receive \/ thread2Other
>
> Next ==
> /\ \/ thread1
> \/ thread2
> /\ SYNC!SyncThreadActions(rVar, sVar, thread2Receive, thread1Send)
>
> Spec ==
> /\ Init
> /\ [][Next]_vars
> =============================================================================
> \* Modification History
> \* Last modified Mon Jun 10 12:04:10 AST 2019 by marko
> \* Created Mon Jun 10 10:41:14 AST 2019 by 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/877e9t2z45.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
> For more options, visit https://groups.google.com/d/optout.
> ---------------------------- MODULE Synchronizer ----------------------------
> VARIABLES threadAWaiting, threadBWaiting
>
> Init ==
> /\ threadAWaiting = FALSE
> /\ threadBWaiting = FALSE
>
> waitingForB(threadAVars) ==
> /\ threadAWaiting
> /\ UNCHANGED threadAVars
>
> waitingForA(threadBVars) ==
> /\ threadBWaiting
> /\ UNCHANGED threadBVars
>
> threadA(threadAAction) ==
> threadAAction =>
> /\ threadBWaiting => threadBWaiting' = FALSE
> /\ \neg threadBWaiting => threadAWaiting' = TRUE
>
> threadB(threadBAction) ==
> threadBAction =>
> /\ threadAWaiting => threadAWaiting' = FALSE
> /\ \neg threadAWaiting => threadBWaiting' = TRUE
>
> SyncThreadActions(threadAVars, threadBVars, threadAAction, threadBAction) ==
> \/ waitingForA(threadBVars)
> \/ waitingForB(threadAVars)
> \/ threadA(threadAAction)
> \/ threadB(threadBAction)
>
> =============================================================================
> \* Modification History
> \* Last modified Mon Jun 10 11:09:16 AST 2019 by marko
> \* Created Mon Jun 10 09:52:33 AST 2019 by 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/877e9t2z45.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
> For more options, visit https://groups.google.com/d/optout.

Marko Schütz-Schmuck

unread,
Jun 12, 2019, 8:01:12 AM6/12/19
to tlaplus
Thanks! That helped.

Johan Persson

unread,
Feb 1, 2020, 12:03:27 PM2/1/20
to tlaplus
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
WorkspaceLock.tla

Shiyao MA

unread,
Feb 1, 2020, 8:07:13 PM2/1/20
to tlaplus
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.

Leslie Lamport

unread,
Feb 1, 2020, 8:35:36 PM2/1/20
to tlaplus
Please look up CHOOSE and see what 

    CHOOSE u \in Users : ...  

means.  Then look up \E and see what 

    \E u \in Users : ...

means.

Johan Persson

unread,
Feb 2, 2020, 4:05:22 PM2/2/20
to tlaplus
Thanks, I see that my first attempt was not math, but an thinly veiled instruction to what TLC ought to do.  I evidently have a lot of programmer quirks to iron out.
Another thing I realized was that my usage of helpers hid the fact that I tried to set the next state of locks twice per action.

The following rewrite works as intended:


OpenWorkspace(u, w) == /\ locks[w] <= 0
                       /\ openWorkspaces' = [openWorkspaces EXCEPT ![u] = openWorkspaces[u] \cup {w}]
                       /\ locks' = [c \in Workspaces |-> IF c = w THEN 10 ELSE locks[c] - 1]

EditWorkspace(u, w) == /\ locks[w] > 0
                       /\ w \in openWorkspaces[u]
                       /\ locks' = [c \in Workspaces |-> IF c = w THEN 10 ELSE locks[c] - 1]
                       /\ UNCHANGED openWorkspaces

CloseWorkspace(u, w) == /\ locks[w] > 0
                        /\ openWorkspaces' = [openWorkspaces EXCEPT ![u] = openWorkspaces[u] \cap {w}]
                        /\ locks' = [c \in Workspaces |-> IF c = w THEN 0 ELSE locks[c] - 1]

Next == \/ \E u \in Users, w \in Workspaces : OpenWorkspace(u, w)
        \/ \E u \in Users, w \in Workspaces : EditWorkspace(u, w)
        \/ \E u \in Users, w \in Workspaces : CloseWorkspace(u, w)


It's a silly and naïve specification, but I'm having a lot of fun playing around with it. :)

Reply all
Reply to author
Forward
0 new messages