test for prevoting nil because of more recent lock

specs/quint/specs/TendermintDSL.qnt

@@ -23,6 +23,10 @@ run ListDeliverProposal (active, propMsg) = {
     active.length().reps(i => deliverProposal(active[i], propMsg))
 }
 
+run ListDeliverVote (active, voteMsg) = {
+    active.length().reps(i => deliverVote(active[i], voteMsg))
+}
+
 run ListDeliverSomeProposal (active) = {
     active.length().reps(i => deliverSomeProposal(active[i]))
 }

specs/quint/tests/line32/line32Test.qnt

@@ -13,10 +13,23 @@ import line32run(
     slowByz = "v3"
 ) as N4F3 from "./line32run"
 
-run line32Test = {
+run line32TestInvalid = {
     N4F3::runToLine32invalid
 }
 
+import line32run(
+    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)
+    testedVal = "v4",
+    slowByz = "v1"
+) as N4F1 from "./line32run"
 
+run line32TestLocked = {
+    N4F1::runToLine32locked
+}
 
 }

specs/quint/tests/line32/line32run.qnt

@@ -8,11 +8,10 @@ export TendermintDSL.*
 const testedVal : Address
 const slowByz : Address
 
-// the driver does not store invalid proposals. So we need to receive prevotes first and then the proposal
-// first we send the correct guy to round 1
-
 
 run runToLine32invalid = 
+// the driver does not store invalid proposals. So we need to receive prevotes first and then the proposal
+// first we send the correct guy to round 1
     val nextProposer = proposer(validatorSet, 0, 1)
     val propVal = "invalid"
     init
@@ -43,4 +42,59 @@ run runToLine32invalid =
 
     )
 
+
+run runToLine32locked = 
+    // we need proposer of round 1 to not lock, and someone to lock.
+    val nextProposer = proposer(validatorSet, 0, 1)
+    val thirdProposer = proposer(validatorSet, 0, 2)
+    nondet value = oneOf(Values)
+    nondet nextValue = oneOf(Values.exclude(Set(value)))
+    init
+    .then(all {
+        everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, value)
+    })
+    // third receive all prevotes    
+    .then(ProcessDeliverAllVotes(Prevote, thirdProposer, correctList, validatorSet, 0, 0, Val(value)))
+    .then(correctList.length().reps(_ => valStep(thirdProposer)))
+    .then(2.reps(_ => valStep(thirdProposer)))
+    // now third proposer as locked and consumed step change
+    .then(ListDeliverVote(correctList.select(x => x != thirdProposer), mkVote(Prevote, slowByz, 0, 0, Nil)))
+    .then(ListTakeAStep(correctList.select(x => x != thirdProposer)))
+    .then(ListDeliverAllVotes(Prevote, correctList.select(x => x != thirdProposer), correctList.select(x => x != thirdProposer), validatorSet, 0, 0, Val(value)))
+    .then(correctList.length().reps(_ => ListTakeAStep(correctList.select(x => x != thirdProposer)))) // process 2f correct and 1 faulty prevotes processed
+    .then(ListTakeAStep(correctList.select(x => x != thirdProposer))) // consume step change
+    .then(ListDeliverVote(correctList, mkVote(Precommit, thirdProposer, 0, 0, Val(value))))
+    .then(ListDeliverAllVotes(Precommit, correctList.select(x => x != thirdProposer), correctList, validatorSet, 0, 0, Nil))
+    .then(correctList.length().reps(_ => ListTakeAStep(correctList)))
+    // here all correct have precommit timeout started
+    // thirdproposer has locked value
+    // we go to the next round
+    .then(all {
+        everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 1, nextValue)
+    })
+    .then(ListDeliverVote(correctList.select(x => x != thirdProposer), mkVote(Prevote, slowByz, 0, 1, Val(nextValue))))
+    .then(ListDeliverAllVotes(Prevote, correctList.select(x => x != thirdProposer), correctList.select(x => x != thirdProposer), validatorSet, 0, 1, Val(nextValue)))
+    .then(correctList.length().reps(_ => ListTakeAStep(correctList.select(x => x != thirdProposer))))
+    .then(2.reps(_ => ListTakeAStep(correctList.select(x => x != thirdProposer))))
+    .then(ListDeliverVote(correctList, mkVote(Precommit, slowByz, 0, 1, Nil)))
+    .then(ListDeliverAllVotes(Precommit, correctList.select(x => x != thirdProposer), correctList, validatorSet, 0, 1, Val(nextValue)))
+    .then(correctList.length().reps(_ => ListTakeAStep(correctList)))    
+    // here all correct have precommit timeout started
+    // thirdproposer has locked value
+    // other correct processes have locked nextValue
+    // now we deliver the prevote from thirdProposer so that others have Polka for round 0
+    .then(ListDeliverVote(correctList.select(x => x != thirdProposer), mkVote(Prevote, thirdProposer, 0, 0, Val(value))))
+    .then(ListTakeAStep(correctList.select(x => x != thirdProposer)))
+    // we go to the next round
+   .then(all {
+        everyoneReceivesProposalVR(correctList, validatorList, validatorSet, 0, 2, value, 0)
+    })
+    .then(all { // the others prevoted Nil because they had a more recent lock
+        assert(SetFromList(correctList.select(x => x != thirdProposer)).forall(x => 
+                system.get(x).es.cs.step == PrevoteStep and
+                voteBuffer.get(x).contains(mkVote(Prevote, x, 0, 2, Nil))
+                )),
+        unchangedAll
+    })
+
 }