Inductive invariant validation with Apalache and TLC #5

lemmy · 2024-08-16T09:28:34Z

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

Ordinary invariant checking `TypeOK` and `SafetyInv` of `Spec` and `SpecByz`

Rewrite for set membership of the powerset of a record where the record has infinite co-domains. apalache-mc/apalache#2946
Fix the release pipeline apalache-mc/apalache#2951
Bogus safety violation checking if a set is a subset of Nat apalache-mc/apalache#2948
Unexpected equality test over types CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] apalache-mc/apalache#2972
ExprOptimizer: Rewrite S \in SUBSET T when it occurs in subexpressions apalache-mc/apalache#2975

TLC

tlaplus/tlaplus@6a1ea00

The text was updated successfully, but these errors were encountered:

* https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds * apalache-mc/apalache#425 * apalache-mc/apalache#1431 Github issue heidihoward#5 heidihoward#5 [Apalache] Signed-off-by: Markus Alexander Kuppe <[email protected]>

terminate gracefully. Real-world project where some simulation workers seemingly never terminate: https://github.com/heidihoward/pbft-tlaplus/actions/workflows/tla.yml [Feature][TLC] Signed-off-by: Markus Alexander Kuppe <[email protected]>

lemmy · 2024-08-28T16:13:23Z

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
==========================================================================

apalache-mc/apalache#2972 related if Tstamp and Views would still be infinite sets.

lemmy · 2024-09-05T02:23:24Z

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 00c4de7:

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 |-> {}]

* https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds * apalache-mc/apalache#425 * apalache-mc/apalache#1431 Github issue #5 #5 [Apalache] Signed-off-by: Markus Alexander Kuppe <[email protected]>

lemmy · 2024-09-06T17:38:12Z

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

lemmy added the enhancement New feature or request label Aug 16, 2024

lemmy mentioned this issue Aug 19, 2024

Inductive invariant validation. #6

Merged

This comment was marked as resolved.

Sign in to view

lemmy mentioned this issue Aug 19, 2024

Rewrite for set membership of the powerset of a record where the record has infinite co-domains. apalache-mc/apalache#2946

Merged

2 tasks

This comment was marked as resolved.

Sign in to view

lemmy changed the title ~~Inductive invariant validation with Apalache~~ Inductive invariant validation with Apalache and TLC Sep 6, 2024

lemmy closed this as completed Sep 6, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Inductive invariant validation with Apalache and TLC #5

Inductive invariant validation with Apalache and TLC #5

lemmy commented Aug 16, 2024 •

edited

Loading

This comment was marked as resolved.

This comment was marked as resolved.

lemmy commented Aug 28, 2024 •

edited

Loading

lemmy commented Sep 5, 2024

lemmy commented Sep 6, 2024

Inductive invariant validation with Apalache and TLC #5

Inductive invariant validation with Apalache and TLC #5

Comments

lemmy commented Aug 16, 2024 • edited Loading

Ordinary invariant checking TypeOK and SafetyInv of Spec and SpecByz

TLC

This comment was marked as resolved.

This comment was marked as resolved.

lemmy commented Aug 28, 2024 • edited Loading

Apalache Limitations and Bugs

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

2. Mapping over infinite set Nat not supported

Workarounds 1. and 2.

3. Expand a powerset of size 2^48

lemmy commented Sep 5, 2024

lemmy commented Sep 6, 2024

lemmy commented Aug 16, 2024 •

edited

Loading

Ordinary invariant checking `TypeOK` and `SafetyInv` of `Spec` and `SpecByz`

lemmy commented Aug 28, 2024 •

edited

Loading

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

2. Mapping over infinite set `Nat` not supported