test(spec): A problematic run

specs/quint/tests/decideForPastRound/decideForPastRoundTest.qnt

@@ -0,0 +1,20 @@
+// -*- mode: Bluespec; -*-
+
+module decideForPastRoundTest {
+
+import decideForPastRound(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v1"),
+    Values = Set("red", "blue"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0), // , 1, 2, 3)
+    otherSet = Set("v2", "v3"),
+    testedVal = ("v4")
+) as N4F1 from "./decideForPastRoundrun"
+
+run decidePastTest = {
+    N4F1::runToDecision
+}
+
+}

specs/quint/tests/decideForPastRound/decideForPastRoundrun.qnt

@@ -0,0 +1,61 @@
+// -*- mode: Bluespec; -*-
+
+module decideForPastRound {
+
+import TendermintDSL.* from "../../specs/TendermintDSL"
+export TendermintDSL.*
+
+const testedVal : Address
+const otherSet : Set[Address]
+val others = otherSet.fold(List(), (s, x) => s.append(x)) 
+
+/*
+- there is a correct validator "testedVal" that we want to observe
+- there need to be faulty processes
+- there are *other* processes that together with the faulty ones are 2f+1
+- the others include the proposer.
+- the faulty processes help the others to decide in round 0
+- testedVal goes to round 1 upon timeoutPrecommit
+
+*/
+
+run runToDecision = {
+    val nextProposer = proposer(validatorSet, 0, 1)
+    init
+    .then(valStep(testedVal))
+// proposer sends proposal and other processes receive it -> send prevote value
+    .then(all {
+        // others should be at most 2/3.
+        // if this assertion fails the set need to be set differently
+        assert(3 * size(otherSet) <= 2 * size(validators)),  
+        assert(3 * size(otherSet.union(Faulty)) > 2 * size(validators)),  
+        everyoneReceivesProposal(others, validatorList, validatorSet, 0, 0, "blue")
+    })
+
+// Others receive the prevotes of others and the faulty ones -> send precommit value
+    .then(ListDeliverAllVotes (Prevote, others.concat(faultyList), others, validatorSet, 0, 0, Val("blue")))
+    .then(others.concat(faultyList).length().reps(_ => ListTakeAStep(others)))
+    .then(ListTakeAStep(others))
+
+// Precommit from faulty processes are delivered -> value to others, nil to testedVal
+    .then(ListDeliverAllVotes (Precommit, faultyList, others, validatorSet, 0, 0, Val("blue")))
+    .then(ProcessDeliverAllVotes (Precommit, testedVal, faultyList, validatorSet, 0, 0, Nil))
+
+// Precommit from others are delivered to all correct processes
+    .then(ListDeliverAllVotes (Precommit, others, correctList, validatorSet, 0, 0, Val("blue")))
+// correct ones (others and testedVal) take steps to process all incoming precommits
+    .then(others.concat(faultyList).length().reps(_ => ListTakeAStep(others.concat(List(testedVal)))))
+
+// at this point others have decided and testedVal is ready to go into next round.
+    .then(valStep(testedVal))
+
+// TODO: at this point we are stuck. Let's discuss
+
+//    .then(ProcessDeliverAllVotes ("Precommit", testedVal, faultyList, validatorSet, 0, 0, "blue"))
+ //   .then(valStep(testedVal))
+ //   .then(deliverSomeProposal(testedVal))
+ //   .then(valStep(testedVal))
+// not sure what should happen now.
+}
+
+}

specs/quint/tests/line26/line26Test.qnt

@@ -0,0 +1,21 @@
+// -*- mode: Bluespec; -*-
+
+module line26Test {
+
+import line26run(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v3"), // validator of second round
+    Values = Set("red", "blue"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0), // , 1, 2, 3)
+    otherSet = Set("v2", "v4")
+) as N4F1 from "./line26run"
+
+run line26Test = {
+    N4F1::runToLine26
+}
+
+
+
+}

specs/quint/tests/line26/line26run.qnt

@@ -0,0 +1,60 @@
+// -*- mode: Bluespec; -*-
+
+module line26run {
+
+import TendermintDSL.* from "../../specs/TendermintDSL"
+export TendermintDSL.*
+
+const otherSet : Set[Address]
+val others = otherSet.fold(List(), (s, x) => s.append(x)) 
+
+/*
+- there need to be faulty processes
+- there are other processes that together with the faulty ones are 2f+1
+- the others include the proposer.
+- the others are successful until sending precommit value
+    - they set locked value and valid value
+- then faulty precommit nil are delivered to correct processes
+- the precommits from others are delivered to correct processes so that timeoutprecommit is started
+- correct processes go to the next round
+- there the proposer
+    - ignores the valid value stored and send a proposal for a different value
+    - correct processes take this to execute line 26 and prevote nil
+*/
+
+run runToLine26 = {
+    val nextProposer = proposer(validatorSet, 0, 1)
+    nondet value = oneOf(Values)
+    nondet otherValue = oneOf(Values.exclude(Set(value)))
+    init
+
+    // proposer sends proposal and correct processes receive -> send prevote value
+    .then(all {
+        // others should be at most 2/3.
+        // if this assertion fails the set need to be set differently
+        assert(3 * size(otherSet) <= 2 * size(validators)),  
+        assert(3 * size(otherSet.union(Faulty)) > 2 * size(validators)),  
+        everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, value)
+    })
+    // correct processes receive prevotes from correct processes -> send precommit    
+    .then(fromPrevoteToPrecommit(correctList, correctList, validatorList, validatorSet, 0, 0, Val(value)))
+    // TODO assertion: valid and locked is set.
+    // now the faulty nodes precommit nil
+    .then(ListDeliverAllVotes(Precommit, faultyList, correctList, validatorSet, 0, 0, Nil))
+    // correct processes receive faulty precommit nil
+    .then(faultyList.length().reps(_ => ListTakeAStep(correctList)))   
+    // now the precommits from some correct processes are delivered, 
+    // "other" processes are just enough so that timeoutPrecommit is started
+    .then(ListDeliverAllVotes(Precommit, others, correctList, validatorSet, 0, 0, Val(value)))
+    .then(others.length().reps(_ => ListTakeAStep(correctList)))
+    .then(ListTakeAStep(correctList))
+    .then(ListDeliverProposal(correctList, mkProposal(nextProposer, 0, 1, otherValue, -1)))
+    .then(ListTakeAStep(correctList))
+    .then(all{
+        // TODO: this test fails, commented it by now
+	// assert(voteBuffer.get("v1").contains(mkVote(Prevote, "v4", 0, 1, Nil))),
+        unchangedAll
+    })
+}
+
+}

specs/quint/tests/line28/line28run.qnt

@@ -5,13 +5,28 @@ module line28run {
 import TendermintDSL.* from "../../specs/TendermintDSL"
 export TendermintDSL.*
 
-const otherSet: Set[Address]
+const otherSet : Set[Address]
 val others = otherSet.fold(List(), (s, x) => s.append(x)) 
 
+/*
+- there need to be faulty processes
+- there are other processes that together with the faulty ones are 2f+1
+- the others include the proposer.
+- the others are successful until sending precommit value
+    - they set locked value and valid value
+- then faulty precommit nil are delivered to correct processes
+- the precommits from others are delivered to correct processes so that timeoutprecommit is started
+- correct processes go to the next round
+- there the proposer
+    - uses the valid value stored to send proposal for valid value
+    - correct processes take this to execute line 28 and prevote for this value
+*/
+
 run runToLine28 = 
     val nextProposer = proposer(validatorSet, 0, 1)
     nondet value = oneOf(Values)
     init
+    // proposer sends proposal and correct processes receive -> send prevote value
     .then(all {
         // others should be at most 2/3.
         // if this assertion fails the set need to be set differently