Fairness

Ruling out "eventually just stop"

Last chapter's <>(x = 2) failed because [][Next]_vars always permits stuttering forever. Fairness is the missing piece: a temporal condition you conjoin onto Spec that rules out certain kinds of "give up." The simplest form is weak fairness, written WF_vars(A) for an action A:

If A is continuously enabled from some point on, A must eventually happen.

Read WF_vars(Next) and it sounds like exactly what's missing — surely if some Next step is always available, one must eventually be taken? Add it and try again:

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

TLC still reports <>(x = 2) violated — but the counterexample has changed shape. No more stuttering:

State 1: x=0, y=0
State 2: <IncX> x=1, y=0
State 3: <IncY> x=1, y=1
State 4: <IncY> x=1, y=2
State 5: <IncY> x=1, y=0
State 6: <IncY> x=1, y=1
Back to state 4

x gets to 1 once and then TLC runs IncY forever. This is now a legal behavior even under WF_vars(Next), because Next — the disjunction IncX \/ IncY — never stops being enabled: IncY alone keeps it continuously true. WF_vars(Next) only promises "some disjunct of Next keeps firing," and it's satisfied without IncX ever being the one chosen.

Fairness belongs on the sub-action, not the disjunction

To force IncX specifically, assert fairness on IncX specifically:

Spec == Init /\ [][Next]_vars /\ WF_vars(IncX)

Now IncX is continuously enabled the entire time (nothing about IncY ever disables it — it doesn't touch x), so WF_vars(IncX) forces it to happen, and <>(x = 2) holds. TLC confirms it with no counterexample.

This is the general rule: name the specific action you need progress from, and assert fairness on that name, not on a larger disjunction it happens to be part of. A Next built from several named actions typically needs its own WF_vars(...) conjunct per action you're making a liveness claim about — you don't get progress "for free" from any of them just because Next as a whole keeps moving.

What you'll do in this exercise

Take TwoCounters and add WF_vars(IncX) to Spec, then check Live == <>(x = 2) as a PROPERTY. This is the first exercise in the course where a liveness claim actually holds.