search

heidihoward / pbft-tlaplus

Formal specification of PBFT in TLA+
MIT License
7 stars 1 forks source link

Inductive invariant validation with Apalache and TLC #5

Closed lemmy closed 1 month ago

lemmy commented 2 months ago

Note the use of Apalache's Gen operator in the first link.

Ordinary invariant checking TypeOK and SafetyInv of Spec and SpecByz

TLC

lemmy commented 2 months ago

Apalache finds a violation of SafetyInv, i.e., OneReplyInv under byzantine behavior (SpecByz) after 4 steps:

$ tlc -note -config violation1.tla violation1.tla

---------------------------- MODULE violation1 ----------------------------

EXTENDS APApbft, TLC

SetAsFun(__S) ==
    LET __Dom == { __x: <<__x, __y>> \in __S }
        __Rng == { __y: <<__x, __y>> \in __S }
    IN
    [ __x \in __Dom |-> CHOOSE __y \in __Rng: <<__x, __y>> \in __S ]

(* Initial state *)
State0 ==
  ByzR = { 0, 1, 2, 3 }
    /\ Checkpoints = {2}
    /\ R = { 0, 1, 2, 3 }
    /\ mlogs
      = SetAsFun({ <<
          0, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          1, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          2, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          3, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >> })
    /\ msgs
      = [checkpoint |-> {},
        commit |-> {},
        newview |-> {},
        prepare |-> {},
        preprepare |-> {},
        reply |-> {},
        request |-> { [t |-> 1], [t |-> 2], [t |-> 3] },
        viewchange |-> {}]
    /\ sCheckpoint = SetAsFun({ <<0, {}>>, <<1, {}>>, <<2, {}>>, <<3, {}>> })
    /\ states = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ vChange
      = SetAsFun({ <<0, FALSE>>, <<1, FALSE>>, <<2, FALSE>>, <<3, FALSE>> })
    /\ views = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ TRUE

(* Transition 15 to State1 *)
State1 ==
  ByzR = { 0, 1, 2, 3 }
    /\ Checkpoints = {2}
    /\ R = { 0, 1, 2, 3 }
    /\ mlogs
      = SetAsFun({ <<
          0, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          1, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          2, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          3, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >> })
    /\ msgs
      = [checkpoint |-> {},
        commit |-> {},
        newview |-> {},
        prepare |-> {},
        preprepare |-> {},
        reply |-> {[i |-> 2, r |-> 1, t |-> 1, v |-> 0]},
        request |-> { [t |-> 1], [t |-> 2], [t |-> 3] },
        viewchange |-> {}]
    /\ sCheckpoint = SetAsFun({ <<0, {}>>, <<1, {}>>, <<2, {}>>, <<3, {}>> })
    /\ states = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ vChange
      = SetAsFun({ <<0, FALSE>>, <<1, FALSE>>, <<2, FALSE>>, <<3, FALSE>> })
    /\ views = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ TRUE

(* Transition 15 to State2 *)
State2 ==
  ByzR = { 0, 1, 2, 3 }
    /\ Checkpoints = {2}
    /\ R = { 0, 1, 2, 3 }
    /\ mlogs
      = SetAsFun({ <<
          0, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          1, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          2, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          3, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >> })
    /\ msgs
      = [checkpoint |-> {},
        commit |-> {},
        newview |-> {},
        prepare |-> {},
        preprepare |-> {},
        reply |->
          { [i |-> 0, r |-> 2, t |-> 1, v |-> 0],
            [i |-> 2, r |-> 1, t |-> 1, v |-> 0] },
        request |-> { [t |-> 1], [t |-> 2], [t |-> 3] },
        viewchange |-> {}]
    /\ sCheckpoint = SetAsFun({ <<0, {}>>, <<1, {}>>, <<2, {}>>, <<3, {}>> })
    /\ states = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ vChange
      = SetAsFun({ <<0, FALSE>>, <<1, FALSE>>, <<2, FALSE>>, <<3, FALSE>> })
    /\ views = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ TRUE

