From 535c498ae50ccf16396646f50e816ebae4098589 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sat, 18 Jul 2026 19:19:31 +0200 Subject: [PATCH] safety proof of EWD687a Signed-off-by: Stephan Merz --- .../AdvancedExamples/Graphs.tla | 6 + specifications/ewd687a/EWD687a.tla | 46 +- specifications/ewd687a/EWD687a_proof.tla | 1248 +++++------------ specifications/ewd687a/MCEWD687a.cfg | 42 +- specifications/ewd687a/MCEWD687a.tla | 32 +- 5 files changed, 368 insertions(+), 1006 deletions(-) diff --git a/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla b/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla index c2c99508..1d555699 100644 --- a/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla +++ b/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla @@ -1,4 +1,10 @@ ------------------------------- MODULE Graphs ------------------------------- +(***************************************************************************) +(* Representation of (directed) graphs in TLA+. *) +(* This is the ancestor of the Graphs community module, available at *) +(* https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla *) +(* which contains more operators and also slightly changed definitions. *) +(***************************************************************************) LOCAL INSTANCE Naturals LOCAL INSTANCE Sequences diff --git a/specifications/ewd687a/EWD687a.tla b/specifications/ewd687a/EWD687a.tla index 948ecf08..cdc2c4a8 100644 --- a/specifications/ewd687a/EWD687a.tla +++ b/specifications/ewd687a/EWD687a.tla @@ -87,7 +87,7 @@ (* not to be detected. It requires that a process can send acknowledgment *) (* messages to any process that can send it computation messages. *) (***************************************************************************) -EXTENDS Integers +EXTENDS Integers, Graphs (***************************************************************************) (* We declare the following constants: *) @@ -215,7 +215,7 @@ VARIABLES (* network. In an implementation, we would, thus, expect to find *) (* code that maintains the values of active, sentUnacked, and *) (* rcvdUnacked in the implementation of a process. The variables msgs *) - (* and acks, however, would likely be implicitly because they model *) + (* and acks, however, would likely be implicit because they model *) (* the state of the network. *) (***********************************************************************) @@ -231,7 +231,7 @@ VARIABLES msgs, (***********************************************************************) (* For an edge <> \in OutEdges(p), acks[<>] is the number of *) - (* control) messages in transit from process p to process q. *) + (* (control) messages in transit from process p to process q. *) (***********************************************************************) acks (***********************************************************************) @@ -330,7 +330,7 @@ RcvAck(p) == \E e \in OutEdges(p) : (* 2b. The receiver q of the ack is the parent of p in the overlay tree, *) (* and p is neutral after sending the ack. *) (* *) -(* UP. If process p is neutral after sending an ack (hence netural(p)'), *) +(* UP. If process p is neutral after sending an ack (hence neutral(p)'), *) (* it removes itself from the overlay tree by setting the value of *) (* upEdge[p] to NotAnEdge. *) (***************************************************************************) @@ -383,16 +383,17 @@ RcvMsg(p) == \E e \in InEdges(p) : (* that p was not a node of the overlay tree when it became idle. Thus, *) (* there is no need to change upEdge[p] in the Idle subaction. *) (***************************************************************************) -Idle(p) == /\ active' = [active EXCEPT ![p] = FALSE] +Idle(p) == /\ active[p] \* otherwise this step is subsumed by stuttering + /\ active' = [active EXCEPT ![p] = FALSE] /\ UNCHANGED <> ---------------------------------------------------------------------------- - + Next == \E p \in Procs : SendMsg(p) \/ SendAck(p) \/ RcvMsg(p) \/ RcvAck(p) \/ Idle(p) Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - + ---------------------------------------------------------------------------- (***************************************************************************) @@ -401,34 +402,33 @@ Spec == Init /\ [][Next]_vars /\ WF_vars(Next) (* rcvdUnacked[e] equals sentUnacked[e], for any e in Edges. *) (***************************************************************************) CountersConsistent == - [] \A e \in Edges: sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e] + \A e \in Edges: sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e] -THEOREM Spec => CountersConsistent +THEOREM Spec => []CountersConsistent (***************************************************************************) -(* The overlay tree is a tree of non-neutral nodes rooted in the leader, *) -(* or the tree is empty s.t. it has no edges nor nodes. *) -(* With bigger graphs, expect a significant slowdown when model-checking *) -(* the property TreeWithRoot. *) +(* The overlay tree is a tree rooted in the leader such that all inner *) +(* nodes are non-neutral. *) (* *) (* In a variant of this spec, the conjunct labelled Up in the SendAck *) (* subactions could be removed. In this variant, the processes in the *) (* overlay tree would be processes that are or were non-neutral in the *) (* past. Consequently, the conjunct labelled N would have to be *) -(* removed from the property TreeWithRoot . *) +(* removed from the property TreeWithRoot. *) (***************************************************************************) + TreeWithRoot == LET E == {upEdge[p] : p \in DOMAIN upEdge} \ {NotAnEdge} - N == {e[1] : e \in E} \cup {e[2] : e \in E} - G == INSTANCE Graphs - O == G!Transpose([edge |-> E, node |-> N]) - IN []( - \* O is a tree rooted in the leader. - /\ O.edge # {} => G!IsTreeWithRoot(O, Leader) - \* All nodes of the overlay tree are non-neutral. - /\ N:: \A n \in O.node: ~neutral(n)) + \* The original definition includes every node occurring in the tree + \* twice (except the leader), which unnecessarily complicates the proof. + N == (* {e[1] : e \in E} \cup *) {e[2] : e \in E} \cup {Leader} + O == Transpose([edge |-> E, node |-> N]) + IN \* O is a tree rooted in the leader. + /\ IsTreeWithRoot(O, Leader) + \* All nodes of the overlay tree, except the root, are non-neutral. + /\ N:: \A n \in O.node \ {Leader} : ~neutral(n) -THEOREM Spec => TreeWithRoot +THEOREM Spec => []TreeWithRoot --------------------------------------------------------------------------- diff --git a/specifications/ewd687a/EWD687a_proof.tla b/specifications/ewd687a/EWD687a_proof.tla index dff11b63..17f56ecd 100644 --- a/specifications/ewd687a/EWD687a_proof.tla +++ b/specifications/ewd687a/EWD687a_proof.tla @@ -1,8 +1,8 @@ --------------------------- MODULE EWD687a_proof --------------------------- (***************************************************************************) -(* TLAPS proofs of the theorems stated in EWD687a.tla. *) +(* Proofs of the theorems stated in EWD687a.tla. *) (***************************************************************************) -EXTENDS EWD687a, NaturalsInduction, FiniteSetTheorems, TLAPS +EXTENDS EWD687a, NaturalsInduction, FiniteSetTheorems, GraphTheorems, TLAPS ----------------------------------------------------------------------------- (***************************************************************************) @@ -18,18 +18,16 @@ EXTENDS EWD687a, NaturalsInduction, FiniteSetTheorems, TLAPS (* knowing the counters are consistent. We therefore prove TypeOK and the *) (* state predicate Counters together as a single inductive invariant. *) (***************************************************************************) -Counters == \A e \in Edges : sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e] +Inv1 == TypeOK /\ CountersConsistent -Inv1 == TypeOK /\ Counters - -LEMMA Inv1Init == Init => Inv1 -BY DEF Init, Inv1, TypeOK, Counters, NotAnEdge - -LEMMA Inv1Step == Inv1 /\ [Next]_vars => Inv1' +THEOREM Invariant1 == Spec => []Inv1 +<1>1. Init => Inv1 + BY DEF Init, Inv1, TypeOK, CountersConsistent, NotAnEdge +<1>2. Inv1 /\ [Next]_vars => Inv1' <2> SUFFICES ASSUME Inv1, [Next]_vars PROVE Inv1' OBVIOUS - <2>. USE DEF Inv1, TypeOK, Counters + <2>. USE DEF Inv1, TypeOK, CountersConsistent <2>1. ASSUME NEW p \in Procs, SendMsg(p) PROVE Inv1' BY <2>1 DEF SendMsg, OutEdges @@ -62,952 +60,340 @@ LEMMA Inv1Step == Inv1 /\ [Next]_vars => Inv1' <2>6. CASE UNCHANGED vars BY <2>6 DEF vars <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next - -LEMMA Inv1Inductive == Spec => []Inv1 -BY Inv1Init, Inv1Step, PTL DEF Spec +<1>. QED BY <1>1, <1>2, PTL DEF Spec THEOREM TypeCorrect == Spec => []TypeOK -BY Inv1Inductive, PTL DEF Inv1 +BY Invariant1, PTL DEF Inv1 THEOREM Thm_CountersConsistent == Spec => CountersConsistent -BY Inv1Inductive, PTL DEF CountersConsistent, Inv1, Counters +BY Invariant1, PTL DEF CountersConsistent, Inv1 ----------------------------------------------------------------------------- (***************************************************************************) -(* Theorem 3: Spec => []DT1Inv *) -(* *) -(* Main safety property: when the leader is neutral, the entire *) -(* computation has terminated, i.e., every non-leader process is also *) -(* neutral. *) -(* *) -(* DT1Inv is not directly inductive. We strengthen it by adding two *) -(* invariants describing the structure of the overlay tree: *) -(* *) -(* - Non-neutral non-leader processes always have an upEdge (so they *) -(* are part of the overlay tree). *) -(* - If p is in the tree, then upEdge[p] is a well-formed incoming edge *) -(* of p, the edge has at least one unacknowledged message *) -(* (rcvdUnacked >= 1), and (the key fact for DT1Inv) the parent of p *) -(* in the overlay tree is itself non-neutral. *) -(* *) -(* From the second invariant, the chain of upEdges from any non-neutral *) -(* non-leader p consists of non-neutral processes, so the leader cannot *) -(* be neutral whenever any other process is non-neutral. Formalising the *) -(* finite-chain argument needs Procs to be finite and a small amount of *) -(* well-founded reasoning, factored out as a separate lemma. *) +(* In preparation of the main correctness theorem expressed by DT1Inv, we *) +(* prove a strengthening of invariant TreeWithRoot. *) (***************************************************************************) -ASSUME ProcsFinite == IsFiniteSet(Procs) +TreeInv == + /\ TreeWithRoot + /\ \A p \in Procs \ {Leader} : + /\ upEdge[p] = NotAnEdge => neutral(p) + /\ upEdge[p] # NotAnEdge => + /\ upEdge[p] \in InEdges(p) + /\ rcvdUnacked[upEdge[p]] # 0 -InTree(p) == upEdge[p] # NotAnEdge - -Inv2 == /\ \A p \in Procs \ {Leader} : ~neutral(p) => InTree(p) - /\ \A p \in Procs \ {Leader} : - InTree(p) => - /\ upEdge[p] \in Edges - /\ upEdge[p][2] = p - /\ upEdge[p][1] \in Procs \ {p} - /\ rcvdUnacked[upEdge[p]] >= 1 - -(***************************************************************************) -(* The chain step. *) -(* *) -(* Assume Inv2 and neutral(Leader). Suppose, for contradiction, that *) -(* S == {p \in Procs \ {Leader} : ~neutral(p)} is non-empty. *) -(* *) -(* - Conjunct 3 of Inv2 gives InTree(p) for every p in S. *) -(* - Conjunct 4 of Inv2 + Counters give sentUnacked[upEdge[p]] >= 1, *) -(* so the parent upEdge[p][1] is non-neutral. *) -(* - Since neutral(Leader), the parent is not Leader, hence the parent *) -(* is itself in S. *) -(* *) -(* So upEdge[_][1] defines a function f : S -> S with no fixed points. *) -(* In any non-empty set such an f might still admit a cycle, so we need an *) -(* auxiliary invariant ruling out cycles in the upEdge graph. We use the *) -(* following formulation: there is no non-empty set of in-tree non-leader *) -(* processes that is closed under taking the parent. (Equivalently: every *) -(* in-tree process can reach the leader by following upEdge.) *) -(* *) -(* NoCycle is established inductively (NoCycleInductive below). All *) -(* actions other than RcvMsg either leave upEdge unchanged or, in the *) -(* case of SendAck removing p from the tree, leave p with no children *) -(* (its OutEdges are quiescent), so any putative new closed set would *) -(* already have been a closed set in the previous state. RcvMsg may *) -(* attach a new process p to the tree with parent e[1]; if a closed set *) -(* S' arose in the new state with p \in S', then by Counters and Inv2 *) -(* conjunct 4 no other in-tree process points to p (since p was neutral, *) -(* every OutEdge of p has sentUnacked = 0), so removing p from S' yields *) -(* a smaller closed set in the previous state - contradicting the *) -(* induction hypothesis. *) -(***************************************************************************) -NoCycle == \A S \in SUBSET (Procs \ {Leader}) : - ~ (/\ S # {} - /\ \A q \in S : InTree(q) /\ upEdge[q][1] \in S) +LEMMA NotAnEdgeNoEdge == NotAnEdge \notin Edges +BY EdgeFacts DEF NotAnEdge -LEMMA Inv2Inductive == Spec => []Inv2 -<1>1. Init => Inv2 - <2>. SUFFICES ASSUME Init PROVE Inv2 - OBVIOUS - <2>2. \A p \in Procs \ {Leader} : ~neutral(p) => InTree(p) - BY DEF Init, neutral, InEdges, OutEdges - <2>3. \A p \in Procs \ {Leader} : ~ InTree(p) - BY DEF Init, InTree, NotAnEdge - <2>. QED BY <2>2, <2>3 DEF Inv2 -<1>2. Inv1 /\ Inv1' /\ Inv2 /\ [Next]_vars => Inv2' - <2> SUFFICES ASSUME Inv1, Inv1', Inv2, [Next]_vars - PROVE Inv2' - OBVIOUS - <2>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge - <2>1. ASSUME NEW p \in Procs, SendMsg(p) - PROVE Inv2' - \* SendMsg only changes sentUnacked and msgs on one out-edge of p. - \* It does not change active, rcvdUnacked, or upEdge. - BY <2>1, EdgeFacts DEF SendMsg, OutEdges, InEdges, neutral - <2>5. ASSUME NEW p \in Procs, Idle(p) - PROVE Inv2' - \* Idle only changes active[p] to FALSE. Counters and upEdge are - \* unchanged. Neutral status of any p' might switch from non-neutral - \* to neutral, but the conjuncts of Inv2 are upper bounds, so they - \* are preserved. - BY <2>5, EdgeFacts DEF Idle, OutEdges, InEdges, neutral - <2>6. CASE UNCHANGED vars - BY <2>6 DEF vars, neutral, InEdges, OutEdges - <2>2. ASSUME NEW p \in Procs, RcvAck(p) - PROVE Inv2' - <3>1. PICK e \in OutEdges(p) : - /\ acks[e] > 0 - /\ acks' = [acks EXCEPT ![e] = @ - 1] - /\ sentUnacked' = [sentUnacked EXCEPT ![e] = @ - 1] - /\ UNCHANGED <> - BY <2>2 DEF RcvAck - <3>2. e \in Edges /\ e[1] = p /\ e[1] # e[2] /\ e[2] \in Procs \ {p} - BY <3>1, EdgeFacts DEF OutEdges - \* Only sentUnacked and acks for e change. active, rcvdUnacked, msgs, - \* and upEdge are unchanged. The neutrality of any q with q # p is - \* unaffected (sentUnacked, acks change only on edges in OutEdges(p)). - <3>3. \A q \in Procs : q # p => (neutral(q) <=> neutral(q)') - BY <3>1, <3>2 DEF neutral, OutEdges, InEdges - \* For p, the new sentUnacked[e] is one less; if that makes p neutral, - \* the conjunct "non-neutral implies InTree" still holds (vacuously - \* for p) since others' status is preserved. - <3>4. \A q \in Procs \ {Leader} : ~ neutral(q)' => InTree(q)' - <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, ~ neutral(q)' - PROVE InTree(q)' - OBVIOUS - <4>2. CASE q = p - \* upEdge unchanged, so InTree(p)' = InTree(p). Need ~neutral(p). - \* If neutral(p) before, then sentUnacked[e] = 0 (since e \in - \* OutEdges(p)). By Counters, acks[e] = 0, contradicting <3>1. - <5>1. ~ neutral(p) - <6>1. SUFFICES ASSUME neutral(p) PROVE FALSE - OBVIOUS - <6>2. sentUnacked[e] = 0 - BY <3>2, <6>1 DEF neutral - <6>3. acks[e] = 0 - BY <3>2, <6>2 DEF Counters - <6>4. acks[e] > 0 - BY <3>1 - <6>. QED BY <6>3, <6>4 - <5>2. InTree(p) - BY <4>2, <5>1 - <5>3. upEdge'[p] = upEdge[p] - BY <3>1 - <5>. QED BY <4>2, <5>2, <5>3 - <4>3. CASE q # p - <5>1. ~ neutral(q) - BY <3>3, <4>3, <4>1 - <5>2. InTree(q) - BY <5>1 - <5>3. upEdge'[q] = upEdge[q] - BY <3>1 - <5>. QED BY <5>2, <5>3 - <4>. QED BY <4>2, <4>3 - <3>5. \A q \in Procs \ {Leader} : - InTree(q)' => - /\ upEdge'[q] \in Edges - /\ upEdge'[q][2] = q - /\ upEdge'[q][1] \in Procs \ {q} - /\ rcvdUnacked'[upEdge'[q]] >= 1 - <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, InTree(q)' - PROVE /\ upEdge'[q] \in Edges - /\ upEdge'[q][2] = q - /\ upEdge'[q][1] \in Procs \ {q} - /\ rcvdUnacked'[upEdge'[q]] >= 1 - OBVIOUS - <4>2. upEdge'[q] = upEdge[q] - BY <3>1 - <4>3. InTree(q) - BY <4>1, <4>2 - <4>4. /\ upEdge[q] \in Edges - /\ upEdge[q][2] = q - /\ upEdge[q][1] \in Procs \ {q} - /\ rcvdUnacked[upEdge[q]] >= 1 - BY <4>3 - <4>5. rcvdUnacked'[upEdge[q]] = rcvdUnacked[upEdge[q]] - BY <3>1 - <4>. QED BY <4>2, <4>4, <4>5 - <3>. QED BY <3>4, <3>5 DEF Inv2 - <2>3. ASSUME NEW p \in Procs, SendAck(p) - PROVE Inv2' - <3>1. PICK e \in InEdges(p) : - /\ rcvdUnacked[e] > 0 - /\ (e = upEdge[p]) => +THEOREM TreeInvariant == Spec => []TreeInv +<1>. DEFINE E == {upEdge[p] : p \in DOMAIN upEdge} \ {NotAnEdge} + N == {e[2] : e \in E} \cup {Leader} + T == [node |-> N, edge |-> E] + O == Transpose(T) +\* introductory steps for removing the LET in the definition of TreeWithRoot: +\* this allows us to hide the definitions of E, N, and O and reduce the size +\* of the formulas given to the backends +<1>1. TreeWithRoot <=> /\ IsTreeWithRoot(O, Leader) + /\ \A n \in N \ {Leader} : ~ neutral(n) + BY DEF TreeWithRoot, Transpose +<1>2. TreeWithRoot' <=> /\ IsTreeWithRoot(O', Leader) + /\ \A n \in N' \ {Leader} : ~ neutral(n)' + BY DEF TreeWithRoot, Transpose +<1>3. Init => TreeInv + <2>. SUFFICES ASSUME Init PROVE TreeWithRoot + BY DEF Init, TreeInv, neutral, InEdges, OutEdges + <2>. /\ N = {Leader} + /\ O = [edge |-> {}, node |-> N] + BY Zenon DEF Init, Transpose + <2>. HIDE DEF O, N + <2>. QED BY <1>1, SingletonIsTreeWithRoot +<1>4. Inv1 /\ Inv1' /\ TreeInv /\ [Next]_vars => TreeInv' + <2>. SUFFICES ASSUME TypeOK, TypeOK', CountersConsistent, TreeInv, [Next]_vars + PROVE TreeInv' + BY DEF Inv1 + <2>. USE DEF TypeOK + \* Because we have a tree, both ends of each edge are nodes + <2>1. ASSUME NEW e \in E PROVE e[1] \in N + <3>. E \subseteq Edges + OBVIOUS + <3>. HIDE DEF E, N, O + <3>1. IsTreeWithRoot(O, Leader) + BY <1>1 DEF TreeInv + <3>2. e[2] \in O.node + BY DEF Transpose, O, N + <3>3. PICK p \in Path(O) : p[1] = e[2] /\ p[Len(p)] = Leader + BY <3>1, <3>2 DEF IsTreeWithRoot, AreConnectedIn + <3>. p \in Seq(O.node) \ { <<>> } + BY DEF Path + <3>4. e[2] # Leader + BY EdgeFacts DEF InEdges + <3>5. 1 \in 1 .. Len(p)-1 + BY <3>3, <3>4 + <3>6. <> \in O.edge + BY <3>5 DEF Path + <3>7. <> \in O.edge + BY EdgeFacts DEF O, Transpose + <3>8. <> = <> + BY <3>1, <3>3, <3>6, <3>7 DEF IsTreeWithRoot + <3>9. e[1] \in O.node + BY <3>5, <3>8 + <3>. QED BY <3>9 DEF O, Transpose + <2>2. IsDirectedGraph(T) + BY EdgeFacts, <2>1 DEF IsDirectedGraph + <2>3. /\ N \subseteq Procs + /\ N' \subseteq Procs + BY EdgeFacts + <2>4. ASSUME NEW p \in Procs, SendMsg(p) PROVE TreeInv' + <3>1. UNCHANGED <> + BY <2>4 DEF SendMsg + <3>2. \A n \in Procs : neutral(n)' <=> neutral(n) + BY <2>4 DEF SendMsg, neutral, InEdges, OutEdges + <3>. HIDE DEF O, N + <3>. QED BY <1>1, <1>2, <2>3, <3>1, <3>2 DEF TreeInv + <2>5. ASSUME NEW p \in Procs, SendAck(p) PROVE TreeInv' + <3>1. PICK e \in InEdges(p) : + /\ rcvdUnacked[e] > 0 + /\ e = upEdge[p] => \/ rcvdUnacked[e] > 1 - \/ /\ ~ active[p] + \/ /\ ~ active[p] /\ \A d \in InEdges(p) \ {e} : rcvdUnacked[d] = 0 /\ \A d \in OutEdges(p) : sentUnacked[d] = 0 - /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ - 1] - /\ acks' = [acks EXCEPT ![e] = @ + 1] - BY <2>3 DEF SendAck - <3>2. /\ UNCHANGED <> - /\ upEdge' = IF neutral(p)' THEN [upEdge EXCEPT ![p] = NotAnEdge] - ELSE upEdge - BY <2>3 DEF SendAck - <3>3a. e \in Edges /\ e[2] = p /\ e \in Procs \X Procs /\ e[1] # e[2] - BY <3>1, EdgeFacts DEF InEdges - <3>3b. p # Leader - <4>1. SUFFICES ASSUME p = Leader PROVE FALSE - OBVIOUS - <4>2. e \in InEdges(Leader) - BY <3>1, <4>1 - <4>3. InEdges(Leader) = {} - BY EdgeFacts - <4>. QED BY <4>2, <4>3 - <3>3. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs - BY <3>3a, <3>3b - \* For q # p, neutrality is unchanged (rcvdUnacked, acks change only on - \* edge e in InEdges(p), so for q # p, no relevant counters change). - <3>4. \A q \in Procs : q # p => (neutral(q) <=> neutral(q)') - BY <3>1, <3>2, <3>3 DEF neutral, OutEdges, InEdges - \* Conjunct 3 of Inv2. - <3>5. \A q \in Procs \ {Leader} : ~ neutral(q)' => InTree(q)' - <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, ~ neutral(q)' - PROVE InTree(q)' - OBVIOUS - <4>2. CASE q = p - \* If neutral'(p) holds, ~ neutral(p)' is false; trivial. - \* Otherwise, upEdge' = upEdge. We must show p was non-neutral - \* before, hence upEdge[p] # NotAnEdge (i.e., InTree(p)). - <5>1. ~ neutral(p) - \* p was non-neutral because rcvdUnacked[e] > 0 with e \in - \* InEdges(p), so the conjunct rcvdUnacked = 0 of neutral fails. - BY <3>1, <3>3 DEF neutral - <5>2. InTree(p) - BY <4>2, <5>1 - <5>3. ~ neutral(p)' - BY <4>1, <4>2 - <5>4. upEdge'[p] = upEdge[p] - BY <3>2, <5>3 - <5>. QED BY <4>2, <5>2, <5>4 - <4>3. CASE q # p - <5>1. ~ neutral(q) - BY <3>4, <4>3, <4>1 - <5>2. InTree(q) - BY <5>1 - <5>3. upEdge'[q] = upEdge[q] - \* upEdge'[q] = upEdge[q] regardless of the conditional, since - \* the conditional only changes upEdge[p]. - BY <3>2, <4>3 - <5>. QED BY <5>2, <5>3 - <4>. QED BY <4>2, <4>3 - \* Conjunct 4 of Inv2. - <3>6. \A q \in Procs \ {Leader} : - InTree(q)' => - /\ upEdge'[q] \in Edges - /\ upEdge'[q][2] = q - /\ upEdge'[q][1] \in Procs \ {q} - /\ rcvdUnacked'[upEdge'[q]] >= 1 - <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, InTree(q)' - PROVE /\ upEdge'[q] \in Edges - /\ upEdge'[q][2] = q - /\ upEdge'[q][1] \in Procs \ {q} - /\ rcvdUnacked'[upEdge'[q]] >= 1 - OBVIOUS - <4>2. CASE q = p - \* InTree(p)' implies upEdge'[p] # NotAnEdge. By <3>2, this means - \* either ~neutral'(p) and upEdge unchanged for p, or neutral'(p) - \* and upEdge'[p] = NotAnEdge (contradicting InTree(p)'). - <5>1. ~ neutral(p)' - BY <4>1, <4>2, <3>2, <3>3 DEF NotAnEdge - <5>2. upEdge'[p] = upEdge[p] - BY <3>2, <5>1 - <5>3. InTree(p) - BY <4>1, <4>2, <5>2 - <5>4. /\ upEdge[p] \in Edges - /\ upEdge[p][2] = p - /\ upEdge[p][1] \in Procs \ {p} - /\ rcvdUnacked[upEdge[p]] >= 1 - BY <5>3, <3>3 - \* For the rcvdUnacked' >= 1 part: - \* - If upEdge[p] # e (the SendAck edge), then rcvdUnacked' is - \* unchanged at upEdge[p]. - \* - If upEdge[p] = e, then SendAck's case-2a/2b applies: either - \* rcvdUnacked[e] > 1 (so rcvdUnacked' >= 1), or neutral'(p) - \* holds, contradicting <5>1. - <5>5. rcvdUnacked'[upEdge[p]] >= 1 - <6>1. CASE upEdge[p] # e - BY <3>1, <5>4, <6>1 - <6>2. CASE upEdge[p] = e - <7>1. CASE rcvdUnacked[e] > 1 - \* rcvdUnacked'[e] = rcvdUnacked[e] - 1 >= 1. - BY <3>1, <3>3, <5>4, <6>2, <7>1 - <7>2. CASE ~ rcvdUnacked[e] > 1 - \* Then rcvdUnacked[e] = 1 (since rcvdUnacked[e] > 0). - \* From SendAck precondition (since case 2a fails), case 2b - \* must hold: ~active[p] /\ all other rcvdUnacked = 0 /\ all - \* sentUnacked = 0 on OutEdges(p). Combined with - \* rcvdUnacked'[e] = 0, we obtain neutral'(p), contradicting - \* ~neutral'(p). - <8>0. rcvdUnacked[e] = 1 - BY <3>1, <3>3, <7>2 DEF Counters, TypeOK - <8>1. /\ ~active[p] - /\ \A d \in InEdges(p) \ {e} : rcvdUnacked[d] = 0 - /\ \A d \in OutEdges(p) : sentUnacked[d] = 0 - BY <3>1, <6>2, <7>2 - <8>2. rcvdUnacked'[e] = 0 - BY <3>1, <3>3, <8>0 - <8>3. \A d \in InEdges(p) : rcvdUnacked'[d] = 0 - <9>1. SUFFICES ASSUME NEW d \in InEdges(p) - PROVE rcvdUnacked'[d] = 0 - OBVIOUS - <9>2. CASE d = e - BY <8>2, <9>2 - <9>3. CASE d # e - <10>1. rcvdUnacked'[d] = rcvdUnacked[d] - BY <3>1, <9>1, <9>3 DEF InEdges - <10>2. rcvdUnacked[d] = 0 - BY <8>1, <9>1, <9>3 - <10>. QED BY <10>1, <10>2 - <9>. QED BY <9>2, <9>3 - <8>4. \A d \in OutEdges(p) : sentUnacked'[d] = 0 - BY <3>2, <8>1 - <8>5. ~active[p]' - BY <3>2, <8>1 - <8>6. neutral(p)' - BY <8>3, <8>4, <8>5 DEF neutral - <8>. QED BY <8>6, <5>1 - <7>. QED BY <7>1, <7>2 - <6>. QED BY <6>1, <6>2 - <5>. QED BY <4>2, <5>2, <5>4, <5>5 - <4>3. CASE q # p - <5>1. upEdge'[q] = upEdge[q] - BY <3>2, <4>3 - <5>2. InTree(q) - BY <4>1, <5>1 - <5>3. /\ upEdge[q] \in Edges - /\ upEdge[q][2] = q - /\ upEdge[q][1] \in Procs \ {q} - /\ rcvdUnacked[upEdge[q]] >= 1 - BY <5>2 - \* upEdge[q][2] = q and e[2] = p (from <3>3), with q # p, - \* so upEdge[q] # e. Hence rcvdUnacked' is unchanged at upEdge[q]. - <5>4. upEdge[q] # e - BY <3>3, <4>3, <5>3 - <5>5. rcvdUnacked'[upEdge[q]] = rcvdUnacked[upEdge[q]] - BY <3>1, <5>3, <5>4 - <5>. QED BY <5>1, <5>3, <5>5 - <4>. QED BY <4>2, <4>3 - <3>. QED BY <3>5, <3>6 DEF Inv2 - <2>4. ASSUME NEW p \in Procs, RcvMsg(p) - PROVE Inv2' - <3>1. PICK e \in InEdges(p) : - /\ msgs[e] > 0 - /\ msgs' = [msgs EXCEPT ![e] = @ - 1] - /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1] - /\ active' = [active EXCEPT ![p] = TRUE] - /\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e] + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ - 1] + /\ acks' = [acks EXCEPT ![e] = @ + 1] + /\ upEdge' = IF neutral(p)' THEN [upEdge EXCEPT ![p] = NotAnEdge] ELSE upEdge - /\ UNCHANGED <> - BY <2>4 DEF RcvMsg - <3>2. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs - BY <3>1, EdgeFacts DEF InEdges - \* Active'[p] = TRUE, hence ~neutral'(p) (due to active flag). - \* For q # p, neutrality status is unchanged by RcvMsg(p). - <3>3. \A q \in Procs : q # p => (neutral(q) <=> neutral(q)') - BY <3>1, <3>2 DEF neutral, InEdges, OutEdges - <3>4. ~ (neutral(p))' - BY <3>1, <3>2 DEF neutral - <3>5. \A q \in Procs \ {Leader} : ~ neutral(q)' => InTree(q)' - <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, ~ neutral(q)' - PROVE InTree(q)' - OBVIOUS - <4>2. CASE q = p - \* If p was neutral, upEdge' is set to e, so InTree'(p). - \* If p was non-neutral, upEdge' = upEdge and we use the IH. - <5>1. CASE neutral(p) - \* upEdge'[p] = e \in Edges, e \in Procs \X Procs, so e is a - \* 2-tuple, hence e # NotAnEdge = <<>>. - <6>1. upEdge'[p] = e - BY <3>1, <3>2, <5>1 - <6>2. e \in Procs \X Procs - BY <3>2, EdgeFacts - <6>3. e # NotAnEdge - BY <6>2 DEF NotAnEdge - <6>. QED BY <4>2, <6>1, <6>3 - <5>2. CASE ~neutral(p) - <6>1. InTree(p) - BY <5>2, <3>2 - <6>2. upEdge'[p] = upEdge[p] - BY <3>1, <5>2 - <6>. QED BY <4>2, <6>1, <6>2 + /\ UNCHANGED <> + BY <2>5 DEF SendAck + <3>. e \in Edges /\ p # Leader + BY EdgeFacts DEF InEdges + <3>2. ~ neutral(p) + BY <3>1 DEF neutral, InEdges + <3>3. \A q \in Procs \ {p} : neutral(q)' <=> neutral(q) + BY <3>1 DEF neutral, InEdges, OutEdges + <3>4. CASE neutral(p)' + <4>1. ASSUME NEW q \in Procs \ {Leader} + PROVE /\ upEdge'[q] = NotAnEdge => neutral(q)' + /\ upEdge'[q] # NotAnEdge => + /\ upEdge'[q] \in InEdges(q) + /\ rcvdUnacked'[upEdge'[q]] # 0 + <5>1. CASE q = p + BY <3>1, <3>4, <5>1 + <5>2. CASE q # p + BY <3>1, <3>3, <5>2, NotAnEdgeNoEdge DEF TreeInv, InEdges <5>. QED BY <5>1, <5>2 - <4>3. CASE q # p - <5>1. ~neutral(q) - BY <3>3, <4>3, <4>1 - <5>2. InTree(q) + <4>2. rcvdUnacked[e] = 1 + BY <3>1, <3>4 DEF neutral, InEdges + <4>3. e = upEdge[p] + <5>. SUFFICES ASSUME e # upEdge[p] PROVE FALSE + OBVIOUS + <5>1. /\ upEdge[p] \in InEdges(p) + /\ rcvdUnacked[upEdge[p]] # 0 + BY <3>2 DEF TreeInv + <5>2. PICK u \in InEdges(p) : u = upEdge[p] BY <5>1 - <5>3. upEdge'[q] = upEdge[q] + <5>3. rcvdUnacked'[u] # 0 + BY <3>1, <5>1, <5>2 DEF InEdges + <5>. QED BY <3>4, <5>3 DEF neutral + <4>4. ~ \E q \in Procs \ {Leader} : upEdge[q] \in OutEdges(p) + <5>. SUFFICES ASSUME NEW q \in Procs \ {Leader}, upEdge[q] \in OutEdges(p) + PROVE FALSE + OBVIOUS + <5>1. PICK u \in OutEdges(p) : u = upEdge[q] + OBVIOUS + <5>2. /\ u \in InEdges(q) + /\ rcvdUnacked[u] # 0 + BY NotAnEdgeNoEdge, <5>1 DEF TreeInv, OutEdges + <5>3. sentUnacked[u] = rcvdUnacked[u] + acks[u] + msgs[u] + BY <5>2 DEF CountersConsistent, InEdges + <5>4. sentUnacked[u] # 0 + BY <5>2, <5>3 DEF InEdges + <5>. QED BY <3>1, <3>4, <5>4 DEF neutral + <4>5. /\ e \in E + /\ e[2] = p + /\ p \in N + BY <3>2, <4>3 DEF TreeInv, InEdges + <4>6. Successors(T, p) = {} + BY EdgeFacts, <4>4 DEF Successors, OutEdges + <4>7. E' = E \ {e} + <5>1. E' \subseteq E + BY <3>1 + <5>2. ASSUME e \in E' PROVE FALSE + <6>1. PICK q \in Procs \ {Leader} : e = upEdge'[q] /\ e # NotAnEdge + BY <5>2 + <6>2. q # p /\ e = upEdge[q] + BY <3>1, <3>4, <6>1 + <6>3. e \in InEdges(q) + BY <6>1, <6>2 DEF TreeInv + <6>. QED BY <6>2, <6>3 DEF InEdges + <5>3. (E \ {e}) \subseteq E' BY <3>1, <4>3 - <5>. QED BY <5>2, <5>3 - <4>. QED BY <4>2, <4>3 - <3>6. \A q \in Procs \ {Leader} : - InTree(q)' => - /\ upEdge'[q] \in Edges - /\ upEdge'[q][2] = q - /\ upEdge'[q][1] \in Procs \ {q} - /\ rcvdUnacked'[upEdge'[q]] >= 1 - <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, InTree(q)' - PROVE /\ upEdge'[q] \in Edges - /\ upEdge'[q][2] = q - /\ upEdge'[q][1] \in Procs \ {q} - /\ rcvdUnacked'[upEdge'[q]] >= 1 - OBVIOUS - <4>2. CASE q = p - <5>1. CASE neutral(p) - \* upEdge'[p] = e, e[2] = p, e \in Edges, e[1] \in Procs \ {p}. - \* rcvdUnacked'[e] = rcvdUnacked[e] + 1 >= 1. - BY <3>1, <3>2, <4>2, <5>1 - <5>2. CASE ~neutral(p) - \* upEdge'[p] = upEdge[p], use IH for p. - <6>1. InTree(p) - BY <5>2, <3>2 - <6>2. upEdge'[p] = upEdge[p] - BY <3>1, <5>2 - <6>3. /\ upEdge[p] \in Edges - /\ upEdge[p][2] = p - /\ upEdge[p][1] \in Procs \ {p} - /\ rcvdUnacked[upEdge[p]] >= 1 - BY <6>1, <3>2 - \* Either upEdge[p] = e (then rcvdUnacked' = rcvdUnacked+1 >= 2) - \* or upEdge[p] # e (then rcvdUnacked'[upEdge[p]] = rcvdUnacked[upEdge[p]]). - <6>4. rcvdUnacked'[upEdge[p]] >= 1 - BY <3>1, <6>3 - <6>. QED BY <4>2, <6>2, <6>3, <6>4 + <5>. QED BY <5>1, <5>2, <5>3 + <4>8. N' = N \ {p} + <5>1. N' \subseteq N + BY <3>1 + <5>2. p \notin N' + BY <3>1, <3>4, <4>4 DEF OutEdges + <5>3. (N \ {p}) \subseteq N' + BY <3>1 + <5>. QED BY <5>1, <5>2, <5>3 + <4>. HIDE DEF N, E + <4>9. IsTreeWithRoot(O', Leader) + BY <1>1, EdgeFacts, RemoveLeafFromTransposedTree, <2>1, <2>2, <4>5, <4>6, <4>7, <4>8, SMTT(10) + DEF TreeInv + <4>11. TreeWithRoot' + BY <1>1, <1>2, <2>3, <3>3, <4>9, <4>8, Zenon DEF TreeInv + <4>. QED BY <4>1, <4>11 DEF TreeInv + <3>5. CASE ~ neutral(p)' + <4>1. UNCHANGED <> + BY <3>1, <3>5 + <4>2. ASSUME NEW q \in Procs \ {Leader}, upEdge[q] # NotAnEdge + PROVE (rcvdUnacked[upEdge[q]] = 0) <=> (rcvdUnacked'[upEdge[q]] = 0) + <5>1. CASE q = p + BY <3>1, <3>5, <4>2, <5>1 DEF neutral, InEdges, OutEdges + <5>2. CASE q # p + BY <3>1, <4>2, <5>2 DEF TreeInv, InEdges <5>. QED BY <5>1, <5>2 - <4>3. CASE q # p - \* upEdge'[q] = upEdge[q]. Neutrality of q unchanged. - <5>1. upEdge'[q] = upEdge[q] - BY <3>1, <4>3 - <5>2. InTree(q) - BY <4>1, <5>1 - <5>3. /\ upEdge[q] \in Edges - /\ upEdge[q][2] = q - /\ upEdge[q][1] \in Procs \ {q} - /\ rcvdUnacked[upEdge[q]] >= 1 - BY <5>2 - \* upEdge[q][2] = q and e[2] = p, with q # p, so upEdge[q] # e. - <5>4. upEdge[q] # e - BY <3>2, <4>3, <5>3 - <5>5. rcvdUnacked'[upEdge[q]] = rcvdUnacked[upEdge[q]] - BY <3>1, <5>3, <5>4 - <5>. QED BY <5>1, <5>3, <5>5 - <4>. QED BY <4>2, <4>3 - <3>. QED BY <3>5, <3>6 DEF Inv2 - <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next -<1>. QED BY <1>1, <1>2, Inv1Inductive, PTL DEF Spec - ------------------------------------------------------------------------------ -(***************************************************************************) -(* Inductiveness of the auxiliary acyclicity invariant NoCycle (defined *) -(* alongside Inv2 above). The proof depends on Inv2 (in particular *) -(* Counters and conjunct 4) for the RcvMsg case. *) -(***************************************************************************) -LEMMA NoCycleInit == Init => NoCycle - <1>. SUFFICES ASSUME Init, - NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q) /\ upEdge[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <1>1. PICK q \in S : TRUE - OBVIOUS - <1>2. q \in Procs \ {Leader} - OBVIOUS - <1>3. upEdge[q] = NotAnEdge - BY <1>2 DEF Init - <1>4. ~ InTree(q) - BY <1>3 DEF InTree - <1>. QED BY <1>1, <1>4 - -LEMMA NoCycleStep == Inv1 /\ Inv2 /\ NoCycle /\ [Next]_vars => NoCycle' - <1>. SUFFICES ASSUME Inv1, Inv2, NoCycle, [Next]_vars - PROVE NoCycle' - OBVIOUS - <1>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge - <1>1. ASSUME NEW p \in Procs, SendMsg(p) - PROVE NoCycle' - <2>1. upEdge' = upEdge - BY <1>1 DEF SendMsg - <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <2>. QED BY <2>1 DEF NoCycle - <1>2. ASSUME NEW p \in Procs, RcvAck(p) - PROVE NoCycle' - <2>1. upEdge' = upEdge - BY <1>2 DEF RcvAck - <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <2>. QED BY <2>1 DEF NoCycle - <1>3. ASSUME NEW p \in Procs, Idle(p) - PROVE NoCycle' - <2>1. upEdge' = upEdge - BY <1>3 DEF Idle - <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <2>. QED BY <2>1 DEF NoCycle - <1>4. CASE UNCHANGED vars - <2>1. upEdge' = upEdge - BY <1>4 DEF vars - <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <2>. QED BY <2>1 DEF NoCycle - <1>5. ASSUME NEW p \in Procs, SendAck(p) - PROVE NoCycle' - <2>0. PICK e \in InEdges(p) : - /\ rcvdUnacked[e] > 0 - /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ - 1] - /\ acks' = [acks EXCEPT ![e] = @ + 1] - BY <1>5 DEF SendAck - <2>1. upEdge' = IF neutral(p)' THEN [upEdge EXCEPT ![p] = NotAnEdge] - ELSE upEdge - BY <1>5 DEF SendAck - <2>2. p # Leader - <3>1. SUFFICES ASSUME p = Leader PROVE FALSE - OBVIOUS - <3>2. e \in InEdges(Leader) - BY <2>0, <3>1 - <3>3. InEdges(Leader) = {} - BY EdgeFacts - <3>. QED BY <3>2, <3>3 - <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <2>case1. CASE ~ neutral(p)' - <3>1. upEdge' = upEdge - BY <2>1, <2>case1 - <3>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S - BY <3>1 - <3>. QED BY <3>2 DEF NoCycle - <2>case2. CASE neutral(p)' - <3>1. upEdge' = [upEdge EXCEPT ![p] = NotAnEdge] - BY <2>1, <2>case2 - <3>2. p \in DOMAIN upEdge - BY <2>2 - <3>3. upEdge'[p] = NotAnEdge - BY <3>1, <3>2 - <3>4. ~ InTree(p)' - BY <3>3 - <3>5. p \notin S - BY <3>4 - <3>6. \A q \in S : q # p - BY <3>5 - <3>7. \A q \in S : upEdge'[q] = upEdge[q] - BY <3>1, <3>6 - <3>8. \A q \in S : InTree(q) /\ upEdge[q][1] \in S - BY <3>7 - <3>. QED BY <3>8 DEF NoCycle - <2>. QED BY <2>case1, <2>case2 - <1>6. ASSUME NEW p \in Procs, RcvMsg(p) - PROVE NoCycle' - <2>0. PICK e \in InEdges(p) : - /\ msgs[e] > 0 - /\ msgs' = [msgs EXCEPT ![e] = @ - 1] - /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1] - /\ active' = [active EXCEPT ![p] = TRUE] - /\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e] - ELSE upEdge - /\ UNCHANGED <> - BY <1>6 DEF RcvMsg - <2>1. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs - BY <2>0, EdgeFacts DEF InEdges - <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), - S # {}, - \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S - PROVE FALSE - BY DEF NoCycle - <2>case1. CASE ~ neutral(p) - <3>1. upEdge' = upEdge - BY <2>0, <2>case1 - <3>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S - BY <3>1 - <3>. QED BY <3>2 DEF NoCycle - <2>case2. CASE neutral(p) - <3>1. upEdge' = [upEdge EXCEPT ![p] = e] - BY <2>0, <2>case2 - <3>2. p \in DOMAIN upEdge - BY <2>1 - <3>caseA. CASE p \notin S - <4>1. \A q \in S : q # p - BY <3>caseA - <4>2. \A q \in S : upEdge'[q] = upEdge[q] - BY <3>1, <4>1 - <4>3. \A q \in S : InTree(q) /\ upEdge[q][1] \in S - BY <4>2 - <4>. QED BY <4>3 DEF NoCycle - <3>caseB. CASE p \in S - <4>0. upEdge'[p] = e - BY <3>1, <3>2 - <4>1. upEdge'[p][1] = e[1] - BY <4>0 - <4>2. e[1] \in S - BY <3>caseB, <4>1 - <4>3. e[1] # p - BY <2>1 - <4>4. e[1] \in S \ {p} - BY <4>2, <4>3 - <4>5. SUFFICES ASSUME NEW q \in S \ {p} - PROVE InTree(q) /\ upEdge[q][1] \in (S \ {p}) - BY <4>4 DEF NoCycle - <4>9. q \in S /\ q # p /\ q \in Procs \ {Leader} - OBVIOUS - <4>11. upEdge'[q] = upEdge[q] - BY <3>1, <4>9 - <4>12. InTree(q) - BY <4>9, <4>11 - <4>13. upEdge[q][1] \in S - BY <4>9, <4>11 - <4>14. /\ upEdge[q] \in Edges - /\ upEdge[q][2] = q - /\ upEdge[q][1] \in Procs \ {q} - /\ rcvdUnacked[upEdge[q]] >= 1 - BY <4>9, <4>12 - <4>15. sentUnacked[upEdge[q]] >= 1 - BY <4>14 - <4>16. upEdge[q][1] # p - <5>1. SUFFICES ASSUME upEdge[q][1] = p PROVE FALSE - OBVIOUS - <5>2. upEdge[q] \in OutEdges(p) - BY <5>1, <4>14 DEF OutEdges - <5>3. sentUnacked[upEdge[q]] = 0 - BY <2>case2, <5>2 DEF neutral - <5>. QED BY <4>15, <5>3 - <4>17. upEdge[q][1] \in (S \ {p}) - BY <4>13, <4>16 - <4>. QED BY <4>12, <4>17 - <3>. QED BY <3>caseA, <3>caseB - <2>. QED BY <2>case1, <2>case2 - <1>. QED - BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6 DEF Next - -LEMMA NoCycleInductive == Spec => []NoCycle - <1>1. Init => NoCycle - BY NoCycleInit - <1>2. Inv1 /\ Inv2 /\ NoCycle /\ [Next]_vars => NoCycle' - BY NoCycleStep - <1>3. Spec => []Inv2 - BY Inv2Inductive - <1>4. Spec => []Inv1 - BY Inv1Inductive - <1>. QED - BY <1>1, <1>2, <1>3, <1>4, PTL DEF Spec - -(***************************************************************************) -(* Discharge of DT1FromInv2 using Inv2 and the acyclicity invariant. *) -(***************************************************************************) -LEMMA DT1FromInv2 == Inv1 /\ Inv2 /\ NoCycle => DT1Inv - <1>. SUFFICES ASSUME Inv1, Inv2, NoCycle PROVE DT1Inv - OBVIOUS - <1>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge - <1>. SUFFICES ASSUME neutral(Leader), - NEW p0 \in Procs \ {Leader} - PROVE neutral(p0) - BY DEF DT1Inv - <1>contra. ASSUME ~ neutral(p0) PROVE FALSE - <2>. DEFINE S == {q \in Procs \ {Leader} : ~ neutral(q)} - <2>4. S # {} - BY <1>contra DEF S - <2>5. S \in SUBSET (Procs \ {Leader}) - BY DEF S - <2>6. SUFFICES ASSUME NEW q \in S - PROVE InTree(q) /\ upEdge[q][1] \in S - BY <2>4, <2>5 DEF NoCycle - <2>8. q \in Procs \ {Leader} /\ ~ neutral(q) - BY DEF S - <2>9. InTree(q) - BY <2>8 - <2>10. /\ upEdge[q] \in Edges - /\ upEdge[q][2] = q - /\ upEdge[q][1] \in Procs \ {q} - /\ rcvdUnacked[upEdge[q]] >= 1 - BY <2>8, <2>9 - <2>11. sentUnacked[upEdge[q]] >= 1 - BY <2>10 - <2>12. upEdge[q] \in OutEdges(upEdge[q][1]) - BY <2>10 DEF OutEdges - <2>13. ~ neutral(upEdge[q][1]) - BY <2>11, <2>12 DEF neutral - <2>16. upEdge[q][1] \in S - BY <2>10, <2>13 DEF S - <2>. QED BY <2>9, <2>16 - <1>. QED BY <1>contra - -THEOREM Thm_DT1Inv == Spec => []DT1Inv - <1>0. Spec => []Inv1 - BY Inv1Inductive - <1>1. Spec => []Inv2 - BY Inv2Inductive - <1>2. Spec => []NoCycle - BY NoCycleInductive - <1>3. Inv1 /\ Inv2 /\ NoCycle => DT1Inv - BY DT1FromInv2 - <1>. QED - BY <1>0, <1>1, <1>2, <1>3, PTL + <4>. HIDE DEF N, O + <4>. QED BY <1>1, <1>2, <2>3, <3>2, <3>3, <3>5, <4>1, <4>2 DEF TreeInv + <3>. QED BY <3>4, <3>5 + <2>6. ASSUME NEW p \in Procs, RcvMsg(p) PROVE TreeInv' + <3>1. PICK e \in InEdges(p) : + /\ msgs[e] > 0 + /\ msgs' = [msgs EXCEPT ![e] = @ - 1] + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1] + /\ active' = [active EXCEPT ![p] = TRUE] + /\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e] + ELSE upEdge + /\ UNCHANGED <> + BY <2>6 DEF RcvMsg + <3>. e \in Edges /\ p # Leader + BY EdgeFacts DEF InEdges + <3>2. ~ neutral(p)' + BY <3>1 DEF neutral + <3>3. \A q \in Procs \ {p} : neutral(q)' <=> neutral(q) + BY <3>1 DEF neutral, InEdges + <3>4. CASE neutral(p) + <4>1. ASSUME NEW q \in Procs \ {Leader} + PROVE upEdge'[q] = NotAnEdge => neutral(q)' + BY NotAnEdgeNoEdge, <3>1, <3>3, <3>4 DEF TreeInv + <4>2. ASSUME NEW q \in Procs \ {Leader}, upEdge'[q] # NotAnEdge + PROVE /\ upEdge'[q] \in InEdges(q) + /\ rcvdUnacked'[upEdge'[q]] # 0 + BY <3>1, <3>4, <4>2 DEF TreeInv, InEdges + <4>3. p \notin N + BY <1>1, <3>4 DEF TreeInv + <4>4. e[1] \in N + <5>. e[1] \in Procs + BY EdgeFacts + <5>1. e \in OutEdges(e[1]) /\ sentUnacked[e] # 0 + BY <3>1 DEF CountersConsistent, OutEdges + <5>2. ~ neutral(e[1]) + BY <5>1 DEF neutral + <5>. QED BY <5>2 DEF TreeInv + <4>5. E' = E \cup {e} + BY NotAnEdgeNoEdge, <3>1, <3>4, <4>3 + <4>6. N' = N \cup {p} + BY <4>5 DEF InEdges + <4>. HIDE DEF N, E + <4>7. IsTreeWithRoot(O', Leader) + BY EdgeFacts, <1>1, AddLeafToTransposedTree, <2>2, <4>3, <4>4, <4>5, <4>6, SMTT(10) + DEF TreeInv, InEdges + <4>8. \A n \in N' \ {Leader} : ~ neutral(n)' + BY <1>1, <2>3, <3>2, <3>3, <4>6 DEF TreeInv + <4>. QED BY <1>2, <4>1, <4>2, <4>7, <4>8, Zenon DEF TreeInv + <3>5. CASE ~ neutral(p) + <4>1. UNCHANGED <> + BY <3>1, <3>5 + <4>. HIDE DEF O + <4>2. TreeWithRoot' + BY <1>1, <1>2, <2>3, <3>2, <3>3, <3>5, <4>1, Zenon DEF TreeInv + <4>. QED BY <4>2, <3>1, <3>2, <3>3, <3>5, <4>1 DEF TreeInv + <3>. QED BY <3>4, <3>5 + <2>7. ASSUME NEW p \in Procs, RcvAck(p) PROVE TreeInv' + <3>1. UNCHANGED <> + BY <2>7 DEF RcvAck + <3>2. ASSUME NEW q \in Procs \ {Leader} + PROVE neutral(q)' <=> neutral(q) + <4>1. CASE q = p + <5>1. ~ neutral(p) + BY <2>7 DEF RcvAck, neutral, CountersConsistent, OutEdges + <5>2. /\ upEdge[p] \in InEdges(p) + /\ rcvdUnacked[upEdge[p]] # 0 + BY <4>1, <5>1 DEF TreeInv + <5>. QED BY <3>1, <4>1, <5>1, <5>2 DEF neutral + <4>2. CASE q # p + BY <2>7, <4>2 DEF RcvAck, neutral, InEdges, OutEdges + <4>. QED BY <4>1, <4>2 + <3>. HIDE DEF N, O + <3>. QED BY <1>1, <1>2, <2>3, <3>1, <3>2 DEF TreeInv + <2>8. ASSUME NEW p \in Procs, Idle(p) PROVE TreeInv' + <3>1. UNCHANGED <> + BY <2>8 DEF Idle + <3>2. ASSUME NEW q \in Procs \ {Leader} + PROVE neutral(q)' <=> neutral(q) + <4>1. CASE q = p + <5>1. ~ neutral(p) + BY <2>8 DEF Idle, neutral + <5>2. /\ upEdge[p] \in InEdges(p) + /\ rcvdUnacked[upEdge[p]] # 0 + BY <4>1, <5>1 DEF TreeInv + <5>. QED BY <3>1, <4>1, <5>1, <5>2 DEF neutral + <4>2. CASE q # p + BY <2>8, <4>2 DEF Idle, neutral, InEdges, OutEdges + <4>. QED BY <4>1, <4>2 + <3>. QED BY <1>1, <1>2, <2>3, <3>1, <3>2 DEF TreeInv + <2>9. CASE UNCHANGED vars + BY <2>9 DEF vars, TreeInv, TreeWithRoot, neutral, InEdges, OutEdges + <2>. QED BY <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next +<1>. QED BY <1>3, <1>4, Invariant1, PTL DEF Spec ----------------------------------------------------------------------------- (***************************************************************************) -(* Theorem 2: Spec => TreeWithRoot *) -(* *) -(* The set E of upEdges (excluding NotAnEdge), with N the set of nodes *) -(* appearing in those edges, forms (when transposed) a tree rooted at *) -(* the leader, and every node of that tree is non-neutral. *) -(* *) -(* The structural invariants Inv2 + NoCycle proven above already capture *) -(* the tree shape; what's left is to relate them to the *) -(* IsTreeWithRoot/AreConnectedIn predicates from the community-modules *) -(* Graphs module. For the connectivity part, we construct a simple path *) -(* from each node to the leader by iterating upEdge. *) -(***************************************************************************) -G == INSTANCE Graphs - -(***************************************************************************) -(* Concrete in-tree structure (the transposed overlay tree). *) -(***************************************************************************) -EE == {upEdge[p] : p \in DOMAIN upEdge} \ {NotAnEdge} -NN == {e[1] : e \in EE} \cup {e[2] : e \in EE} -OO == G!Transpose([edge |-> EE, node |-> NN]) - -(***************************************************************************) -(* Both endpoints of every E-edge are non-neutral. Children are *) -(* non-neutral by Inv2 (InTree implies they are in the tree, hence *) -(* non-neutral); parents are non-neutral because the tree edge has *) -(* rcvdUnacked >= 1, so by Counters sentUnacked >= 1 and the parent *) -(* fails the neutral predicate. *) -(***************************************************************************) -LEMMA TreeNodesNonNeutral == - ASSUME Inv1, Inv2 - PROVE \A n \in NN : ~ neutral(n) - <1>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge, NN, EE - <1>. SUFFICES ASSUME NEW n \in NN - PROVE ~ neutral(n) - OBVIOUS - <1>1. PICK e \in EE : n = e[1] \/ n = e[2] - OBVIOUS - <1>2. PICK p \in DOMAIN upEdge : upEdge[p] = e /\ e # NotAnEdge - OBVIOUS - <1>3. p \in Procs \ {Leader} - OBVIOUS - <1>4. InTree(p) - BY <1>2 - <1>5. /\ upEdge[p] \in Edges - /\ upEdge[p][2] = p - /\ upEdge[p][1] \in Procs \ {p} - /\ rcvdUnacked[upEdge[p]] >= 1 - BY <1>3, <1>4 - <1>6. e \in Edges /\ e[2] = p /\ e[1] \in Procs \ {p} - BY <1>2, <1>5 - <1>7. rcvdUnacked[e] >= 1 - BY <1>2, <1>5 - <1>8. sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e] - BY <1>6 - <1>9. sentUnacked[e] >= 1 - BY <1>7, <1>8 - <1>10. e \in OutEdges(e[1]) /\ e \in InEdges(e[2]) - BY <1>6 DEF OutEdges, InEdges - <1>11. ~ neutral(e[1]) - BY <1>9, <1>10 DEF neutral - <1>12. ~ neutral(e[2]) - BY <1>7, <1>10 DEF neutral - <1>. QED BY <1>1, <1>11, <1>12 - -(***************************************************************************) -(* Tree-structural facts about OO derived from Inv2. *) -(***************************************************************************) -LEMMA TreeStructure == - ASSUME Inv1, Inv2 - PROVE /\ OO.edge \subseteq NN \X NN - /\ OO.node = NN - /\ \A e \in OO.edge : e[1] # Leader - /\ \A e \in OO.edge : - \A f \in OO.edge : (e[1] = f[1]) => (e = f) - <1>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge, - EE, NN, OO, G!Transpose - <1>1. OO.edge \subseteq NN \X NN - \* Each OO-edge is <> for some e \in EE. For e \in EE, - \* e[1] \in NN and e[2] \in NN (definition of NN). - <2>. SUFFICES ASSUME NEW oe \in OO.edge - PROVE oe \in NN \X NN - OBVIOUS - <2>1. PICK e \in EE : oe = <> - OBVIOUS - <2>2. PICK p \in DOMAIN upEdge : upEdge[p] = e /\ e # NotAnEdge - OBVIOUS - <2>3. e \in Edges /\ e \in Procs \X Procs - BY <2>2, EdgeFacts - <2>4. e[1] \in NN /\ e[2] \in NN - BY <2>1 - <2>. QED BY <2>1, <2>4 - <1>2. OO.node = NN - OBVIOUS - <1>3. \A oe \in OO.edge : oe[1] # Leader - \* OO.edge entries are <> for e \in EE. e[2] = p (some - \* non-leader process from DOMAIN upEdge). - <2>. SUFFICES ASSUME NEW oe \in OO.edge - PROVE oe[1] # Leader - OBVIOUS - <2>1. PICK e \in EE : oe = <> - OBVIOUS - <2>2. PICK p \in DOMAIN upEdge : upEdge[p] = e /\ e # NotAnEdge - OBVIOUS - <2>3. p \in Procs \ {Leader} - OBVIOUS - <2>4. InTree(p) - BY <2>2 - <2>5. e[2] = p - BY <2>2, <2>3, <2>4 - <2>6. oe[1] = e[2] - BY <2>1 - <2>. QED BY <2>3, <2>5, <2>6 - <1>4. \A oe \in OO.edge : - \A of \in OO.edge : (oe[1] = of[1]) => (oe = of) - \* If two OO-edges share a source (= original target = the child), - \* then they correspond to the same upEdge[p] for the same p. - <2>. SUFFICES ASSUME NEW oe \in OO.edge, NEW of \in OO.edge, - oe[1] = of[1] - PROVE oe = of - OBVIOUS - <2>1. PICK e1 \in EE : oe = <> - OBVIOUS - <2>2. PICK e2 \in EE : of = <> - OBVIOUS - <2>3. PICK p1 \in DOMAIN upEdge : upEdge[p1] = e1 /\ e1 # NotAnEdge - OBVIOUS - <2>4. PICK p2 \in DOMAIN upEdge : upEdge[p2] = e2 /\ e2 # NotAnEdge - OBVIOUS - <2>5. p1 \in Procs \ {Leader} /\ p2 \in Procs \ {Leader} - OBVIOUS - <2>6. InTree(p1) /\ InTree(p2) - BY <2>3, <2>4 - <2>7. e1[2] = p1 /\ e2[2] = p2 - BY <2>5, <2>6, <2>3, <2>4 - <2>8. oe[1] = p1 /\ of[1] = p2 - BY <2>1, <2>2, <2>7 - <2>9. p1 = p2 - BY <2>8 - <2>10. e1 = e2 - BY <2>3, <2>4, <2>9 - <2>. QED BY <2>1, <2>2, <2>10 - <1>. QED BY <1>1, <1>2, <1>3, <1>4 - -(***************************************************************************) -(* The connectivity part of IsTreeWithRoot says every node has a path to *) -(* the root. We construct that path by iterating upEdge. This requires *) -(* SimplePath / Cardinality reasoning which is delicate; we leave the *) -(* concrete path-construction OMITTED and discharge the rest of *) -(* IsTreeWithRoot from TreeStructure. *) -(* *) -(* AreConnectedIn(n, Leader, OO) follows from the chain *) -(* n -> upEdge[n][1] -> upEdge[upEdge[n][1]][1] -> ... -> Leader *) -(* which terminates by NoCycle + Procs finite. *) +(* We can now prove the main safety property of the algorithm, expressed *) +(* as DT1Inv, as a consequence of the preceding invariants. *) (***************************************************************************) -LEMMA AreConnectedToLeader == - ASSUME Inv1, Inv2, NoCycle, NEW n \in OO.node - PROVE G!AreConnectedIn(n, Leader, OO) - OMITTED - -LEMMA TreeIsTree == - ASSUME Inv1, Inv2, NoCycle, OO.edge # {} - PROVE G!IsTreeWithRoot(OO, Leader) - <1>. USE DEF G!IsTreeWithRoot, G!IsDirectedGraph, OO, G!Transpose - <1>1. OO = [node |-> OO.node, edge |-> OO.edge] - BY DEF OO, G!Transpose - <1>2. OO.edge \subseteq OO.node \X OO.node - BY TreeStructure DEF OO, G!Transpose - <1>3. \A e \in OO.edge : /\ e[1] # Leader - /\ \A f \in OO.edge : - (e[1] = f[1]) => (e = f) - BY TreeStructure - <1>4. \A nn \in OO.node : G!AreConnectedIn(nn, Leader, OO) - BY AreConnectedToLeader - <1>. QED BY <1>1, <1>2, <1>3, <1>4 - -(***************************************************************************) -(* The body of TreeWithRoot (under []), with module-level OO/NN/EE. *) -(***************************************************************************) -TreeBody == - /\ OO.edge # {} => G!IsTreeWithRoot(OO, Leader) - /\ \A n \in OO.node: ~neutral(n) - -(***************************************************************************) -(* The structural pieces above (TreeNodesNonNeutral / TreeStructure / *) -(* TreeIsTree) discharge most of TreeWithRoot. The QED below would close *) -(* the proof; it requires: *) -(* (a) AreConnectedToLeader (OMITTED above) -- the SimplePath / Cardinal- *) -(* ity / SeqOf reasoning to construct a path from any node to the *) -(* leader by iterating upEdge. *) -(* (b) Bridging the syntactic gap between TreeWithRoot's `LET ... IN []` *) -(* shape and our `[]TreeBody` form. The two are semantically equal *) -(* because LET is just substitution, but TLAPS' temporal backend *) -(* currently does not unify them. *) -(***************************************************************************) -LEMMA Inv2GivesTreeBody == Inv1 /\ Inv2 /\ NoCycle => TreeBody - <1>. SUFFICES ASSUME Inv1, Inv2, NoCycle PROVE TreeBody - OBVIOUS - <1>1. OO.edge # {} => G!IsTreeWithRoot(OO, Leader) - BY TreeIsTree - <1>2. \A n \in OO.node : ~ neutral(n) - <2>1. OO.node = NN - BY TreeStructure - <2>. QED BY <2>1, TreeNodesNonNeutral - <1>. QED BY <1>1, <1>2 DEF TreeBody - -LEMMA SpecGivesAlwaysTreeBody == Spec => [] TreeBody - <1>1. Spec => []Inv1 - BY Inv1Inductive - <1>2. Spec => []Inv2 - BY Inv2Inductive - <1>3. Spec => []NoCycle - BY NoCycleInductive - <1>. QED BY <1>1, <1>2, <1>3, Inv2GivesTreeBody, PTL - -THEOREM Thm_TreeWithRoot == Spec => TreeWithRoot -OMITTED +THEOREM Safety == Spec => []DT1Inv +<1>1. Inv1 /\ TreeInv => DT1Inv + <2>. DEFINE S == {p \in Procs \ {Leader} : ~ neutral(p)} + <2>. SUFFICES ASSUME TypeOK, CountersConsistent, TreeInv, neutral(Leader), S # {} + PROVE FALSE + BY DEF Inv1, DT1Inv + <2>. USE DEF TypeOK + <2>. DEFINE E == {upEdge[p] : p \in DOMAIN upEdge} \ {NotAnEdge} + N == {e[2] : e \in E} \cup {Leader} + T == [node |-> N, edge |-> E] + O == Transpose(T) + <2>1. IsTreeWithRoot(O, Leader) + BY DEF TreeInv, TreeWithRoot + <2>2. O.node = N + BY DEF Transpose + <2>3. S \subseteq N + BY DEF TreeInv + <2>4. PICK q \in S : \A e \in O.edge : e[1] = q => e[2] \notin S + <3>. HIDE DEF N, O, S + <3>. QED BY TreeAcyclic, <2>1, <2>2, <2>3, Zenon + <2>. DEFINE e == upEdge[q] parent == e[1] + <2>5. /\ e # NotAnEdge + /\ e \in InEdges(q) + /\ rcvdUnacked[e] # 0 + BY DEF TreeInv + <2>6. /\ e \in OutEdges(parent) + /\ e = <> + BY EdgeFacts, <2>5 DEF InEdges, OutEdges + <2>7. sentUnacked[e] # 0 + BY <2>5 DEF CountersConsistent, InEdges + <2>8. ~ neutral(parent) + BY <2>6, <2>7 DEF neutral + <2>9. parent \in S + BY EdgeFacts, <2>5, <2>8 + <2>10. <> \in O.edge + BY <2>5, <2>6 DEF Transpose + <2>. HIDE DEF O, S + <2>. QED BY <2>4, <2>9, <2>10 +<1>. QED BY <1>1, Invariant1, TreeInvariant, PTL ----------------------------------------------------------------------------- (***************************************************************************) -(* Theorem 4: Spec => DT2 (liveness) *) -(* *) -(* Liveness: Terminated ~> neutral(Leader). *) -(* *) -(* Once the computation has globally terminated, the WF_vars(Next) *) -(* fairness assumption guarantees progress on each remaining *) -(* RcvMsg/SendAck/RcvAck step until all counters drain to 0 and the *) -(* leader becomes neutral. A multiset/well-founded measure on *) -(* (msgs, rcvdUnacked, acks, sentUnacked) is needed; left as future work. *) +(* The proof of the liveness property DT2 is left for future work. *) (***************************************************************************) -THEOREM Thm_DT2 == Spec => DT2 -OMITTED ============================================================================= diff --git a/specifications/ewd687a/MCEWD687a.cfg b/specifications/ewd687a/MCEWD687a.cfg index ffe26374..7b7adbbf 100644 --- a/specifications/ewd687a/MCEWD687a.cfg +++ b/specifications/ewd687a/MCEWD687a.cfg @@ -1,45 +1,25 @@ -\* MV CONSTANT declarations CONSTANTS + \* model values for processes L = L P1 = P1 P2 = P2 P3 = P3 -\* MV CONSTANT definitions + MaxCounter = 3 + Leader = L + Procs <- MCProcs + Edges <- MCEdges -CONSTANT - Procs <- const_1633116534008310000 -\* CONSTANT definitions +CONSTRAINT StateConstraint -CONSTANT - Edges <- const_1633116534008311000 -\* CONSTANT definitions +SPECIFICATION Spec -CONSTANT - Leader <- const_1633116534008312000 +CHECK_DEADLOCK FALSE -\* CONSTRAINT definition -CONSTRAINT - constr_1633116534008313000 - -\* SPECIFICATION definition -SPECIFICATION - Spec - -CHECK_DEADLOCK - FALSE - -\* INVARIANT definition -INVARIANT +INVARIANTS TypeOK + CountersConsistent + TreeWithRoot DT1Inv -\* PROPERTY definition PROPERTY DT2 - -PROPERTIES - CountersConsistent - TreeWithRoot - \* StableUpEdge - -\* Generated on Fri Oct 01 12:28:54 PDT 2021 \ No newline at end of file diff --git a/specifications/ewd687a/MCEWD687a.tla b/specifications/ewd687a/MCEWD687a.tla index bd482df9..73f6c9da 100644 --- a/specifications/ewd687a/MCEWD687a.tla +++ b/specifications/ewd687a/MCEWD687a.tla @@ -1,29 +1,19 @@ ---- MODULE MCEWD687a ---- EXTENDS EWD687a, TLC -\* MV CONSTANT declarations@modelParameterConstants -CONSTANTS -L, P1, P2, P3 ----- +CONSTANTS + L, P1, P2, P3, \* constants representing the processes in the MC instance + MaxCounter \* bound on counter values -\* MV CONSTANT definitions Procs -const_1633116534008310000 == -{L, P1, P2, P3} ----- +MCProcs == {L, P1, P2, P3} +MCEdges == + {<>, <>, <>, <>, <>} -\* CONSTANT definitions @modelParameterConstants:1Edges -const_1633116534008311000 == -{<>, <>, <>, <>, <>} ----- - -\* CONSTANT definitions @modelParameterConstants:2Leader -const_1633116534008312000 == -L ----- - -\* CONSTRAINT definition @modelParameterContraint:0 -constr_1633116534008313000 == -\A e \in Edges : msgs[e] < 3 /\ acks[e] < 3 /\ sentUnacked[e] < 3 /\ rcvdUnacked[e] < 3 +StateConstraint == \A e \in Edges : + /\ msgs[e] < MaxCounter + /\ acks[e] < MaxCounter + /\ sentUnacked[e] < MaxCounter + /\ rcvdUnacked[e] < MaxCounter ============================================================================= \* Modification History