diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt index dd1d505f8..5ec3391ea 100644 --- a/Specs/Quint/executor.qnt +++ b/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" }) diff --git a/Specs/Quint/statemachine.qnt b/Specs/Quint/statemachine.qnt index bec170c08..c20691f17 100644 --- a/Specs/Quint/statemachine.qnt +++ b/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") -*/ }