From 062215ebe614a2367717fd42b7d3ab620acca8ae Mon Sep 17 00:00:00 2001
From: Josef Widder <josef@informal.systems>
Date: Wed, 29 Nov 2023 16:07:59 +0100
Subject: [PATCH] nice parameterized testrun

---
 Specs/Quint/line28Test.qnt | 19 +++++++++++++++++
 Specs/Quint/line28run.qnt  | 42 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+)
 create mode 100644 Specs/Quint/line28Test.qnt
 create mode 100644 Specs/Quint/line28run.qnt

diff --git a/Specs/Quint/line28Test.qnt b/Specs/Quint/line28Test.qnt
new file mode 100644
index 000000000..75e1c15d9
--- /dev/null
+++ b/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
+}
+
+}
\ No newline at end of file
diff --git a/Specs/Quint/line28run.qnt b/Specs/Quint/line28run.qnt
new file mode 100644
index 000000000..741481c32
--- /dev/null
+++ b/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
+    })
+}
+
+}
\ No newline at end of file