(* Transition 15 to State3 *)
State3 ==
  ByzR = { 0, 1, 2, 3 }
    /\ Checkpoints = {2}
    /\ R = { 0, 1, 2, 3 }
    /\ mlogs
      = SetAsFun({ <<
          0, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          1, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          2, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          3, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >> })
    /\ msgs
      = [checkpoint |-> {},
        commit |-> {},
        newview |-> {},
        prepare |-> {},
        preprepare |-> {},
        reply |->
          { [i |-> 0, r |-> 2, t |-> 1, v |-> 0],
            [i |-> 1, r |-> 1, t |-> 1, v |-> 0],
            [i |-> 2, r |-> 1, t |-> 1, v |-> 0] },
        request |-> { [t |-> 1], [t |-> 2], [t |-> 3] },
        viewchange |-> {}]
    /\ sCheckpoint = SetAsFun({ <<0, {}>>, <<1, {}>>, <<2, {}>>, <<3, {}>> })
    /\ states = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ vChange
      = SetAsFun({ <<0, FALSE>>, <<1, FALSE>>, <<2, FALSE>>, <<3, FALSE>> })
    /\ views = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })

(* Transition 15 to State4 *)
State4 ==
  ByzR = { 0, 1, 2, 3 }
    /\ Checkpoints = {2}
    /\ R = { 0, 1, 2, 3 }
    /\ mlogs
      = SetAsFun({ <<
          0, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          1, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          2, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >>,
        <<
          3, [checkpoint |-> {},
            commit |-> {},
            prepare |-> {},
            preprepare |-> {},
            reply |-> {},
            request |-> {},
            viewchange |-> {}]
        >> })
    /\ msgs
      = [checkpoint |-> {},
        commit |-> {},
        newview |-> {},
        prepare |-> {},
        preprepare |-> {},
        reply |->
          { [i |-> 0, r |-> 2, t |-> 1, v |-> 0],
            [i |-> 1, r |-> 1, t |-> 1, v |-> 0],
            [i |-> 2, r |-> 1, t |-> 1, v |-> 0],
            [i |-> 2, r |-> 2, t |-> 1, v |-> 0] },
        request |-> { [t |-> 1], [t |-> 2], [t |-> 3] },
        viewchange |-> {}]
    /\ sCheckpoint = SetAsFun({ <<0, {}>>, <<1, {}>>, <<2, {}>>, <<3, {}>> })
    /\ states = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })
    /\ vChange
      = SetAsFun({ <<0, FALSE>>, <<1, FALSE>>, <<2, FALSE>>, <<3, FALSE>> })
    /\ views = SetAsFun({ <<0, 0>>, <<1, 0>>, <<2, 0>>, <<3, 0>> })

Constraint ==
    CASE TLCGet("level") = 1 -> State0
      [] TLCGet("level") = 2 -> State1
      [] TLCGet("level") = 3 -> State2
      [] TLCGet("level") = 4 -> State3
      [] TLCGet("level") = 5 -> State4

================================================================================
(* Created by Apalache on Mon Aug 19 10:08:32 CEST 2024 *)

------ CONFIG violation1 ------
SPECIFICATION
    SpecByz
INVARIANT
    TypeOK
    SafetyInv
CONSTANT 
    R = { 0, 1, 2, 3 }
    ByzR = { 0, 1, 2, 3 }
    Tstamps = {1,2,3}
    Views = {0,1,2,3}
    Checkpoints = {2}
CONSTRAINT
    Constraint 
========
lemmy commented 2 months ago

The counterexample above are four consecutive InjectReply steps:

State 1: <Initial predicate>
/\ msgs = [preprepare |-> {}, prepare |-> {}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}, newview |-> {}]
/\ states = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ vChange = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 1 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 2 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 3 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}])
/\ sCheckpoint = (0 :> {} @@ 1 :> {} @@ 2 :> {} @@ 3 :> {})
/\ views = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)

