On Saturday, February 4, 2017 at 9:34:37 AM UTC-5, Stephan Merz wrote:
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.
OK, a behavior is a sequence of states, and for a behavior to "end" means that all future states in the behavior's sequence are the same state. (Ignoring stuttering which comes later). Thanks!
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.
What does it means for a state such as
sn+1 to "exist"?