|The basic form of a TLA+ specification is|
Init /\ [Next]_vars
and this allows for stuttering to occur at any state, even indefinitely, since [Next]_vars is shorthand for
Next \/ UNCHANGED vars
It may appear silly to allow stuttering steps to occur as long as you consider only one algorithm at a single level of abstraction but it turns out to be an essential concept for representing composition and refinement using conjunction and implication. The underlying philosophy is that a TLA+ specification describes an entire universe that contains the system that you are describing, and in that universe many events take place besides those that correspond to system steps.
The upshot is that you need to add fairness conditions if you want to ensure the system to make progress. For more information, please watch lecture 9 of the TLA+ video course.
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1EDD6030-F52F-464D-9459-EA1350C66F4F%40gmail.com.