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.

Regards,

Stephan

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.