From 1cd989ca877c8cefae13d1e3d8c56a37efc8fc0a Mon Sep 17 00:00:00 2001
From: Josef Widder <josef@informal.systems>
Date: Tue, 28 Nov 2023 16:36:58 +0100
Subject: [PATCH] Overview over consensus logic covered with tests

---
 Specs/Quint/asyncModelsTest.qnt |  6 ++---
 Specs/Quint/coverage.md         | 43 +++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 3 deletions(-)
 create mode 100644 Specs/Quint/coverage.md

diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt
index 93a120eae..261f77afe 100644
--- a/Specs/Quint/asyncModelsTest.qnt
+++ b/Specs/Quint/asyncModelsTest.qnt
@@ -156,10 +156,10 @@ run RoundswitchTest = {
     ThreeDecideInRound1V4stillinZeroTest
     .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
     .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" })) 
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v4"))
     .then(N4F0::valStep("v4"))
+    .then(all {
+        assert(N4F0::system.get("v4").es.cs.round == 0),
+        N4F0::valStep("v4")})
     .then(all {
         assert(N4F0::system.get("v4").es.cs.round == 1),
         N4F0::unchangedAll
diff --git a/Specs/Quint/coverage.md b/Specs/Quint/coverage.md
new file mode 100644
index 000000000..f53280b1c
--- /dev/null
+++ b/Specs/Quint/coverage.md
@@ -0,0 +1,43 @@
+# Tests for consensus statemachine (and sometimes driver)
+
+## Overview over covered consensus algorithm lines
+
+| line | comment | (C) | test |
+|  -----:| ---- | -----| -----| 
+ 16 |  reuse valid value | | 
+ 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 |
+ 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  |
+ 45 | precommit nil | X2b
+ 48 | start timeoutPrecommit  | X2 , X2b
+ 51 | decide  | X1
+ 56 | skip round  | | (A) RoundswitchTest
+ 57 | OnTimeoutPropose  | X2b
+ 61 | OnTimeOutPrevote  | X2
+ 64 | OnTimeOutPrecommit  | X2, X2b
+ 
+## Comments
+
+- (C) 
+    - refers to DecideNonProposerTest in consensusTest.qnt. 
+    - X1 covered in height 1, X2b: covered in height 2 round 2, etc.
+    - is only containing the consensus state machine. No driver
+    - contains an event to go to height 1
+- (A) asyncModelsTest.qnt
+- ^1 ThreeDecideInRound1V4stillinZeroTest delivers proposal so it must have been sent before
+
+
+## Other tests
+
+- asyncModelsTest.qnt
+    - DisagreementTest: 2/4 faulty lead to disagreement
+    - three processes go to round 1 and decide, on process left behind. Test whether process decides
+        - DecideForFutureRoundTest: first receives proposal then precommits
+        - DecideOnProposalTest: first receives precommits then proposal
\ No newline at end of file