Your specification has the form Init /\ [][Next]_vars This formula allows for stuttering, i.e. transitions satisfying vars' = vars, and this is exactly what happens in the counterexample. In order to ensure progress (when this is possible) you should add a suitable fairness condition to your specification. In your case, the specification Init /\ [][Next]_vars /\ WF_vars(Next) should be enough. From PlusCal, you can replace algorithm ... by fair algorithm in order to make the PlusCal translator generate the fairness condition for you. In general, determining which fairness conditions are "reasonable" depends on the system that you intend to model and can be nontrivial. See also chapter 8 of Specifying Systems. Hope this helps, Stephan
