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
> On 10 Jun 2019, at 18:18, 'Marko Schuetz-Schmuck' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> 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 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 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.
--
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/24FBF48E-45AE-4391-9258-55A39E0A7DEC%40gmail.com.
For more options, visit https://groups.google.com/d/optout.