Starting from TwoCounters, add weak fairness on IncX so that x
eventually reaches 2.
Requirements:
Spec == Init /\ [][Next]_vars /\ WF_vars(IncX).Live == <>(x = 2).model.cfg: SPECIFICATION Spec and PROPERTY Live.Fill in starter.tla where marked, then click Run Model Checker. TLC
should report no violations — IncX is always enabled (nothing about
IncY ever disables it), so weak fairness on IncX alone is enough to
guarantee x gets there.