the corresponding TLA+ module is contained in the distribution of the TLA Proof System  and also available from  (with the temporal reasoning steps omitted because TLAPS didn't support them at the time). In short, the module has the definitions
vars == << flag, turn, pc >>
Spec == Init /\ [Next]_vars
This is the idiomatic form of TLA+ specifications: the next-state relation allows stuttering steps in which the variables declared in the specification do not change their values.
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/BE5C1A4C-BD12-4F3C-892A-EF1E902EA102%40gmail.com.