one line fix (#1179)

* fix the model * add the assumption * fix the tests
informalsystems · Sep 22, 2023 · ff4a4b1 · ff4a4b1
1 parent 62a7b8f
commit ff4a4b1
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 45 deletions.
diff --git a/examples/cosmos/tendermint/Tendermint.qnt b/examples/cosmos/tendermint/Tendermint.qnt
@@ -78,6 +78,9 @@ module Tendermint {
   // the proposer function from 0..NRounds to the set of processes
   const Proposer: Round_t -> Proc_t
 
+  assume Corr_and_faulty_are_disjoint =
+      (Corr.intersect(Faulty) == Set())
+
   assume Corr_and_faulty_make_N =
       N == size(Corr.union(Faulty))
 

diff --git a/examples/cosmos/tendermint/TendermintModels.qnt b/examples/cosmos/tendermint/TendermintModels.qnt
@@ -12,7 +12,7 @@ module TendermintModels {
   ) as n4_f1 from "./TendermintTest"
 
   import TendermintTest(
-    Corr = Set("p1", "p2", "p3"),
+    Corr = Set("p1", "p2"),
     Faulty = Set("p3", "p4"),
     N = 4,
     T = 1,

diff --git a/examples/cosmos/tendermint/TendermintTest.qnt b/examples/cosmos/tendermint/TendermintTest.qnt
@@ -23,26 +23,30 @@ module TendermintTest {
 
   // three correct processes behave and decide on the same value
   run decisionTest = {
-    nondet v = oneOf(ValidValues)
-    val p1 = Proposer.get(0)
-    nondet p2 = Corr.exclude(Set(p1)).oneOf()
-    nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
-    Init.then(InsertProposal(p1, v))
-        .then(UponProposalInPropose(p1, v))
-        .then(UponProposalInPropose(p2, v))
-        .then(UponProposalInPropose(p3, v))
-        .then(UponProposalInPrevoteOrCommitAndPrevote(p1, v, NilRound))
-        .then(UponProposalInPrevoteOrCommitAndPrevote(p2, v, NilRound))
-        .then(UponProposalInPrevoteOrCommitAndPrevote(p3, v, NilRound))
-        .then(UponProposalInPrecommitNoDecision(p1, v, 0, NilRound))
-        .then(UponProposalInPrecommitNoDecision(p2, v, 0, NilRound))
-        .then(UponProposalInPrecommitNoDecision(p3, v, 0, NilRound))
-        .then(all {
-          assert(decision.get(p1) == v),
-          assert(decision.get(p2) == v),
-          assert(decision.get(p3) == v),
-          unchangedAll,
-        })
+    if (size(Corr) >= 3) {
+      nondet v = oneOf(ValidValues)
+      val p1 = Proposer.get(0)
+      nondet p2 = Corr.exclude(Set(p1)).oneOf()
+      nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
+      Init.then(InsertProposal(p1, v))
+          .then(UponProposalInPropose(p1, v))
+          .then(UponProposalInPropose(p2, v))
+          .then(UponProposalInPropose(p3, v))
+          .then(UponProposalInPrevoteOrCommitAndPrevote(p1, v, NilRound))
+          .then(UponProposalInPrevoteOrCommitAndPrevote(p2, v, NilRound))
+          .then(UponProposalInPrevoteOrCommitAndPrevote(p3, v, NilRound))
+          .then(UponProposalInPrecommitNoDecision(p1, v, 0, NilRound))
+          .then(UponProposalInPrecommitNoDecision(p2, v, 0, NilRound))
+          .then(UponProposalInPrecommitNoDecision(p3, v, 0, NilRound))
+          .then(all {
+            assert(decision.get(p1) == v),
+            assert(decision.get(p2) == v),
+            assert(decision.get(p3) == v),
+            unchangedAll,
+          })
+    } else {
+      Init.then(unchangedAll)
+    }
   }
 
   // a correct proposer cannot propose twice in the same round
@@ -55,29 +59,33 @@ module TendermintTest {
 
   // a correct proposer proposes but other processes timeout
   run timeoutProposeTest = {
-    val p1 = Proposer.get(0)
-    nondet p2 = Corr.exclude(Set(p1)).oneOf()
-    nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
-    Init.then(InsertProposal(p1, "v0"))
-        .then(UponProposalInPropose(p1, "v0"))
-        .then(OnTimeoutPropose(p2))
-        .then(OnTimeoutPropose(p3))
-        .then(
-          val E = msgsPrevote.get(0).filter(m => m.src.in(Corr))
-          UponQuorumOfPrevotesAny(p1, E)
-            .then(UponQuorumOfPrevotesAny(p2, E))
-            .then(UponQuorumOfPrevotesAny(p3, E))
-        )
-        .then(
-          val E = msgsPrecommit.get(0).filter(m => m.src.in(Corr))
-          UponQuorumOfPrecommitsAny(p1, E)
-            .then(UponQuorumOfPrecommitsAny(p2, E))
-            .then(UponQuorumOfPrecommitsAny(p3, E))
-        )
-        .then(all {
-          // all correct processes switch to the next round
-          assert(Corr.forall(p => round.get(p) == 1)),
-          unchangedAll,
-        })
+    if (size(Corr) >= 3) {
+      val p1 = Proposer.get(0)
+      nondet p2 = Corr.exclude(Set(p1)).oneOf()
+      nondet p3 = Corr.exclude(Set(p1, p2)).oneOf()
+      Init.then(InsertProposal(p1, "v0"))
+          .then(UponProposalInPropose(p1, "v0"))
+          .then(OnTimeoutPropose(p2))
+          .then(OnTimeoutPropose(p3))
+          .then(
+            val E = msgsPrevote.get(0).filter(m => m.src.in(Corr))
+            UponQuorumOfPrevotesAny(p1, E)
+              .then(UponQuorumOfPrevotesAny(p2, E))
+              .then(UponQuorumOfPrevotesAny(p3, E))
+          )
+          .then(
+            val E = msgsPrecommit.get(0).filter(m => m.src.in(Corr))
+            UponQuorumOfPrecommitsAny(p1, E)
+              .then(UponQuorumOfPrecommitsAny(p2, E))
+              .then(UponQuorumOfPrecommitsAny(p3, E))
+          )
+          .then(all {
+            // all correct processes switch to the next round
+            assert(Corr.forall(p => round.get(p) == 1)),
+            unchangedAll,
+          })
+    } else {
+      Init.then(unchangedAll)
+    }
   }
 }