Illustrating fairness in TLA

Fair.cfg

SPECIFICATION Spec

INVARIANT TypeInv
PROPERTY EventuallyC

Fair.tla

---- MODULE Fair ----

VARIABLE st

A == 1
B == 2
C == 3

TypeInv == st \in {A, B, C}

Init == st = A

AB == st = A /\ st' = B
BA == st = B /\ st' = A
AC == st = A /\ st' = C
CC == st = C /\ st' = C

(* You need WF on BA to make sure we don't just stutter forever in B (SF is
sufficient but unnecessary). You need SF on AC because it is infinitely often
disabled (because AB can preempt it) to assert you must eventually go to C. *)
Spec == Init /\ [][AB \/ BA \/ AC \/ CC]_st /\ WF_st(BA) /\ SF_st(AC)

EventuallyC == <>(st = C)

=====================