------------ MODULE Bakery ---------------------------- EXTENDS Naturals (***************************************************************************) (* We first declare N to be the number of processes, and we assume that N *) (* is a natural number. *) (***************************************************************************) CONSTANT N ASSUME N \in Nat (***************************************************************************) (* We define Procs to be the set {1, 2, ... , N} of processes. *) (***************************************************************************) Procs == 1..N (***************************************************************************) (* \prec is defined to be the lexicographical less-than relation on pairs *) (* of numbers. *) (***************************************************************************) a \prec b == \/ a[1] < b[1] \/ (a[1] = b[1]) /\ (a[2] < b[2]) VARIABLES num, flag, pc, unchecked, max, nxt vars == << num, flag, pc, unchecked, max, nxt >> ProcSet == (Procs) Init == (* Global variables *) /\ num = [i \in Procs |-> 0] /\ flag = [i \in Procs |-> FALSE] (* Process p *) /\ unchecked = [self \in Procs |-> {}] /\ max = [self \in Procs |-> 0] /\ nxt = [self \in Procs |-> 1] /\ pc = [self \in ProcSet |-> "ncs"] ncs(self) == /\ pc[self] = "ncs" /\ pc' = [pc EXCEPT ![self] = "e1"] /\ UNCHANGED << num, flag, unchecked, max, nxt >> e1(self) == /\ pc[self] = "e1" /\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] /\ pc' = [pc EXCEPT ![self] = "e1"] /\ UNCHANGED <> \/ /\ flag' = [flag EXCEPT ![self] = TRUE] /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] /\ max' = [max EXCEPT ![self] = 0] /\ pc' = [pc EXCEPT ![self] = "e2"] /\ UNCHANGED << num, nxt >> e2(self) == /\ pc[self] = "e2" /\ IF unchecked[self] # {} THEN /\ \E i \in unchecked[self]: /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}] /\ IF num[i] > max[self] THEN /\ max' = [max EXCEPT ![self] = num[i]] ELSE /\ TRUE /\ max' = max /\ pc' = [pc EXCEPT ![self] = "e2"] ELSE /\ pc' = [pc EXCEPT ![self] = "e3"] /\ UNCHANGED << unchecked, max >> /\ UNCHANGED << num, flag, nxt >> e3(self) == /\ pc[self] = "e3" /\ \/ /\ \E k \in Nat: num' = [num EXCEPT ![self] = k] /\ pc' = [pc EXCEPT ![self] = "e3"] \/ /\ \E i \in {j \in Nat : j > max[self]}: num' = [num EXCEPT ![self] = i] /\ pc' = [pc EXCEPT ![self] = "e4"] /\ UNCHANGED << flag, unchecked, max, nxt >> e4(self) == /\ pc[self] = "e4" /\ \/ /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] /\ pc' = [pc EXCEPT ![self] = "e4"] /\ UNCHANGED unchecked \/ /\ flag' = [flag EXCEPT ![self] = FALSE] /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] /\ pc' = [pc EXCEPT ![self] = "w1"] /\ UNCHANGED << num, max, nxt >> w1(self) == /\ pc[self] = "w1" /\ IF unchecked[self] # {} THEN /\ \E i \in unchecked[self]: nxt' = [nxt EXCEPT ![self] = i] /\ ~ flag[nxt'[self]] /\ pc' = [pc EXCEPT ![self] = "w2"] ELSE /\ pc' = [pc EXCEPT ![self] = "cs"] /\ nxt' = nxt /\ UNCHANGED << num, flag, unchecked, max >> w2(self) == /\ pc[self] = "w2" /\ \/ num[nxt[self]] = 0 \/ <> \prec <> /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {nxt[self]}] /\ pc' = [pc EXCEPT ![self] = "w1"] /\ UNCHANGED << num, flag, max, nxt >> cs(self) == /\ pc[self] = "cs" /\ TRUE /\ pc' = [pc EXCEPT ![self] = "exit"] /\ UNCHANGED << num, flag, unchecked, max, nxt >> exit(self) == /\ pc[self] = "exit" /\ \/ /\ \E k \in Nat: num' = [num EXCEPT ![self] = k] /\ pc' = [pc EXCEPT ![self] = "exit"] \/ /\ num' = [num EXCEPT ![self] = 0] /\ pc' = [pc EXCEPT ![self] = "ncs"] /\ UNCHANGED << flag, unchecked, max, nxt >> p(self) == ncs(self) \/ e1(self) \/ e2(self) \/ e3(self) \/ e4(self) \/ w1(self) \/ w2(self) \/ cs(self) \/ exit(self) Next == (\E self \in Procs: p(self)) Spec == /\ Init /\ [][Next]_vars /\ \A self \in Procs : WF_vars((pc[self] # "ncs") /\ p(self)) \* END TRANSLATION (this ends the translation of the PlusCal code) (***************************************************************************) (* MutualExclusion asserts that two distinct processes are in their *) (* critical sections. *) (***************************************************************************) MutualExclusion == \A i,j \in Procs : (i # j) => ~ /\ pc[i] = "cs" /\ pc[j] = "cs" ----------------------------------------------------------------------------- (***************************************************************************) (* The Inductive Invariant *) (* *) (* TypeOK is the type-correctness invariant. *) (***************************************************************************) TypeOK == /\ num \in [Procs -> Nat] /\ flag \in [Procs -> BOOLEAN] /\ unchecked \in [Procs -> SUBSET Procs] /\ max \in [Procs -> Nat] /\ nxt \in [Procs -> Procs] /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", "e4", "w1", "w2", "cs", "exit"}] (***************************************************************************) (* Before(i, j) is a condition that implies that num[i] > 0 and, if j is *) (* trying to enter its critical section and i does not change num[i], then *) (* j either has or will choose a value of num[j] for which *) (* *) (* <> \prec <> *) (* *) (* is true. *) (***************************************************************************) Before(i,j) == /\ num[i] > 0 /\ \/ pc[j] \in {"ncs", "e1", "exit"} \/ /\ pc[j] = "e2" /\ \/ i \in unchecked[j] \/ max[j] >= num[i] \/ /\ pc[j] = "e3" /\ max[j] >= num[i] \/ /\ pc[j] \in {"e4", "w1", "w2"} /\ <> \prec <> /\ (pc[j] \in {"w1", "w2"}) => (i \in unchecked[j]) (***************************************************************************) (* Inv is the complete inductive invariant. *) (***************************************************************************) Inv == /\ TypeOK /\ \A i \in Procs : \* /\ (pc[i] \in {"ncs", "e1", "e2"}) => (num[i] = 0) /\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0) /\ (pc[i] \in {"e2", "e3"}) => flag[i] /\ (pc[i] = "w2") => (nxt[i] # i) /\ pc[i] \in {(*"e2",*) "w1", "w2"} => i \notin unchecked[i] /\ (pc[i] \in {"w1", "w2"}) => \A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j) /\ /\ (pc[i] = "w2") /\ \/ (pc[nxt[i]] = "e2") /\ (i \notin unchecked[nxt[i]]) \/ pc[nxt[i]] = "e3" => max[nxt[i]] >= num[i] /\ (pc[i] = "cs") => \A j \in Procs \ {i} : Before(i, j) ----------------------------------------------------------------------------- ============================================================================= \* Modification History \* Last modified Mon Mar 02 19:53:36 IRST 2020 by AmirHossein \* Last modified Tue Aug 27 12:23:10 PDT 2019 by loki \* Last modified Fri May 25 11:18:47 CEST 2018 by merz \* Last modified Sat May 19 16:40:23 CEST 2018 by merz \* Last modified Thu May 17 07:02:45 PDT 2018 by lamport \* Created Thu Nov 21 15:54:32 PST 2013 by lamport