Section 6.4 "Specifying Alternation: Liveness" in main.pdf of the TLA+ Hyperbook says:
Beginning the algorithm with --fair algorithm adds the fairness requirement WFvar(Next), which asserts:
3. The behavior does not end in a state sn if there exists a state sn+1 such
that the sequence s1 → ... → sn+1 also satisfies condition 2.
(Where condition 2 is "Each step si → si+1 of the behavior is a Next step
What does it mean for a behavior to "end"?
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...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at https://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout