Added a test to reach line 42 without locking

Specs/Quint/TendermintDSL.qnt

@@ -41,8 +41,12 @@ run everyoneReceivesProposal (active, valList, valset, h, r, value) = {
     .then(ListTakeAStep(active))    
 }
 
-
-
+run fromPrevoteToPrecommit (prevoteSenders, prevoteReceivers, valList, valset, h, r, value) = {
+    ListDeliverAllVotes("Prevote", prevoteSenders, prevoteReceivers, valset, h, r, value)
+    .then(prevoteSenders.length().reps(_ => ListTakeAStep(prevoteReceivers)))
+    // extra step due to timeoutprevote double step
+    .then(ListTakeAStep(prevoteReceivers))
+}
 
 
 }

Specs/Quint/coverage.md

@@ -4,17 +4,17 @@
 
 | line | comment | (C) | test |
 |  -----:| ---- | -----| -----| 
- 16 |  reuse valid value | | 
+ 16 |  reuse valid value | | line28Test.qnt
  18 | new value | X2 
  19 | send proposal | | (A) RoundswitchTest (^1)
  21 | start timeoutPropose | X1, X2b, X2c
  24 | prevote value | X1, X2
  26 | prevote nil (on invalid or locked) | X2c
- 30 | prevote value on old prevotes |
+ 30 | prevote value on old prevotes | | line28Test.qnt
  32 | prevote nil on old prevotes (on invalid or locked)  |
  35 | start timeoutPrevote  | X2
  40 | precommit value  | X1
- 42 without 41  | set valid without locked  |
+ 42 without 41  | set valid without locked  | | line42Test
  45 | precommit nil | X2b
  48 | start timeoutPrecommit  | X2 , X2b
  51 | decide  | X1

Specs/Quint/line28run.qnt

@@ -19,10 +19,7 @@ run runToLine28 = {
         everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "blue")
     })
     // receive all prevotes    
-    .then(ListDeliverAllVotes("Prevote", correctList, correctList, validatorSet, 0, 0, "blue"))
-    .then(correctList.length().reps(_ => ListTakeAStep(correctList)))
-    // extra step due to timeoutprevote double step
-    .then(ListTakeAStep(correctList))
+    .then(fromPrevoteToPrecommit (correctList, correctList, validatorList, validatorSet, 0, 0, "blue"))
     // now the faulty nodes precommit nil
     .then(ListDeliverAllVotes("Precommit", faultyList, correctList, validatorSet, 0, 0, "nil"))
     .then(faultyList.length().reps(_ => ListTakeAStep(correctList)))   

Specs/Quint/line42Test.qnt

@@ -0,0 +1,19 @@
+// -*- mode: Bluespec; -*-
+
+module line42Test {
+
+import line42run(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set(),
+    Values = Set("red", "blue"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0), // , 1, 2, 3)
+    testedVal = "v4"
+) as N4F0 from "./line42run"
+
+run line42Test = {
+    N4F0::runToLine42
+}
+
+}

Specs/Quint/line42run.qnt

@@ -0,0 +1,48 @@
+// -*- mode: Bluespec; -*-
+
+module line42run {
+
+import TendermintDSL.* from "./TendermintDSL"
+export TendermintDSL.*
+
+const testedVal : Address_t
+val others = validators.exclude(Set(testedVal)) 
+val othersList = others.fold(List(), (s, x) => s.append(x))
+
+run runToLine42 = {
+    val value = "blue"
+    init
+    .then(valStep(testedVal))
+    .then(everyoneReceivesProposal(othersList, validatorList, validatorSet, 0, 0, value))
+    .then(fromPrevoteToPrecommit(othersList, othersList, validatorList, validatorSet, 0, 0, value))
+    // At this point we have set up the environment for "testedVal" to reach line 42 without
+    // any other process taking any steps
+    .then(all{
+        assert(system.get(testedVal).timeout.contains(("TimeoutPropose", 0, 0))),
+        valStep(testedVal)
+    })
+    .then(ProcessDeliverAllVotes("Prevote", testedVal, othersList, validatorSet, 0, 0, value))
+    .then(othersList.length().reps(_ => valStep(testedVal)))
+    .then(all{
+        assert(system.get(testedVal).timeout.contains(("TimeoutPrevote", 0, 0))),
+        valStep(testedVal) 
+    })
+    .then(all{
+        assert(system.get(testedVal).es.cs.step == "Precommit"),
+        deliverSomeProposal(testedVal)
+    })
+    .then(valStep(testedVal)) // here it executes line 36 with branch 42
+    .then(all{
+        val cstate = system.get(testedVal).es.cs
+        assert(all{
+            cstate.lockedRound == -1,
+            cstate.lockedValue == "nil",
+            cstate.validRound == 0,
+            cstate.validValue == value
+            }),
+        unchangedAll
+    }) 
+}
+
+}
+