|Your algorithm may fail to terminate due to stuttering: any TLA+ specification of the form|
Init /\ [Next]_vars
may take stuttering steps, even infinitely many. In order to rule out infinite stuttering, add a fairness assumption of the form
to the specification generated by the PlusCal translator. If you write "fair algorithm" instead of "algorithm", the PlusCal translator will generate that fairness condition for you.
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/D95FD7E0-3A3F-434B-A7E9-B960C2A39220%40gmail.com.