you are not showing us the full specification. A TLA+ specifications of the form
Init /\ [Next]_v
allows for infinite stuttering. Adding fairness conditions WF_v(A) or SF_v(A) enforces action <<A>>_v to occur infinitely often if it is "often enough" enabled and therefore in particular rules out infinite stuttering in those cases. But infinite stuttering is still possible when A is disabled at the state where stuttering occurs.
The absence of deadlocks does not rule out infinite stuttering. For example, consider the specification
Init == x=0
Inc == x<5 /\ x'=x+1
Reset == x=5 /\ x'=0
Spec == Init /\ [Inc \/ Reset]_x /\ WF_x(Inc)
The spec has no deadlock, since at least one action is possible at any reachable state. However, it fails to satisfy the property
because there is a behavior that stutters infinitely at the state where x=5: since Inc is disabled at that state, the fairness property is trivially satisfied.
More to the point, your next-state relation contains a disjunct that prevents deadlock (as indicated by the comment), but it may very well allow for infinite stuttering.
Hope this helps,
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.