|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 counter-example. 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
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 non-trivial. See also chapter 8 of Specifying Systems.
Hope this helps,