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

Re: [tlaplus] What does it mean for a behavior to "end"?

In TLA+, finite behaviors are represented by infinite stuttering from the final state. See also section 6.3, which says, "the only behaviors of this algorithm are the infinite behavior ... *and any finite prefix of it*". So a behavior ending in a state s_n formally means that it loops indefinitely at that state.


On 4 Feb 2017, at 15:19, Andrew Wilcox <andrew...@xxxxxxxxx> wrote:

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.