State 2: <InjectReply(0) line 737, col 5 to line 743, col 63 of module pbft>
/\ msgs = [preprepare |-> {}, prepare |-> {}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {}, reply |-> {[i |-> 0, v |-> 0, t |-> 1, r |-> 1]}, checkpoint |-> {}, newview |-> {}]
/\ states = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ vChange = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 1 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 2 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 3 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}])
/\ sCheckpoint = (0 :> {} @@ 1 :> {} @@ 2 :> {} @@ 3 :> {})
/\ views = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)

State 3: <InjectReply(0) line 737, col 5 to line 743, col 63 of module pbft>
/\ msgs = [preprepare |-> {}, prepare |-> {}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {}, reply |-> {[i |-> 0, v |-> 0, t |-> 1, r |-> 1], [i |-> 0, v |-> 0, t |-> 2, r |-> 1]}, checkpoint |-> {}, newview |-> {}]
/\ states = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ vChange = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 1 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 2 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 3 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}])
/\ sCheckpoint = (0 :> {} @@ 1 :> {} @@ 2 :> {} @@ 3 :> {})
/\ views = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)

State 4: <InjectReply(1) line 737, col 5 to line 743, col 63 of module pbft>
/\ msgs = [preprepare |-> {}, prepare |-> {}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {}, reply |-> {[i |-> 0, v |-> 0, t |-> 1, r |-> 1], [i |-> 0, v |-> 0, t |-> 2, r |-> 1], [i |-> 1, v |-> 0, t |-> 1, r |-> 1]}, checkpoint |-> {}, newview |-> {}]
/\ states = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ vChange = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 1 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 2 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 3 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}])
/\ sCheckpoint = (0 :> {} @@ 1 :> {} @@ 2 :> {} @@ 3 :> {})
/\ views = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)

State 5: <InjectReply(1) line 737, col 5 to line 743, col 63 of module pbft>
/\ msgs = [preprepare |-> {}, prepare |-> {}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {}, reply |-> {[i |-> 0, v |-> 0, t |-> 1, r |-> 1], [i |-> 0, v |-> 0, t |-> 2, r |-> 1], [i |-> 1, v |-> 0, t |-> 1, r |-> 1], [i |-> 1, v |-> 0, t |-> 2, r |-> 1]}, checkpoint |-> {}, newview |-> {}]
/\ states = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ vChange = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 1 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 2 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}] @@ 3 :> [preprepare |-> {}, prepare |-> {}, request |-> {}, viewchange |-> {}, commit |-> {}, reply |-> {}, checkpoint |-> {}])
/\ sCheckpoint = (0 :> {} @@ 1 :> {} @@ 2 :> {} @@ 3 :> {})
/\ views = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
lemmy commented 2 months ago

Apalache Limitations and Bugs

1. Set-minus makes Apalache represent Tstamp as a constraint on the infinite set Nat.

Tstamps == Nat \ {0}
scala.NotImplementedError: A set filter over InfSet[CellTFrom(Int)] is not implemented
        at at.forsyte.apalache.tla.bmcmt.rules.SetFilterRule.apply(SetFilterRule.scala:32)
        at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:357)
        at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:390)
        at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:424)
        at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.eachExpr$1(SymbStateRewriterImpl.scala:447)
        at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.$anonfun$rewriteSeqUntilDone$1(SymbStateRewriterImpl.scala:453)

2. Mapping over infinite set Nat not supported

Views == Nat

...

PreparedAfterN(i,n) == 
    {<<m, v, nm>> \in (mlogs[i].request \X Views \X SeqNums) 
        : nm > n /\ Prepared(m,v,nm,i)}
...
PASS #13: BoundedChecker                                          I@08:01:50.665
Step 0: picking a transition out of 1 transition(s)               I@08:01:51.491
Input error (see the manual): Found a set map over an infinite set of CellTFrom(Int). Not supported. E@08:01:51.535

Workarounds 1. and 2.

