I copied the bakery algorithm from the book. When I added a check for StarvationFree, I indeed got "Temporal properties were violated.". But when I added a state contraint as in the book, the same happened.
When I played with the numbers (e.g. define Int as 1..10, but constrain
) the error trace stopped with num = <0,0,6>, not with any higher number.
--------------------------- MODULE bakery ---------------------------
EXTENDS Integers
CONSTANT N
ASSUME N \in Nat
Procs == 1..N
a \prec b == \/ a[1] < b[1]
\/ (a[1] = b[1]) /\ (a[2] < b[2])
(*
--fair algorithm BigStepBakery
{ variable num = [i \in Procs |-> 0] ;
process (pr \in Procs)
variable unchecked = {} ;
{ ncs:- while (TRUE)
{ enter: with (i \in { j \in Nat : \A q \in Procs : j > num[q] })
{ num[self] := i } ;
unchecked := Procs \ {self} ;
wait: while (unchecked # {})
{ with (i \in unchecked)
{ await \/ num[i] = 0
\/ <<num[self], self>> \prec <<num[i], i>> ;
unchecked := unchecked \ {i}
}
} ;
cs: skip ; \* critical section
exit: num[self] := 0
}
}
} *)
\* BEGIN TRANSLATION
VARIABLES num, pc, unchecked
vars == << num, pc, unchecked >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ num = [i \in Procs |-> 0]
(* Process pr *)
/\ unchecked = [self \in Procs |-> {}]
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << num, unchecked >>
enter(self) == /\ pc[self] = "enter"
/\ \E i \in { j \in Nat : \A q \in Procs : j > num[q] }:
num' = [num EXCEPT ![self] = i]
/\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}]
/\ pc' = [pc EXCEPT ![self] = "wait"]
wait(self) == /\ pc[self] = "wait"
/\ IF unchecked[self] # {}
THEN /\ \E i \in unchecked[self]:
/\ \/ num[i] = 0
\/ <<num[self], self>> \prec <<num[i], i>>
/\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}]
/\ pc' = [pc EXCEPT ![self] = "wait"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ UNCHANGED unchecked
/\ num' = num
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ UNCHANGED << num, unchecked >>
exit(self) == /\ pc[self] = "exit"
/\ num' = [num EXCEPT ![self] = 0]
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ UNCHANGED unchecked
pr(self) == ncs(self) \/ enter(self) \/ wait(self) \/ cs(self)
\/ exit(self)
Next == (\E self \in Procs: pr(self))
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
\* END TRANSLATION
-----------------------------------------------------------------------------
TypeOK == /\ num \in [Procs -> Nat]
/\ unchecked \in [Procs -> SUBSET Procs]
/\ pc \in [Procs -> {"ncs", "enter", "wait", "cs", "exit"}]
MutualExclusion ==
\A p, q \in Procs : (p # q) => ~((pc[p] = "cs") /\ (pc[q] = "cs"))
\* liveness stuff below
Trying(p) == pc[p] \in {"enter", "wait"}
InCS(p) == pc[p] = "cs"
DeadlockFree == (\E p \in Procs : Trying(p)) ~> (\E p \in Procs : InCS(p))
StarvationFree == \A p \in Procs : Trying(p) ~> InCS(p)
=============================================================================
=============================================================================
\* Modification History
\* Last modified Sun Apr 06 15:06:48 PDT 2014 by Gideon
\* Created Sun Apr 06 13:55:30 PDT 2014 by Gideon