diff --git a/specifications/Bakery-Boulangerie/Bakery.tla b/specifications/Bakery-Boulangerie/Bakery.tla index 0ae5e909..983bd7d2 100644 --- a/specifications/Bakery-Boulangerie/Bakery.tla +++ b/specifications/Bakery-Boulangerie/Bakery.tla @@ -1,282 +1,282 @@ ------------- MODULE Bakery ---------------------------- -(***************************************************************************) -(* The bakery algorithm originally appeared in: *) -(* *) -(* Leslie Lamport *) -(* A New Solution of Dijkstra's Concurrent Programming Problem *) -(* Communications of the ACM 17, 8 (August 1974), 453-455 *) -(* *) -(* The code for the algorithm given in that paper is : *) -(* `. *) -(* begin integer j; *) -(* L1: choosing [i] := 1 ; *) -(* number[i] := 1 + maximum (number[1],..., number[N]); *) -(* choosing[i] := 0; *) -(* for j = 1 step l until N do *) -(* begin *) -(* L2: if choosing[j] /= 0 then goto L2; *) -(* L3: if number[j] /= 0 and (number [j], j) < (number[i],i) *) -(* then goto L3; *) -(* end; *) -(* critical section; *) -(* number[i] := O; *) -(* noncritical section; *) -(* goto L1 ; *) -(* end .' *) -(* *) -(* This PlusCal version of the Atomic Bakery algorithm is one in which *) -(* variables whose initial values are not used are initialized to *) -(* particular type-correct values. If the variables were left *) -(* uninitialized, the PlusCal translation would initialize them to a *) -(* particular unspecified value. This would complicate the proof because *) -(* it would make the type-correctness invariant more complicated, but it *) -(* would be efficient to model check. We could write a version that is *) -(* more elegant and easy to prove, but less efficient to model check, by *) -(* initializing the variables to arbitrarily chosen type-correct values. *) -(***************************************************************************) -EXTENDS Naturals, TLAPS - -(***************************************************************************) -(* 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]) - -(*** this is a comment containing the PlusCal code * - ---algorithm Bakery -{ variables num = [i \in Procs |-> 0], flag = [i \in Procs |-> FALSE]; - fair process (p \in Procs) - variables unchecked = {}, max = 0, nxt = 1 ; - { ncs:- while (TRUE) - { e1: either { flag[self] := ~ flag[self] ; - goto e1 } - or { flag[self] := TRUE; - unchecked := Procs \ {self} ; - max := 0 - } ; - e2: while (unchecked # {}) - { with (i \in unchecked) - { unchecked := unchecked \ {i}; - if (num[i] > max) { max := num[i] } - } - }; - e3: either { with (k \in Nat) { num[self] := k } ; - goto e3 } - or { with (i \in {j \in Nat : j > max}) - { num[self] := i } - } ; - e4: either { flag[self] := ~ flag[self] ; - goto e4 } - or { flag[self] := FALSE; - unchecked := Procs \ {self} - } ; - w1: while (unchecked # {}) - { with (i \in unchecked) { nxt := i }; - await ~ flag[nxt]; - w2: await \/ num[nxt] = 0 - \/ <> \prec <> ; - unchecked := unchecked \ {nxt}; - } ; - cs: skip ; \* the critical section; - exit: either { with (k \in Nat) { num[self] := k } ; - goto exit } - or { num[self] := 0 } - } - } -} - -*** this ends the comment containg the pluscal code **********) - -\* BEGIN TRANSLATION (this begins the translation of the PlusCal code) -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)) - /\ \A self \in Procs : WF_vars(/\ e1(self) \/ e3(self) \/ e4(self) \/ exit(self) - /\ (pc'[self] # pc[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) - ------------------------------------------------------------------------------ -(***************************************************************************) -(* Proof of Mutual Exclusion *) -(* *) -(* This is a standard invariance proof, where <1>2 asserts that any step *) -(* of the algorithm (including a stuttering step) starting in a state in *) -(* which Inv is true leaves Inv true. Step <1>4 follows easily from *) -(* <1>1-<1>3 by simple temporal reasoning, but TLAPS does not yet do any *) -(* temporal reasoning. *) -(***************************************************************************) -THEOREM Spec => []MutualExclusion -<1> USE N \in Nat DEFS Procs, TypeOK, Before, \prec, ProcSet -<1>1. Init => Inv - BY DEF Init, Inv -<1>2. Inv /\ [Next]_vars => Inv' +------------ MODULE Bakery ---------------------------- +(***************************************************************************) +(* The bakery algorithm originally appeared in: *) +(* *) +(* Leslie Lamport *) +(* A New Solution of Dijkstra's Concurrent Programming Problem *) +(* Communications of the ACM 17, 8 (August 1974), 453-455 *) +(* *) +(* The code for the algorithm given in that paper is : *) +(* `. *) +(* begin integer j; *) +(* L1: choosing [i] := 1 ; *) +(* number[i] := 1 + maximum (number[1],..., number[N]); *) +(* choosing[i] := 0; *) +(* for j = 1 step l until N do *) +(* begin *) +(* L2: if choosing[j] /= 0 then goto L2; *) +(* L3: if number[j] /= 0 and (number [j], j) < (number[i],i) *) +(* then goto L3; *) +(* end; *) +(* critical section; *) +(* number[i] := O; *) +(* noncritical section; *) +(* goto L1 ; *) +(* end .' *) +(* *) +(* This PlusCal version of the Atomic Bakery algorithm is one in which *) +(* variables whose initial values are not used are initialized to *) +(* particular type-correct values. If the variables were left *) +(* uninitialized, the PlusCal translation would initialize them to a *) +(* particular unspecified value. This would complicate the proof because *) +(* it would make the type-correctness invariant more complicated, but it *) +(* would be efficient to model check. We could write a version that is *) +(* more elegant and easy to prove, but less efficient to model check, by *) +(* initializing the variables to arbitrarily chosen type-correct values. *) +(***************************************************************************) +EXTENDS Naturals, TLAPS + +(***************************************************************************) +(* 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]) + +(*** this is a comment containing the PlusCal code * + +--algorithm Bakery +{ variables num = [i \in Procs |-> 0], flag = [i \in Procs |-> FALSE]; + fair process (p \in Procs) + variables unchecked = {}, max = 0, nxt = 1 ; + { ncs:- while (TRUE) + { e1: either { flag[self] := ~ flag[self] ; + goto e1 } + or { flag[self] := TRUE; + unchecked := Procs \ {self} ; + max := 0 + } ; + e2: while (unchecked # {}) + { with (i \in unchecked) + { unchecked := unchecked \ {i}; + if (num[i] > max) { max := num[i] } + } + }; + e3: either { with (k \in Nat) { num[self] := k } ; + goto e3 } + or { with (i \in {j \in Nat : j > max}) + { num[self] := i } + } ; + e4: either { flag[self] := ~ flag[self] ; + goto e4 } + or { flag[self] := FALSE; + unchecked := Procs \ {self} + } ; + w1: while (unchecked # {}) + { with (i \in unchecked) { nxt := i }; + await ~ flag[nxt]; + w2: await \/ num[nxt] = 0 + \/ <> \prec <> ; + unchecked := unchecked \ {nxt}; + } ; + cs: skip ; \* the critical section; + exit: either { with (k \in Nat) { num[self] := k } ; + goto exit } + or { num[self] := 0 } + } + } +} + + this ends the comment containing the PlusCal code +*************) + +\* BEGIN TRANSLATION (this begins the translation of the PlusCal code) +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) + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Proof of Mutual Exclusion *) +(* *) +(* This is a standard invariance proof, where <1>2 asserts that any step *) +(* of the algorithm (including a stuttering step) starting in a state in *) +(* which Inv is true leaves Inv true. Step <1>4 follows easily from *) +(* <1>1-<1>3 by simple temporal reasoning, but TLAPS does not yet do any *) +(* temporal reasoning. *) +(***************************************************************************) +THEOREM Spec => []MutualExclusion +<1> USE N \in Nat DEFS Procs, TypeOK, Before, \prec, ProcSet +<1>1. Init => Inv + BY DEF Init, Inv +<1>2. Inv /\ [Next]_vars => Inv' <2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' @@ -284,193 +284,193 @@ THEOREM Spec => []MutualExclusion <2>1. ASSUME NEW self \in Procs, ncs(self) PROVE Inv' - BY <2>1 DEF ncs, Inv + BY <2>1 DEF ncs, Inv <2>2. ASSUME NEW self \in Procs, e1(self) PROVE Inv' - <3>. /\ pc[self] = "e1" - /\ UNCHANGED <> - BY <2>2 DEF e1 - <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] - /\ pc' = [pc EXCEPT ![self] = "e1"] - /\ UNCHANGED <> - BY <3>1 DEF Inv - <3>2. CASE /\ flag' = [flag EXCEPT ![self] = TRUE] - /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] - /\ max' = [max EXCEPT ![self] = 0] - /\ pc' = [pc EXCEPT ![self] = "e2"] - BY <3>2 DEF Inv - <3>. QED BY <3>1, <3>2, <2>2 DEF e1 + <3>. /\ pc[self] = "e1" + /\ UNCHANGED <> + BY <2>2 DEF e1 + <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] + /\ pc' = [pc EXCEPT ![self] = "e1"] + /\ UNCHANGED <> + BY <3>1 DEF Inv + <3>2. CASE /\ flag' = [flag EXCEPT ![self] = TRUE] + /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] + /\ max' = [max EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "e2"] + BY <3>2 DEF Inv + <3>. QED BY <3>1, <3>2, <2>2 DEF e1 <2>3. ASSUME NEW self \in Procs, e2(self) PROVE Inv' - <3>. /\ pc[self] = "e2" - /\ UNCHANGED << num, flag, nxt >> - BY <2>3 DEF e2 - <3>1. ASSUME NEW i \in unchecked[self], - unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], - num[i] > max[self], - max' = [max EXCEPT ![self] = num[i]], - pc' = [pc EXCEPT ![self] = "e2"] - PROVE Inv' - BY <3>1, Z3T(10) DEF Inv - <3>2. ASSUME NEW i \in unchecked[self], - unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], - ~(num[i] > max[self]), - max' = max, - pc' = [pc EXCEPT ![self] = "e2"] - PROVE Inv' - <4>. TypeOK' BY <3>2 DEF Inv -\* <4>0. \A ii \in Procs : (pc'[ii] \in {"ncs", "e1", "e2"}) => (num'[ii] = 0) -\* BY <3>2 DEF Inv - <4>1. \A ii \in Procs : (pc'[ii] \in {"e4", "w1", "w2", "cs"}) => (num'[ii] # 0) - BY <3>2 DEF Inv - <4>2. \A ii \in Procs : (pc'[ii] \in {"e2", "e3"}) => flag'[ii] - BY <3>2 DEF Inv - <4>3. \A ii \in Procs : (pc'[ii] = "w2") => (nxt'[ii] # ii) - BY <3>2 DEF Inv - <4>4. \A ii \in Procs : pc'[ii] \in {(*"e2",*) "w1", "w2"} => ii \notin unchecked'[ii] - BY <3>2 DEF Inv - <4>5. \A ii \in Procs : (pc'[ii] \in {"w1", "w2"}) => - \A j \in (Procs \ unchecked'[ii]) \ {ii} : Before(ii, j)' - BY <3>2 DEF Inv - <4>6. \A ii \in Procs : - /\ (pc'[ii] = "w2") - /\ \/ (pc'[nxt'[ii]] = "e2") /\ (ii \notin unchecked'[nxt'[ii]]) - \/ pc'[nxt'[ii]] = "e3" - => max'[nxt'[ii]] >= num'[ii] - BY <3>2 DEF Inv - <4>7. \A ii \in Procs : (pc'[ii] = "cs") => \A j \in Procs \ {ii} : Before(ii, j)' - BY <3>2 DEF Inv - <4>. QED BY (*<4>0,*) <4>1, <4>2, <4>3, <4>4, <4>5, <4>6, <4>7 DEF Inv - <3>3. CASE /\ unchecked[self] = {} - /\ pc' = [pc EXCEPT ![self] = "e3"] - /\ UNCHANGED << unchecked, max >> - BY <3>3 DEF Inv - <3>. QED BY <3>1, <3>2, <3>3, <2>3 DEF e2 + <3>. /\ pc[self] = "e2" + /\ UNCHANGED << num, flag, nxt >> + BY <2>3 DEF e2 + <3>1. ASSUME NEW i \in unchecked[self], + unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], + num[i] > max[self], + max' = [max EXCEPT ![self] = num[i]], + pc' = [pc EXCEPT ![self] = "e2"] + PROVE Inv' + BY <3>1, Z3T(10) DEF Inv + <3>2. ASSUME NEW i \in unchecked[self], + unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}], + ~(num[i] > max[self]), + max' = max, + pc' = [pc EXCEPT ![self] = "e2"] + PROVE Inv' + <4>. TypeOK' BY <3>2 DEF Inv +\* <4>0. \A ii \in Procs : (pc'[ii] \in {"ncs", "e1", "e2"}) => (num'[ii] = 0) +\* BY <3>2 DEF Inv + <4>1. \A ii \in Procs : (pc'[ii] \in {"e4", "w1", "w2", "cs"}) => (num'[ii] # 0) + BY <3>2 DEF Inv + <4>2. \A ii \in Procs : (pc'[ii] \in {"e2", "e3"}) => flag'[ii] + BY <3>2 DEF Inv + <4>3. \A ii \in Procs : (pc'[ii] = "w2") => (nxt'[ii] # ii) + BY <3>2 DEF Inv + <4>4. \A ii \in Procs : pc'[ii] \in {(*"e2",*) "w1", "w2"} => ii \notin unchecked'[ii] + BY <3>2 DEF Inv + <4>5. \A ii \in Procs : (pc'[ii] \in {"w1", "w2"}) => + \A j \in (Procs \ unchecked'[ii]) \ {ii} : Before(ii, j)' + BY <3>2 DEF Inv + <4>6. \A ii \in Procs : + /\ (pc'[ii] = "w2") + /\ \/ (pc'[nxt'[ii]] = "e2") /\ (ii \notin unchecked'[nxt'[ii]]) + \/ pc'[nxt'[ii]] = "e3" + => max'[nxt'[ii]] >= num'[ii] + BY <3>2 DEF Inv + <4>7. \A ii \in Procs : (pc'[ii] = "cs") => \A j \in Procs \ {ii} : Before(ii, j)' + BY <3>2 DEF Inv + <4>. QED BY (*<4>0,*) <4>1, <4>2, <4>3, <4>4, <4>5, <4>6, <4>7 DEF Inv + <3>3. CASE /\ unchecked[self] = {} + /\ pc' = [pc EXCEPT ![self] = "e3"] + /\ UNCHANGED << unchecked, max >> + BY <3>3 DEF Inv + <3>. QED BY <3>1, <3>2, <3>3, <2>3 DEF e2 <2>4. ASSUME NEW self \in Procs, e3(self) PROVE Inv' - <3>. /\ pc[self] = "e3" - /\ UNCHANGED << flag, unchecked, max, nxt >> - BY <2>4 DEF e3 - <3>1. CASE /\ \E k \in Nat: - num' = [num EXCEPT ![self] = k] - /\ pc' = [pc EXCEPT ![self] = "e3"] - BY <3>1 DEF Inv - <3>2. CASE /\ \E i \in {j \in Nat : j > max[self]}: - num' = [num EXCEPT ![self] = i] - /\ pc' = [pc EXCEPT ![self] = "e4"] - BY <3>2, Z3 DEF Inv - <3>3. QED BY <3>1, <3>2, <2>4 DEF e3 + <3>. /\ pc[self] = "e3" + /\ UNCHANGED << flag, unchecked, max, nxt >> + BY <2>4 DEF e3 + <3>1. CASE /\ \E k \in Nat: + num' = [num EXCEPT ![self] = k] + /\ pc' = [pc EXCEPT ![self] = "e3"] + BY <3>1 DEF Inv + <3>2. CASE /\ \E i \in {j \in Nat : j > max[self]}: + num' = [num EXCEPT ![self] = i] + /\ pc' = [pc EXCEPT ![self] = "e4"] + BY <3>2, Z3 DEF Inv + <3>3. QED BY <3>1, <3>2, <2>4 DEF e3 <2>5. ASSUME NEW self \in Procs, e4(self) PROVE Inv' - <3>. /\ pc[self] = "e4" - /\ UNCHANGED << num, max, nxt >> - BY <2>5 DEF e4 - <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] - /\ pc' = [pc EXCEPT ![self] = "e4"] - /\ UNCHANGED unchecked - BY <3>1 DEF Inv - <3>2. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] - /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] - /\ pc' = [pc EXCEPT ![self] = "w1"] - BY <3>2 DEF Inv - <3>. QED BY <3>1, <3>2, <2>5 DEF e4 + <3>. /\ pc[self] = "e4" + /\ UNCHANGED << num, max, nxt >> + BY <2>5 DEF e4 + <3>1. CASE /\ flag' = [flag EXCEPT ![self] = ~ flag[self]] + /\ pc' = [pc EXCEPT ![self] = "e4"] + /\ UNCHANGED unchecked + BY <3>1 DEF Inv + <3>2. CASE /\ flag' = [flag EXCEPT ![self] = FALSE] + /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}] + /\ pc' = [pc EXCEPT ![self] = "w1"] + BY <3>2 DEF Inv + <3>. QED BY <3>1, <3>2, <2>5 DEF e4 <2>6. ASSUME NEW self \in Procs, w1(self) PROVE Inv' - <3>. /\ pc[self] = "w1" - /\ UNCHANGED << num, flag, unchecked, max >> - BY <2>6 DEF w1 - <3>1. CASE /\ unchecked[self] # {} - /\ \E i \in unchecked[self]: - nxt' = [nxt EXCEPT ![self] = i] - /\ ~ flag[nxt'[self]] - /\ pc' = [pc EXCEPT ![self] = "w2"] - BY <3>1, Z3 DEF Inv - <3>2. CASE /\ unchecked[self] = {} - /\ pc' = [pc EXCEPT ![self] = "cs"] - /\ nxt' = nxt - BY <3>2, Z3 DEF Inv - <3>. QED BY <3>1, <3>2, <2>6 DEF w1 + <3>. /\ pc[self] = "w1" + /\ UNCHANGED << num, flag, unchecked, max >> + BY <2>6 DEF w1 + <3>1. CASE /\ unchecked[self] # {} + /\ \E i \in unchecked[self]: + nxt' = [nxt EXCEPT ![self] = i] + /\ ~ flag[nxt'[self]] + /\ pc' = [pc EXCEPT ![self] = "w2"] + BY <3>1, Z3 DEF Inv + <3>2. CASE /\ unchecked[self] = {} + /\ pc' = [pc EXCEPT ![self] = "cs"] + /\ nxt' = nxt + BY <3>2, Z3 DEF Inv + <3>. QED BY <3>1, <3>2, <2>6 DEF w1 <2>7. ASSUME NEW self \in Procs, w2(self) PROVE Inv' - BY <2>7, Z3 DEF w2, Inv + BY <2>7, Z3 DEF w2, Inv <2>8. ASSUME NEW self \in Procs, cs(self) PROVE Inv' - BY <2>8, Z3 DEF cs, Inv + BY <2>8, Z3 DEF cs, Inv <2>9. ASSUME NEW self \in Procs, exit(self) PROVE Inv' - <3>. /\ pc[self] = "exit" - /\ UNCHANGED << flag, unchecked, max, nxt >> - BY <2>9 DEF exit - <3>1. CASE /\ \E k \in Nat: - num' = [num EXCEPT ![self] = k] - /\ pc' = [pc EXCEPT ![self] = "exit"] - BY <3>1 DEF Inv - <3>2. CASE /\ num' = [num EXCEPT ![self] = 0] - /\ pc' = [pc EXCEPT ![self] = "ncs"] - BY <3>2 DEF Inv - <3>. QED BY <3>1, <3>2, <2>9 DEF exit + <3>. /\ pc[self] = "exit" + /\ UNCHANGED << flag, unchecked, max, nxt >> + BY <2>9 DEF exit + <3>1. CASE /\ \E k \in Nat: + num' = [num EXCEPT ![self] = k] + /\ pc' = [pc EXCEPT ![self] = "exit"] + BY <3>1 DEF Inv + <3>2. CASE /\ num' = [num EXCEPT ![self] = 0] + /\ pc' = [pc EXCEPT ![self] = "ncs"] + BY <3>2 DEF Inv + <3>. QED BY <3>1, <3>2, <2>9 DEF exit <2>10. CASE UNCHANGED vars - BY <2>10 DEF vars, Inv + BY <2>10 DEF vars, Inv <2>11. QED BY <2>1, <2>10, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next, p -<1>3. Inv => MutualExclusion - BY SMT DEF MutualExclusion, Inv -<1>4. QED - BY <1>1, <1>2, <1>3, PTL DEF Spec ------------------------------------------------------------------------------- -Trying(i) == pc[i] = "e1" -InCS(i) == pc[i] = "cs" -DeadlockFree == (\E i \in Procs : Trying(i)) ~> (\E i \in Procs : InCS(i)) -StarvationFree == \A i \in Procs : Trying(i) ~> InCS(i) - ------------------------------------------------------------------------------ -II == \A i \in Procs : -\* /\ (pc[i] \in {"ncs", "e1", "e2"}) => (num[i] = 0) \* not found Test 1 (21993 states) - /\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0) \* found Test 1 - /\ (pc[i] \in {"e2", "e3"}) => flag[i] \* found Test 1 - /\ (pc[i] = "w2") => (nxt[i] # i) \* not found Test 1 (12115 states) or with N=2 - /\ pc[i] \in {"e2", "w1", "w2"} => i \notin unchecked[i] \* found Test 1 - /\ (pc[i] \in {"w1", "w2"}) => \* found Test 1 - \A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j) - /\ /\ (pc[i] = "w2") \* found Test 1 - /\ \/ (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) \* found Test 1 - -IInit == /\ 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"}] - /\ II - -ISpec == IInit /\ [][Next]_vars - -============================================================================= +<1>3. Inv => MutualExclusion + BY SMT DEF MutualExclusion, Inv +<1>4. QED + BY <1>1, <1>2, <1>3, PTL DEF Spec +------------------------------------------------------------------------------ +Trying(i) == pc[i] = "e1" +InCS(i) == pc[i] = "cs" +DeadlockFree == (\E i \in Procs : Trying(i)) ~> (\E i \in Procs : InCS(i)) +StarvationFree == \A i \in Procs : Trying(i) ~> InCS(i) + +----------------------------------------------------------------------------- +II == \A i \in Procs : +\* /\ (pc[i] \in {"ncs", "e1", "e2"}) => (num[i] = 0) \* not found Test 1 (21993 states) + /\ (pc[i] \in {"e4", "w1", "w2", "cs"}) => (num[i] # 0) \* found Test 1 + /\ (pc[i] \in {"e2", "e3"}) => flag[i] \* found Test 1 + /\ (pc[i] = "w2") => (nxt[i] # i) \* not found Test 1 (12115 states) or with N=2 + /\ pc[i] \in {"e2", "w1", "w2"} => i \notin unchecked[i] \* found Test 1 + /\ (pc[i] \in {"w1", "w2"}) => \* found Test 1 + \A j \in (Procs \ unchecked[i]) \ {i} : Before(i, j) + /\ /\ (pc[i] = "w2") \* found Test 1 + /\ \/ (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) \* found Test 1 + +IInit == /\ 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"}] + /\ II + +ISpec == IInit /\ [][Next]_vars + +============================================================================= \* Modification History +\* 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 - -Test 1: 5248 distinct initial states 151056 full initial states -IInit == /\ num \in [Procs -> Nat] - /\ flag \in [Procs -> BOOLEAN] - /\ unchecked \in [Procs -> SUBSET Procs] - /\ max \in [Procs -> {0}] \* Nat] - /\ nxt \in [Procs -> {1}] - /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", - "e4", "w1", "w2", "cs"}] - /\ II - +\* 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 + +Test 1: 5248 distinct initial states 151056 full initial states +IInit == /\ num \in [Procs -> Nat] + /\ flag \in [Procs -> BOOLEAN] + /\ unchecked \in [Procs -> SUBSET Procs] + /\ max \in [Procs -> {0}] \* Nat] + /\ nxt \in [Procs -> {1}] + /\ pc \in [Procs -> {"ncs", "e1", "e2", "e3", + "e4", "w1", "w2", "cs"}] + /\ II diff --git a/specifications/Bakery-Boulangerie/Boulanger.tla b/specifications/Bakery-Boulangerie/Boulanger.tla index f10e2b22..c1e87a3a 100644 --- a/specifications/Bakery-Boulangerie/Boulanger.tla +++ b/specifications/Bakery-Boulangerie/Boulanger.tla @@ -164,7 +164,8 @@ a \prec b == \/ a[1] < b[1] } } -*** this ends the comment containg the pluscal code **********) + this ends the comment containing the PlusCal code +*************) \* BEGIN TRANSLATION (this begins the translation of the PlusCal code) VARIABLES num, flag, pc, unchecked, max, nxt, previous @@ -530,6 +531,7 @@ DeadlockFree == (\E i \in Procs : Trying(i)) ~> (\E i \in Procs : InCS(i)) StarvationFree == \A i \in Procs : Trying(i) ~> InCS(i) ============================================================================= \* Modification History +\* Last modified Tue Aug 27 12:22:38 PDT 2019 by loki \* Last modified Thu May 24 20:03:58 CEST 2018 by merz \* Last modified Thu May 24 13:49:22 CEST 2018 by merz \* Last modified Tue Jul 21 17:55:23 PDT 2015 by lamport diff --git a/specifications/LoopInvariance/BinarySearch.tla b/specifications/LoopInvariance/BinarySearch.tla index 3dcec84f..872f4dd0 100644 --- a/specifications/LoopInvariance/BinarySearch.tla +++ b/specifications/LoopInvariance/BinarySearch.tla @@ -35,7 +35,7 @@ SortedSeqs == {ss \in Seq(Values) : if (mval = val) { result := mid} else if (val < mval) { high := mid - 1} else {low := mid + 1} } } } } - ***************************************************************************) +***************************************************************************) \* BEGIN TRANSLATION VARIABLES seq, val, low, high, result, pc @@ -249,6 +249,7 @@ THEOREM Spec => []resultCorrect <1>4. QED BY <1>1, <1>2, <1>3, PTL DEF Spec ============================================================================= -\* Modification History +\* Modification History +\* Last modified Tue Aug 27 12:59:52 PDT 2019 by loki \* Last modified Fri May 03 16:28:58 PDT 2019 by lamport \* Created Wed Apr 17 15:15:12 PDT 2019 by lamport diff --git a/specifications/LoopInvariance/SumSequence.tla b/specifications/LoopInvariance/SumSequence.tla index 37059f65..40e9d63e 100644 --- a/specifications/LoopInvariance/SumSequence.tla +++ b/specifications/LoopInvariance/SumSequence.tla @@ -53,7 +53,7 @@ with the variable sum equal to the sum of the elements of seq. n := n+1 ; } } } - ***************************************************************************) +***************************************************************************) \* BEGIN TRANSLATION VARIABLES seq, sum, n, pc @@ -542,6 +542,7 @@ LEMMA Lemma5_Proof == <1>4. QED BY <1>3 ============================================================================= -\* Modification History +\* Modification History +\* Last modified Tue Aug 27 12:59:10 PDT 2019 by loki \* Last modified Fri May 03 16:40:42 PDT 2019 by lamport \* Created Fri Apr 19 14:13:06 PDT 2019 by lamport diff --git a/specifications/MisraReachability/ParReach.tla b/specifications/MisraReachability/ParReach.tla index bb2e8dab..2a809a35 100644 --- a/specifications/MisraReachability/ParReach.tla +++ b/specifications/MisraReachability/ParReach.tla @@ -88,9 +88,9 @@ simpler. } -Here is the TLA+ translation of the PlusCal code. - ***************************************************************************) -\* BEGIN TRANSLATION + +***************************************************************************) +\* BEGIN TRANSLATION Here is the TLA+ translation of the PlusCal code. VARIABLES marked, vroot, pc, u, toVroot vars == << marked, vroot, pc, u, toVroot >> @@ -230,6 +230,8 @@ THEOREM Spec => R!Spec THEOREM Spec => R!Init /\ [][R!Next]_R!vars THEOREM Spec => WF_R!vars(R!Next) ============================================================================= -\* Modification History +\* Modification History +\* Last modified Tue Aug 27 14:58:47 PDT 2019 by loki +\* Last modified Fri Jun 28 16:26:24 PDT 2019 by loki \* Last modified Sun Apr 14 16:53:23 PDT 2019 by lamport \* Created Mon Apr 08 10:48:52 PDT 2019 by lamport diff --git a/specifications/MisraReachability/Reachable.tla b/specifications/MisraReachability/Reachable.tla index 2d8ee3a0..eeeb697e 100644 --- a/specifications/MisraReachability/Reachable.tla +++ b/specifications/MisraReachability/Reachable.tla @@ -76,10 +76,9 @@ node and does the following: } -Here is the TLA+ translation of the PlusCal code. ***************************************************************************) -\* BEGIN TRANSLATION +\* BEGIN TRANSLATION Here is the TLA+ translation of the PlusCal code. VARIABLES marked, vroot, pc \*Reachable == ReachableFrom(marked) (* added for a test *) @@ -234,7 +233,8 @@ THEOREM ASSUME IsFiniteSet(Reachable) (* dozen nodes. *) (**************************************************************************) ============================================================================= -\* Modification History +\* Modification History +\* Last modified Tue Aug 27 14:46:36 PDT 2019 by loki \* Last modified Wed Apr 17 12:21:22 PDT 2019 by lamport \* Created Thu Apr 04 10:11:51 PDT 2019 by lamport