Redefine Tstamps and Views to be finite sets such as {1,2,3} and {0,1,2,3}. Also mitigates Apalache bug Bogus safety violation checking if a set is a subset of Nat (specifically subsets of records with infinite sets).

3. Expand a powerset of size 2^48

Redefining Tstamp and Views to be (small) finite sets results in a constraint blowup when using Apalache generators (because of pbft's various defs involving SUBSET):

EXTENDS Apalache, pbft

GenInit ==
    /\ msgs = Gen(1)   \* Apalache's Gen operator is the culprit.
    /\ msgs \in Messages
    \* Below is vanilla pbft!Init
    /\ mlogs = [r \in R |-> [
        request |-> {},preprepare |-> {},prepare |-> {},commit |-> {},reply |-> {},checkpoint |-> {},viewchange |-> {}]
        ]
    /\ views = [r \in R |-> 0]
    /\ states = [r \in R |-> 0]
    /\ sCheckpoint = [r \in R |-> {}]
    /\ vChange = [r \in R |-> FALSE]
...
PASS #13: BoundedChecker                                          I@08:46:21.863
The set $C$163 is expanded, producing O(2^48) constraints. This may slow down the solver. W@08:46:22.706
<unknown>: rewriter error: Attempted to expand a powerset of size 2^48 E@08:46:22.731
at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Attempted to expand a powerset of size 2^48
        at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
        at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:135)
        at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
        at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)

MRE (msgs>ViewChangeMessage>PrepareProof>Views)

------------------------- MODULE MRE -------------------------
EXTENDS Integers, Apalache

VARIABLE
    \* @type: { v: Set( { p: Set( { pm: Set( { v: Int } ) } ) } ) };
    m

TypeOK ==
        m \in [ v : SUBSET [ p : SUBSET [ pm : SUBSET [ v : {1,2,3,4,5} ] ] ] ]

Init ==
\*    /\ m = [ v |-> {[p |-> {[pm |-> {[v |-> 1]}]} ]} ]
    /\ m = Gen(1)
    /\ TypeOK

Next ==
    UNCHANGED m
==========================================================================

https://github.com/apalache-mc/apalache/issues/2972 related if Tstamp and Views would still be infinite sets.

lemmy commented 1 month ago

Confirmed known result that TypeOK /\ SafetyInv not inductive.

The counterexample below was found by TLC's simulation mode running locally (a longer one was found by the Github action) with the configuration in 00c4de7987f9be1ae35bfa3dbb22d2d625ba8f74:

