Jay answered your post, just a quick addition from my side:
In your running example (with a weak fairness condition on the Inc action), infinite stuttering is in fact only allowed at the state where x=5. In general, TLC is not guaranteed to find the shortest counter-example for temporal properties, but it finds a shortest counter-example when checking invariants.
Note that stuttering is in fact very explicit in the next-state relations used in TLA+ specifications: [Next]_v is shorthand for "Next \/ v'=v", and this disjunct is responsible for stuttering. It allows any step to happen that leaves the _expression_ v unchanged, and a little thought will convince you that v'=v is bound to hold if all the variables that appear in v (and perhaps more) remain unchanged.
(I think it's an error to restrict WF to a subset of variables, but someone more knowledgable can correct me.)
It is syntactically legal to write WF_e(A) for any _expression_ e (possibly different from the tuple of all variables) and any action A (even one that does not occur as a disjunct of the next-state relation), and sometimes it makes sense to write such fairness conditions. The problem with these is that they may result in specifications that are not "machine closed". Leslie recently pointed this out in his answer to another thread . Unless you know exactly what you are doing, it is better to restrict yourself to fairness conditions WF_v(A) where v is the same subscript as the one used in [Next]_v, and A is a disjunct of Next.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.