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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. 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.
Attachment:
signature.asc
Description: PGP signature
---------------------------- 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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
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.