State1 ==
/\ msgs = [preprepare |-> {[v |-> 1, n |-> 2, p |-> 2, d |-> 0]}, prepare |-> {[i |-> 0, v |-> 2, n |-> 3, d |-> 1], [i |-> 1, v |-> 0, n |-> 3, d |-> 1], [i |-> 1, v |-> 1, n |-> 1, d |-> 0], [i |-> 1, v |-> 1, n |-> 1, d |-> 2], [i |-> 2, v |-> 2, n |-> 1, d |-> 1], [i |-> 3, v |-> 1, n |-> 3, d |-> 3]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {[i |-> 3, v |-> 0, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 2, r |-> 1], [i |-> 1, v |-> 2, t |-> 3, r |-> 3], [i |-> 2, v |-> 1, t |-> 3, r |-> 3], [i |-> 2, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 2, t |-> 3, r |-> 2], [i |-> 3, v |-> 2, t |-> 3, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 0], [i |-> 1, n |-> 2, d |-> 0], [i |-> 2, n |-> 1, d |-> 2], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 1, d |-> 1]}, newview |-> {[v |-> 2, p |-> 0, vc |-> {[i |-> 1, v |-> 1, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 1, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, o |-> {[v |-> 2, n |-> 1, p |-> 2, d |-> 0]}], [v |-> 2, p |-> 1, vc |-> {[i |-> 0, v |-> 1, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 1, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, o |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 0, n |-> 1, p |-> 3, d |-> 2], [v |-> 1, n |-> 3, p |-> 2, d |-> 3]}], [v |-> 2, p |-> 3, vc |-> {[i |-> 0, v |-> 1, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 1, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, o |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 0, n |-> 1, p |-> 3, d |-> 2], [v |-> 1, n |-> 3, p |-> 2, d |-> 3]}]}]
/\ states = (0 :> 0 @@ 1 :> 3 @@ 2 :> 1 @@ 3 :> 2)
/\ vChange = (0 :> TRUE @@ 1 :> TRUE @@ 2 :> TRUE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 0, v |-> 0, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 0, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 3, v |-> 2, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}] @@ 1 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 3, v |-> 0, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}] @@ 2 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 3, v |-> 0, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}] @@ 3 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 0, v |-> 0, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 0, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 3, v |-> 2, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}])
/\ sCheckpoint = (0 :> {[i |-> 1, n |-> 1, d |-> 2], [i |-> 2, n |-> 2, d |-> 2], [i |-> 2, n |-> 3, d |-> 3]} @@ 1 :> {[i |-> 0, n |-> 1, d |-> 3], [i |-> 3, n |-> 3, d |-> 3]} @@ 2 :> {[i |-> 1, n |-> 1, d |-> 2], [i |-> 2, n |-> 2, d |-> 2], [i |-> 2, n |-> 3, d |-> 3]} @@ 3 :> {[i |-> 0, n |-> 1, d |-> 3], [i |-> 3, n |-> 3, d |-> 3]})
/\ views = (0 :> 2 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 1)

