completed the timeout test

Specs/Quint/executor.qnt

@@ -147,7 +147,6 @@ pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent)
         (es, defaultResult)  
 }
 
-// TODO: make sure only valid proposals are in es.proposals
 
 // We do this if the executor receives a Prevote
 pure def Prevote (es: ExecutorState, input: ExecutorInput,  eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = {
@@ -416,6 +415,7 @@ pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = {
         (state, defaultInput)
 }
 
+// This function can be used to control test runs better.
 pure def nextActionCommand (state: NodeState, command: str) : (NodeState, ExecutorInput) = {
     if (command == "start" and not(state.es.started))
         (state, { ...defaultInput, name: "start" })

Specs/Quint/statemachine.qnt

@@ -178,6 +178,7 @@ run DecidingRunTest = {
         valStepCommand("v3", "vote")
         })
     .then(all{
+    // validator 3 decided on "a block"
     assert(system.get("v3").es.chain.head() == "a block"),
     system' = system,
     _hist' = _hist
@@ -217,20 +218,18 @@ run TimeoutRunTest = {
     .then(valStepCommand("v1", "vote"))
     .then(valStepCommand("v1", "vote"))
     .then(valStepCommand("v1", "vote"))
-    // .then(valStepCommand("v1", "timeout"))
-    // .then(valStepCommand("v2", "timeout"))
-    // .then(valStepCommand("v3", "timeout"))
-    // .then(valStepCommand("v4", "timeout")) 
+    .then(valStepCommand("v4", "vote"))
+    .then(valStepCommand("v4", "vote"))
+    .then(valStepCommand("v4", "vote"))
+    .then(valStepCommand("v4", "vote"))
+    .then(valStepCommand("v4", "vote"))
+    .then(valStepCommand("v4", "timeout"))
+    .then(all {
+        // validator 4 timed out and went to round 1
+        assert(system.get("v4").es.cs.round == 1),
+        system' = system,
+        _hist' = _hist,
+    }) 
 }
 
-/*
-valStepCommand("v1", "start")
-valStepCommand("v2", "start")
-valStepCommand("v3", "start")
-valStepCommand("v4", "start")
-valStepCommand("v1", "timeout")
-valStepCommand("v2", "proposal")
-valStepCommand("v3", "timeout")
-valStepCommand("v4", "timeout")
-*/
 }