nice parameterized testrun

Specs/Quint/line28Test.qnt

@@ -0,0 +1,19 @@
+// -*- mode: Bluespec; -*-
+
+module line28Test {
+
+import line28run(
+    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", "v4")
+) as N4F1 from "./line28run"
+
+run line28Test = {
+    N4F1::runToLine28
+}
+
+}

Specs/Quint/line28run.qnt

@@ -0,0 +1,42 @@
+// -*- mode: Bluespec; -*-
+
+module line28run {
+
+import TendermintDSL.* from "./TendermintDSL"
+export TendermintDSL.*
+
+const otherSet : Set[Address_t]
+val others = otherSet.fold(List(), (s, x) => s.append(x)) 
+
+run runToLine28 = {
+    val nextProposer = Proposer (validatorSet, 0, 1)
+    init
+    .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)),  
+        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))
+    // now the faulty nodes precommit nil
+    .then(ListDeliverAllVotes("Precommit", faultyList, correctList, validatorSet, 0, 0, "nil"))
+    .then(faultyList.length().reps(_ => ListTakeAStep(correctList)))   
+    // now the other precommits are delivered, so that timeoutPrecommit is started
+    .then(ListDeliverAllVotes("Precommit", others, correctList, validatorSet, 0, 0, "blue"))
+    .then(others.length().reps(_ => ListTakeAStep(correctList)))
+    // TimeoutPrecommit is there an can fire and bring is to the next round.
+    .then(all{
+        assert(system.get(nextProposer).timeout.contains(("TimeoutPrecommit", 0, 0))),
+        everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "red")
+    })
+    .then(all{
+        assert(voteBuffer.get(nextProposer).contains( { height: 0, id: "blue", round: 1, src: nextProposer, step: "Prevote" })),
+        unchangedAll
+    })
+}
+
+}