State2 ==
/\ msgs = [preprepare |-> {[v |-> 1, n |-> 2, p |-> 2, d |-> 0]}, prepare |-> {[i |-> 0, v |-> 2, n |-> 3, d |-> 1], [i |-> 1, v |-> 0, n |-> 3, d |-> 1], [i |-> 1, v |-> 1, n |-> 1, d |-> 0], [i |-> 1, v |-> 1, n |-> 1, d |-> 2], [i |-> 2, v |-> 2, n |-> 1, d |-> 1], [i |-> 3, v |-> 1, n |-> 3, d |-> 3]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {}, commit |-> {[i |-> 3, v |-> 0, n |-> 2, d |-> 2]}, reply |-> {[i |-> 0, v |-> 0, t |-> 3, r |-> 1], [i |-> 1, v |-> 0, t |-> 2, r |-> 1], [i |-> 1, v |-> 2, t |-> 3, r |-> 3], [i |-> 2, v |-> 1, t |-> 3, r |-> 3], [i |-> 2, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 2, t |-> 3, r |-> 2], [i |-> 3, v |-> 2, t |-> 3, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 0], [i |-> 1, n |-> 2, d |-> 0], [i |-> 2, n |-> 1, d |-> 2], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 1, d |-> 1]}, newview |-> {[v |-> 2, p |-> 0, vc |-> {[i |-> 1, v |-> 1, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 1, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, o |-> {[v |-> 2, n |-> 1, p |-> 2, d |-> 0]}], [v |-> 2, p |-> 1, vc |-> {[i |-> 0, v |-> 1, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 1, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, o |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 0, n |-> 1, p |-> 3, d |-> 2], [v |-> 1, n |-> 3, p |-> 2, d |-> 3]}], [v |-> 2, p |-> 3, vc |-> {[i |-> 0, v |-> 1, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 1, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, o |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 0, n |-> 1, p |-> 3, d |-> 2], [v |-> 1, n |-> 3, p |-> 2, d |-> 3]}]}]
/\ states = (0 :> 0 @@ 1 :> 3 @@ 2 :> 1 @@ 3 :> 2)
/\ vChange = (0 :> TRUE @@ 1 :> TRUE @@ 2 :> TRUE @@ 3 :> FALSE)
/\ mlogs = (0 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 0, v |-> 0, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 0, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 3, v |-> 2, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}] @@ 1 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 3, v |-> 0, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}] @@ 2 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 3, v |-> 0, n |-> 0, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}] @@ 3 :> [preprepare |-> {[v |-> 0, n |-> 1, p |-> 3, d |-> 1], [v |-> 2, n |-> 1, p |-> 3, d |-> 0]}, prepare |-> {[i |-> 2, v |-> 1, n |-> 1, d |-> 0]}, request |-> {[t |-> 1], [t |-> 2], [t |-> 3]}, viewchange |-> {[i |-> 0, v |-> 0, n |-> 2, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 2, d |-> 3], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 1, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 2, v |-> 0, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 0, n |-> 3, d |-> 0], [i |-> 2, n |-> 1, d |-> 1], [i |-> 2, n |-> 1, d |-> 2], [i |-> 3, n |-> 3, d |-> 1]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}], [i |-> 3, v |-> 2, n |-> 1, c |-> {[i |-> 0, n |-> 2, d |-> 1], [i |-> 1, n |-> 1, d |-> 2]}, p |-> {[preprepare |-> [v |-> 0, n |-> 2, p |-> 0, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 0, n |-> 3, p |-> 1, d |-> 1], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}], [preprepare |-> [v |-> 2, n |-> 2, p |-> 2, d |-> 0], prepare |-> {[i |-> 0, v |-> 0, n |-> 2, d |-> 2]}]}]}, commit |-> {[i |-> 2, v |-> 1, n |-> 2, d |-> 2]}, reply |-> {[i |-> 1, v |-> 0, t |-> 1, r |-> 3], [i |-> 1, v |-> 2, t |-> 3, r |-> 1], [i |-> 2, v |-> 1, t |-> 1, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 1], [i |-> 2, v |-> 1, t |-> 2, r |-> 3]}, checkpoint |-> {[i |-> 0, n |-> 2, d |-> 2], [i |-> 0, n |-> 2, d |-> 3], [i |-> 2, n |-> 2, d |-> 3], [i |-> 2, n |-> 3, d |-> 1], [i |-> 3, n |-> 2, d |-> 1]}])
/\ sCheckpoint = (0 :> {[i |-> 1, n |-> 1, d |-> 2], [i |-> 2, n |-> 2, d |-> 2], [i |-> 2, n |-> 3, d |-> 3]} @@ 1 :> {[i |-> 0, n |-> 1, d |-> 3], [i |-> 3, n |-> 3, d |-> 3]} @@ 2 :> {[i |-> 1, n |-> 1, d |-> 2], [i |-> 2, n |-> 2, d |-> 2], [i |-> 2, n |-> 3, d |-> 3]} @@ 3 :> {[i |-> 0, n |-> 1, d |-> 3], [i |-> 3, n |-> 3, d |-> 3]})
/\ views = (0 :> 2 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 1)

TLC shows and Apalache confirms that the original and the simplified initial state below immediately lead to a violation of SafetyInv.

State0 ==
    /\ msgs = [
        preprepare |-> {},
        prepare |-> {},
        request |-> {},
        viewchange |-> {},
        commit |-> {},
        reply |-> {
            [i |-> 1, v |-> 2, t |-> 3, r |-> 3], 
            [i |-> 2, v |-> 2, t |-> 3, r |-> 2], 
            [i |-> 3, v |-> 2, t |-> 3, r |-> 2]},   \* The honest nodes 1..3 disagree on the value r at t=3 and v=2. 
        checkpoint |-> {},
        newview |-> {} ]
    /\ mlogs = [r \in R |-> [
            request |-> {},
            preprepare |-> {},
            prepare |-> {},
            commit |-> {},
            reply |-> {},
            checkpoint |-> {},
            viewchange |-> {}]]
    /\ vChange = [r \in R |-> FALSE]
    /\ views = [r \in R |-> 0]
    /\ states = [r \in R |-> 0]
    /\ sCheckpoint = [r \in R |-> {}]
lemmy commented 1 month ago

Closing cause validation is working to the extend that it confirms that SafetyInv is not inductive.