[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

What does it mean for a behavior to "end"?



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"?