Weak vs. Strong Fairness

An action that's enabled, but never continuously

Picture a network link that flips between up and down forever, on its own, and a sender that can only deliver a message while the link is up:

VARIABLES link, sent

Toggle == link' = (IF link = "up" THEN "down" ELSE "up") /\ sent' = sent

Send == link = "up" /\ sent' = TRUE /\ link' = link

Next == Toggle \/ Send

Send is enabled sometimes — every other state, whenever link = "up" — but never continuously: right after it becomes enabled, Toggle is free to flip link back to "down" before Send gets a turn. Does weak fairness on Send guarantee the message eventually gets through?

Spec == Init /\ [][Next]_vars /\ WF_vars(Toggle) /\ WF_vars(Send)
Delivered == <>sent

(WF_vars(Toggle) is there just to keep the link actually flipping — without it, TLC could stutter forever at the very first state, which isn't the interesting failure here.) Run it, and Delivered is still violated:

State 1: link = "down", sent = FALSE
State 2: <Toggle> link = "up", sent = FALSE
Back to state 1: <Toggle>

TLC keeps toggling link up and down and never once chooses Send, even though Send is enabled at every other state. This is legal under WF_vars(Send) because weak fairness's promise only kicks in when an action is enabled continuously, forever, from some point on — and Send never is. Being enabled infinitely often isn't enough for WF.

Strong fairness: infinitely often is enough

SF_vars(A) is the stronger promise:

If A is enabled infinitely often (repeatedly, even if not continuously), A must eventually happen.

Swap WF_vars(Send) for SF_vars(Send) and re-run:

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

No violation. Send being enabled every other state is exactly "infinitely often," which is all SF needs.

When to reach for which

• WF_vars(A) — use it for an action that, once nothing else is blocking it, stays available until it runs. Most ordinary "keep doing your job" actions are like this (including IncX from the last chapter — nothing ever disables it once enabled).
• SF_vars(A) — use it for an action whose enabledness can be repeatedly taken away and given back by other actions in the spec (a flaky link, a lock that gets released and re-acquired, a retry after a timeout) — anywhere something else in the system can knock it out temporarily, but not forever.

Reaching for SF when WF would've done no harm — the stronger promise still holds whenever the weaker one would have. But WF where SF was actually needed produces exactly the bug you just saw: a property that looks true, and isn't.

What you'll do in this exercise

Write FlakySignal.tla — link and sent, Toggle and Send as above — with SF_vars(Send) (and WF_vars(Toggle) to keep the link moving), and check Delivered == <>sent.