[tlaplus] TLC reports that "temporal properties were violated" even though the algorithm was declared fair

--------------------------- MODULE DieHarderBook ---------------------------

EXTENDS Integers, GCD

Min(n,m) == IF n < m THEN n ELSE m

CONSTANTS Goal, Jugs, Capacity

ASSUME CONSTANTS_OK == /\ Goal \in Nat
/\ Capacity \in [Jugs -> Nat \ {0}]

(***************************************************************************
--fair algorithm DieHarder {
variable injug = [j \in Jugs |-> 0] ;
{ while (~\E j \in Jugs : injug[j] = Goal)
{ either with (j \in Jugs) \* fill jug j
{ injug[j] := Capacity[j] }
or with (j \in Jugs) \* empty jug j
{ injug[j] := 0 }
or with (j \in Jugs, k \in Jugs \ {j}) \* pour from jug j to jug k
{ with ( poured =
Min(injug[j] + injug[k], Capacity[k]) - injug[k] )
{ injug[j] := injug[j] - poured ||
injug[k] := injug[k] + poured
}
}
}
}
}
***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "b157a2cd" /\ chksum(tla) = "88d18fa9")
VARIABLES injug, pc

vars == << injug, pc >>

Init == (* Global variables *)
/\ injug = [j \in Jugs |-> 0]
/\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
/\ IF ~\E j \in Jugs : injug[j] = Goal
THEN /\ \/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = Capacity[j]]
\/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
\/ /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
/\ pc' = "Lbl_1"
ELSE /\ pc' = "Done"
/\ UNCHANGED <<injug>>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1
\/ Terminating

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

Termination == <>(pc = "Done")

\* END TRANSLATION
=============================================================================