diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index e6d43ac9f..a02a76c90 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -25,7 +25,7 @@ module consensus { type ConsensusState = { p: Address, - height : Height, + height: Height, round: Round, step: Step, // NewRound, Propose, Prevote, Precommit, decided lockedRound: Round, @@ -56,38 +56,38 @@ module consensus { // For the initial state | NoConsensusInput // Setup the state-machine for a single-height execution - | NewHeightConInput(Height) + | NewHeightCInput(Height) // Start a new round, not as proposer. - | NewRoundConInput(Round) + | NewRoundCInput(Round) // Start a new round as proposer with the proposed Value. - | NewRoundProposerConInput((Round, NonNilValue)) + | NewRoundProposerCInput((Round, NonNilValue)) // Receive a proposal without associated valid round. - | ProposalConInput((Round, Value)) + | ProposalCInput((Round, Value)) // Receive a valid proposal with an associated valid round, attested by a a Polka(vr). - | ProposalAndPolkaPreviousAndValidConInput((Value, Round)) + | ProposalAndPolkaPreviousAndValidCInput((Value, Round)) // Receive an invalid proposal: L26 and L32 when isValid(v) == false - | ProposalInvalidConInput + | ProposalInvalidCInput // Receive +2/3 prevotes for nil. - | PolkaNilConInput + | PolkaNilCInput // Receive +2/3 prevotes from different validators, not for the same value or nil. - | PolkaAnyConInput + | PolkaAnyCInput // Proposal and 2/3+ prevotes for the proposal: L36 when valid and step >= prevote - | ProposalAndPolkaAndValidConInput(Value) + | ProposalAndPolkaAndValidCInput(Value) // Receive +2/3 precommits from different validators, not for the same value or nil. - | PrecommitAnyConInput + | PrecommitAnyCInput // Proposal and 2/3+ commits for the proposal => decision - | ProposalAndCommitAndValidConInput(Value) + | ProposalAndCommitAndValidCInput(Value) // Receive +1/3 messages from different validators for a higher round. - | RoundSkipConInput(Round) + | RoundSkipCInput(Round) // Timeout waiting for proposal. - | TimeoutProposeConInput((Height, Round)) + | TimeoutProposeCInput((Height, Round)) // Timeout waiting for prevotes for a value. - | TimeoutPrevoteConInput((Height, Round)) + | TimeoutPrevoteCInput((Height, Round)) // Timeout waiting for precommits for a value. - | TimeoutPrecommitConInput((Height, Round)) + | TimeoutPrecommitCInput((Height, Round)) // found after Montebello // TODO: Discuss what to do about it - | ProposalAndPolkaAndInvalidConInput((Height, Round, Value)) + | ProposalAndPolkaAndInvalidCInput((Height, Round, Value)) // ************************************************************************* // Consensus output @@ -145,13 +145,13 @@ module consensus { | NoConsensusInput => state.toErrorOutput("NoConsensusInput is not a valid consensus input") - | NewHeightConInput(h) => + | NewHeightCInput(h) => if (h > state.height) initConsensusState(state.p, h).toNoConsensusOutput() else state.toNoConsensusOutput() // line 11.14 - | NewRoundProposerConInput(round_value) => + | NewRoundProposerCInput(round_value) => val r = round_value._1 val v = round_value._2 if (r > state.round) @@ -164,7 +164,7 @@ module consensus { // line 11.20 // TODO: discuss comment "ev.round must match state.round" - | NewRoundConInput(r) => + | NewRoundCInput(r) => if (r > state.round) // We just report that a timeout should be started. The executor must take care // of figuring out whether it needs to record the round number and height per @@ -180,7 +180,7 @@ module consensus { // - the value has been checked to be valid // - it is for the current round // The executor checks this upon receiving a propose message "ProposalMsg" - | ProposalConInput(round_value) => + | ProposalCInput(round_value) => val r = round_value._1 val v = round_value._2 if (state.step == ProposeStep) @@ -192,18 +192,18 @@ module consensus { state .with("step", PrevoteStep) .toPrevoteOutput(state.p, state.height, state.round, Nil) // line 26 - else state.toErrorOutput("ProposalConInput when not in ProposeStep") + else state.toErrorOutput("ProposalCInput when not in ProposeStep") // line 26 - | ProposalInvalidConInput => + | ProposalInvalidCInput => if (state.step == ProposeStep) state .with("step", PrevoteStep) .toPrevoteOutput(state.p, state.height, state.round, Nil) - else state.toErrorOutput("ProposalConInput when not in ProposeStep") + else state.toErrorOutput("ProposalCInput when not in ProposeStep") // line 28 - | ProposalAndPolkaPreviousAndValidConInput(value_vr) => + | ProposalAndPolkaPreviousAndValidCInput(value_vr) => val v = value_vr._1 val vr = value_vr._2 if (state.step == ProposeStep and vr >= 0 and vr < state.round) // line 28 @@ -215,21 +215,21 @@ module consensus { state .with("step", PrevoteStep) // line 33 .toPrevoteOutput(state.p, state.height, state.round, Nil) // line 32 - else state.toErrorOutput("ProposalAndPolkaPreviousAndValidConInput") + else state.toErrorOutput("ProposalAndPolkaPreviousAndValidCInput") // TODO: should we add the event to pending in this case. We would need to // do this in the executor // line 34 - | PolkaAnyConInput => + | PolkaAnyCInput => if (state.step == PrevoteStep) // We just report that a timeout should be started. The executor must take care // of figuring out whether it needs to record the round number and height per // timeout state.toTimeoutOutput(PrevoteTimeout) - else state.toErrorOutput("PolkaAnyConInput when not in PrevoteStep") + else state.toErrorOutput("PolkaAnyCInput when not in PrevoteStep") // line 36 - | ProposalAndPolkaAndValidConInput(v) => + | ProposalAndPolkaAndValidCInput(v) => match state.step { | PrevoteStep => state @@ -247,51 +247,51 @@ module consensus { .with("validValue", v) // line 42 .with("validRound", state.round) // line 43 .toNoConsensusOutput() - | _ => state.toErrorOutput("ProposalAndPolkaAndValidConInput when not in PrevoteStep or PrecommitStep") + | _ => state.toErrorOutput("ProposalAndPolkaAndValidCInput when not in PrevoteStep or PrecommitStep") } // line 44 - | PolkaNilConInput => + | PolkaNilCInput => if (state.step == PrevoteStep) state .with("step", PrecommitStep) .toPrecommitOutput(state.p, state.height, state.round, Nil) - else state.toErrorOutput("PolkaNilConInput when not in PrevoteStep") + else state.toErrorOutput("PolkaNilCInput when not in PrevoteStep") // line 47 - | PrecommitAnyConInput => + | PrecommitAnyCInput => state.toTimeoutOutput(PrecommitTimeout) // line 49 - | ProposalAndCommitAndValidConInput(v) => + | ProposalAndCommitAndValidCInput(v) => if (state.step != DecidedStep) state .with("step", DecidedStep) .toDecidedOutput(v) - else state.toErrorOutput("ProposalAndCommitAndValidConInput when in DecidedStep") + else state.toErrorOutput("ProposalAndCommitAndValidCInput when in DecidedStep") - | ProposalAndPolkaAndInvalidConInput => + | ProposalAndPolkaAndInvalidCInput => // TODO state.toNoConsensusOutput() // line 55 - | RoundSkipConInput(r) => + | RoundSkipCInput(r) => if (r > state.round) state.toSkipRoundOutput(r) - else state.toErrorOutput("RoundSkipConInput for round not bigger than current round") + else state.toErrorOutput("RoundSkipCInput for round not bigger than current round") // line 57 - | TimeoutProposeConInput(height_round) => + | TimeoutProposeCInput(height_round) => val h = height_round._1 val r = height_round._2 if (h == state.height and r == state.round and state.step == ProposeStep) state .with("step", PrevoteStep) .toPrevoteOutput(state.p, state.height, state.round, Nil) - else state.toErrorOutput("TimeoutProposeConInput") + else state.toErrorOutput("TimeoutProposeCInput") // line 61 - | TimeoutPrevoteConInput(height_round) => + | TimeoutPrevoteCInput(height_round) => val h = height_round._1 val r = height_round._2 if (h == state.height and r == state.round and state.step == PrevoteStep) @@ -299,17 +299,17 @@ module consensus { state .with("step", PrecommitStep) .toPrecommitOutput(state.p, state.height, state.round, Nil) - else state.toErrorOutput("TimeoutPrevoteConInput") + else state.toErrorOutput("TimeoutPrevoteCInput") // line 65 - | TimeoutPrecommitConInput(height_round) => + | TimeoutPrecommitCInput(height_round) => val h = height_round._1 val r = height_round._2 if (h == state.height and r == state.round) // TODO: here we should call newRound. For this we would need to know whether // we are proposer for next round. state.toSkipRoundOutput(state.round + 1) - else state.toErrorOutput("TimeoutPrecommitConInput") + else state.toErrorOutput("TimeoutPrecommitCInput") } diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt index 07e8ba69e..f8620ebe2 100644 --- a/Specs/Quint/consensusTest.qnt +++ b/Specs/Quint/consensusTest.qnt @@ -36,22 +36,22 @@ module consensusTest { nondet v = oneOf(Set("A", "B", "C")) nondet vr = oneOf(Set(-1, 1, 2, 3, 4)) any { - fireInput("Josef", NewHeightConInput(h)), - fireInput("Josef", NewRoundConInput(r)), - fireInput("Josef", NewRoundProposerConInput((r, v))), - fireInput("Josef", ProposalConInput((r, Val(v)))), - fireInput("Josef", ProposalAndPolkaPreviousAndValidConInput((Val(v), r))), - fireInput("Josef", ProposalInvalidConInput), - fireInput("Josef", PolkaNilConInput), - fireInput("Josef", PolkaAnyConInput), - fireInput("Josef", ProposalAndPolkaAndValidConInput(Val(v))), - fireInput("Josef", PrecommitAnyConInput), - fireInput("Josef", ProposalAndCommitAndValidConInput(Val(v))), - fireInput("Josef", RoundSkipConInput(r)), - fireInput("Josef", TimeoutProposeConInput((h, r))), - fireInput("Josef", TimeoutPrevoteConInput((h, r))), - fireInput("Josef", TimeoutPrecommitConInput((h, r))), - fireInput("Josef", ProposalAndPolkaAndInvalidConInput((h, r, Val(v)))), + fireInput("Josef", NewHeightCInput(h)), + fireInput("Josef", NewRoundCInput(r)), + fireInput("Josef", NewRoundProposerCInput((r, v))), + fireInput("Josef", ProposalCInput((r, Val(v)))), + fireInput("Josef", ProposalAndPolkaPreviousAndValidCInput((Val(v), r))), + fireInput("Josef", ProposalInvalidCInput), + fireInput("Josef", PolkaNilCInput), + fireInput("Josef", PolkaAnyCInput), + fireInput("Josef", ProposalAndPolkaAndValidCInput(Val(v))), + fireInput("Josef", PrecommitAnyCInput), + fireInput("Josef", ProposalAndCommitAndValidCInput(Val(v))), + fireInput("Josef", RoundSkipCInput(r)), + fireInput("Josef", TimeoutProposeCInput((h, r))), + fireInput("Josef", TimeoutPrevoteCInput((h, r))), + fireInput("Josef", TimeoutPrecommitCInput((h, r))), + fireInput("Josef", ProposalAndPolkaAndInvalidCInput((h, r, Val(v)))), } action unchangedAll = all { @@ -71,58 +71,58 @@ module consensusTest { // This test should call each input type at least once run DecideNonProposerTest = initFor(Set("Josef")) - .then(fireInput("Josef", NewRoundConInput(0))) + .then(fireInput("Josef", NewRoundCInput(0))) .then(_assert(_output == TimeoutOutput(ProposeTimeout))) - .then(fireInput("Josef", ProposalConInput((0, Val("block"))))) + .then(fireInput("Josef", ProposalCInput((0, Val("block"))))) .then(_assert(_output.isVoteMsgWith(Prevote, Val("block")))) - .then(fireInput("Josef", ProposalAndPolkaAndValidConInput(Val("block")))) + .then(fireInput("Josef", ProposalAndPolkaAndValidCInput(Val("block")))) .then(_assert(_output.isVoteMsgWith(Precommit, Val("block")))) - .then(fireInput("Josef", ProposalAndCommitAndValidConInput(Val("block")))) + .then(fireInput("Josef", ProposalAndCommitAndValidCInput(Val("block")))) .then(_assert(_output == DecidedOutput(Val("block")))) - .then(fireInput("Josef", NewHeightConInput(system.get("Josef").height + 1))) + .then(fireInput("Josef", NewHeightCInput(system.get("Josef").height + 1))) .then(_assert(system.get("Josef").height == 2)) - .then(fireInput("Josef", NewRoundProposerConInput((0, "nextBlock")))) + .then(fireInput("Josef", NewRoundProposerCInput((0, "nextBlock")))) .then(_assert(_output == ProposalOutput(mkProposal("Josef", 2, 0, "nextBlock", -1)))) - .then(fireInput("Josef", ProposalConInput((0, Val("nextBlock"))))) // it is assumed that the proposer receives its own message + .then(fireInput("Josef", ProposalCInput((0, Val("nextBlock"))))) // it is assumed that the proposer receives its own message .then(_assert(_output.isVoteMsgWith(Prevote, Val("nextBlock")) and system.get("Josef").step == PrevoteStep)) - .then(fireInput("Josef", PolkaAnyConInput)) + .then(fireInput("Josef", PolkaAnyCInput)) .then(_assert(_output == TimeoutOutput(PrevoteTimeout))) - .then(fireInput("Josef", TimeoutPrevoteConInput((2, 0)))) + .then(fireInput("Josef", TimeoutPrevoteCInput((2, 0)))) .then(_assert(_output.isVoteMsgWith(Precommit, Nil) and system.get("Josef").step == PrecommitStep)) - .then(fireInput("Josef", PrecommitAnyConInput)) + .then(fireInput("Josef", PrecommitAnyCInput)) .then(_assert(_output == TimeoutOutput(PrecommitTimeout))) - .then(fireInput("Josef", TimeoutPrecommitConInput((2, 0)))) + .then(fireInput("Josef", TimeoutPrecommitCInput((2, 0)))) .then(_assert(_output == SkipRoundOutput(1))) - .then(fireInput("Josef", NewRoundConInput(1))) + .then(fireInput("Josef", NewRoundCInput(1))) .then(_assert(_output == TimeoutOutput(ProposeTimeout))) - .then(fireInput("Josef", TimeoutProposeConInput((2, 1)))) + .then(fireInput("Josef", TimeoutProposeCInput((2, 1)))) .then(_assert(_output.isVoteMsgWith(Prevote, Nil) and system.get("Josef").step == PrevoteStep)) - .then(fireInput("Josef", PolkaNilConInput)) + .then(fireInput("Josef", PolkaNilCInput)) .then(_assert(_output.isVoteMsgWith(Precommit, Nil) and system.get("Josef").step == PrecommitStep)) - .then(fireInput("Josef", PrecommitAnyConInput)) + .then(fireInput("Josef", PrecommitAnyCInput)) .then(_assert(_output == TimeoutOutput(PrecommitTimeout))) - .then(fireInput("Josef", TimeoutPrecommitConInput((2, 1)))) + .then(fireInput("Josef", TimeoutPrecommitCInput((2, 1)))) .then(_assert(_output == SkipRoundOutput(2))) - .then(fireInput("Josef", NewRoundConInput(2))) + .then(fireInput("Josef", NewRoundCInput(2))) .then(_assert(_output == TimeoutOutput(ProposeTimeout))) - .then(fireInput("Josef", ProposalInvalidConInput)) + .then(fireInput("Josef", ProposalInvalidCInput)) .then(_assert(_output.isVoteMsgWith(Prevote, Nil) and system.get("Josef").step == PrevoteStep)) } diff --git a/Specs/Quint/driver.qnt b/Specs/Quint/driver.qnt index 8762446a4..0bebd10de 100644 --- a/Specs/Quint/driver.qnt +++ b/Specs/Quint/driver.qnt @@ -144,28 +144,29 @@ pure def callConsensus(es: DriverState, bk: Bookkeeper, csInput: ConsensusInput) ({ ...es, bk: bk, cs: res.cs, executedInputs: csInputs }, res.out) // We do this if the driver receives a Precommit +// TODO: vote can be removed because the vote data is already in vkOutput. pure def precommit(es: DriverState, vote: Vote, vkOutput: VoteKeeperOutput): (DriverState, ConsensusOutput) = match vkOutput { | PrecommitValueVKOutput(round_value) => - val round = round_value._1 - val value = round_value._2 - if (es.existsProposal(round, value)) - callConsensus(es, es.bk, ProposalAndCommitAndValidConInput(vote.valueId)) - else if (round == es.cs.round) - callConsensus(es, es.bk, PrecommitAnyConInput) - else if (round > es.cs.round) + val r = round_value._1 + val v = round_value._2 + if (es.existsProposal(r, v)) + callConsensus(es, es.bk, ProposalAndCommitAndValidCInput(vote.valueId)) + else if (r == es.cs.round) + callConsensus(es, es.bk, PrecommitAnyCInput) + else if (r > es.cs.round) // if it is for a future round I can trigger skipround // TODO: should we really do this. It is dead code as the f+1 event already happened - callConsensus(es, es.bk, RoundSkipConInput(vote.round)) + callConsensus(es, es.bk, RoundSkipCInput(vote.round)) // ignore messages from past rounds else (es, NoConsensusOutput) - | PrecommitAnyVKOutput(round) => - if (round == es.cs.round) - callConsensus(es, es.bk, PrecommitAnyConInput) + | PrecommitAnyVKOutput(r) => + if (r == es.cs.round) + callConsensus(es, es.bk, PrecommitAnyCInput) else (es, NoConsensusOutput) - | SkipVKOutput(round) => - if (round > es.cs.round) - callConsensus(es, es.bk, RoundSkipConInput(vote.round)) + | SkipVKOutput(r) => + if (r > es.cs.round) + callConsensus(es, es.bk, RoundSkipCInput(vote.round)) else (es, NoConsensusOutput) // none of the supported Precommit events. Do nothing | _ => (es, NoConsensusOutput) @@ -177,39 +178,39 @@ pure def prevote(es: DriverState, vkOutput: VoteKeeperOutput): (DriverState, Con // TODO: Polka implications missing. match vkOutput { | PolkaValueVKOutput(round_value) => - val round = round_value._1 - val value = round_value._2 - if (round < es.cs.round and es.existsProposalValid(es.cs.round, value, round)) + val r = round_value._1 + val v = round_value._2 + if (r < es.cs.round and es.existsProposalValid(es.cs.round, v, r)) // TODO: the value should come from the proposal - callConsensus(es, es.bk, ProposalAndPolkaPreviousAndValidConInput((value, round))) - else if (round == es.cs.round) - if (es.existsProposal(es.cs.round, value)) - val pending = (ProposalAndPolkaAndValidConInput(Val(value)), es.cs.height, es.cs.round) + callConsensus(es, es.bk, ProposalAndPolkaPreviousAndValidCInput((v, r))) + else if (r == es.cs.round) + if (es.existsProposal(es.cs.round, v)) + val pending = (ProposalAndPolkaAndValidCInput(Val(v)), es.cs.height, es.cs.round) val newES = { ...es, pendingInputs: es.pendingInputs.union(Set(pending)) } - callConsensus(newES, es.bk, PolkaAnyConInput) + callConsensus(newES, es.bk, PolkaAnyCInput) else // there is no matching proposal - callConsensus(es, es.bk, PolkaAnyConInput) + callConsensus(es, es.bk, PolkaAnyCInput) // It is for a future round // TODO: we might check whether it is for a future round and jump else (es, NoConsensusOutput) - | PolkaAnyVKOutput(round) => - if (round == es.cs.round) + | PolkaAnyVKOutput(r) => + if (r == es.cs.round) // call consensus and remember that we did it - callConsensus(es, es.bk, PolkaAnyConInput) + callConsensus(es, es.bk, PolkaAnyCInput) // TODO: we might check whether it is for a future round and jump else (es, NoConsensusOutput) - | PolkaNilVKOutput(round) => - if (round == es.cs.round) - callConsensus(es, es.bk, PolkaNilConInput) + | PolkaNilVKOutput(r) => + if (r == es.cs.round) + callConsensus(es, es.bk, PolkaNilCInput) else (es, NoConsensusOutput) - | SkipVKOutput(round) => - if (round > es.cs.round) - callConsensus(es, es.bk, RoundSkipConInput(round)) + | SkipVKOutput(r) => + if (r > es.cs.round) + callConsensus(es, es.bk, RoundSkipCInput(r)) else (es, NoConsensusOutput) | _ => (es, NoConsensusOutput) @@ -220,9 +221,9 @@ pure def handleTimeout(es: DriverState, t: Timeout): (DriverState, ConsensusOutp // TODO: We assume that the timeout event is always for the current round. If this is not // the case, we need to encode it in the input to which round the timeout belongs match t { - | ProposeTimeout => callConsensus(es, es.bk, TimeoutProposeConInput((es.cs.height, es.cs.round))) - | PrevoteTimeout => callConsensus(es, es.bk, TimeoutPrevoteConInput((es.cs.height, es.cs.round))) - | PrecommitTimeout => callConsensus(es, es.bk, TimeoutPrecommitConInput((es.cs.height, es.cs.round))) + | ProposeTimeout => callConsensus(es, es.bk, TimeoutProposeCInput((es.cs.height, es.cs.round))) + | PrevoteTimeout => callConsensus(es, es.bk, TimeoutPrevoteCInput((es.cs.height, es.cs.round))) + | PrecommitTimeout => callConsensus(es, es.bk, TimeoutPrecommitCInput((es.cs.height, es.cs.round))) } // We do this if the driver receives a proposal @@ -241,7 +242,7 @@ pure def handleProposal(es: DriverState, proposal: Proposal): (DriverState, Cons // we have a commit that matches the proposal. We don't need to compare against // es.cs.round // TODO: check heights in bookkeeper - callConsensus(newES, newES.bk, ProposalAndCommitAndValidConInput(Val(proposal.proposal))) + callConsensus(newES, newES.bk, ProposalAndCommitAndValidCInput(Val(proposal.proposal))) else if (proposal.round != es.cs.round or proposal.height != es.cs.height) // the proposal is from the right proposer and valid, but not for this round // keep the proposal, do nothing else @@ -253,25 +254,28 @@ pure def handleProposal(es: DriverState, proposal: Proposal): (DriverState, Cons val receivedPolkaCurrentVal = checkThreshold(newES.bk, newES.cs.round, Prevote, th) val receivedCommitCurrentVal = checkThreshold(newES.bk, newES.cs.round, Precommit, th) val propId: ValueId = id(Val(proposal.proposal)) + + // TODO: remove this definition when Quint supports multiple cases in one branch of the match statement. val prevoteAndprecommitOutput: (DriverState, ConsensusOutput) = if (receivedCommitCurrentVal) // here we need to call both, Commit and Polka. // We do commit and append polka to pending - val pending = (ProposalAndPolkaAndValidConInput(propId), newES.cs.height, newES.cs.round) + val pending = (ProposalAndPolkaAndValidCInput(propId), newES.cs.height, newES.cs.round) val newES2 = { ...newES, pendingInputs: newES.pendingInputs.union(Set(pending))} - callConsensus(newES2, newES.bk, ProposalAndCommitAndValidConInput(propId)) + callConsensus(newES2, newES.bk, ProposalAndCommitAndValidCInput(propId)) else if (receivedPolkaCurrentVal) - callConsensus(newES, newES.bk, ProposalAndPolkaAndValidConInput(propId)) + callConsensus(newES, newES.bk, ProposalAndPolkaAndValidCInput(propId)) else (newES, NoConsensusOutput) + match newES.cs.step { | ProposeStep => if (proposal.validRound == -1) if (receivedPolkaCurrentVal) - callConsensus(newES, newES.bk, ProposalAndPolkaAndValidConInput(propId)) + callConsensus(newES, newES.bk, ProposalAndPolkaAndValidCInput(propId)) else - callConsensus(newES, newES.bk, ProposalConInput((proposal.round, propId))) + callConsensus(newES, newES.bk, ProposalCInput((proposal.round, propId))) else if (receivedPolkaValidRoundVal) - callConsensus(newES, newES.bk, ProposalAndPolkaPreviousAndValidConInput((propId, proposal.validRound))) + callConsensus(newES, newES.bk, ProposalAndPolkaPreviousAndValidCInput((propId, proposal.validRound))) else (newES, NoConsensusOutput) | PrevoteStep => prevoteAndprecommitOutput @@ -284,9 +288,9 @@ pure def handleProposal(es: DriverState, proposal: Proposal): (DriverState, Cons | ProposeStep => if (es.cs.round == proposal.round and es.cs.height == proposal.height) if (checkThreshold(es.bk, es.cs.round, Prevote, ValueThreshold(proposal.proposal))) - callConsensus(es, es.bk, ProposalAndPolkaAndInvalidConInput((es.cs.height, es.cs.round, id(Val(proposal.proposal))))) + callConsensus(es, es.bk, ProposalAndPolkaAndInvalidCInput((es.cs.height, es.cs.round, id(Val(proposal.proposal))))) else - callConsensus(es, es.bk, ProposalInvalidConInput) + callConsensus(es, es.bk, ProposalInvalidCInput) else (es, NoConsensusOutput) | _ => (es, NoConsensusOutput) } @@ -296,9 +300,9 @@ pure def skip(es: DriverState, r: Round): (DriverState, ConsensusOutput) = // line 15 val prop = if (es.cs.validValue != Nil) es.cs.validValue else es.getValue() if (Proposer(es.valset, es.cs.height, es.cs.round + 1) == es.cs.p) - callConsensus(es, es.bk, NewRoundProposerConInput((r, prop.getVal()))) + callConsensus(es, es.bk, NewRoundProposerCInput((r, prop.getVal()))) else - callConsensus(es, es.bk, NewRoundConInput(r)) + callConsensus(es, es.bk, NewRoundCInput(r)) // what do we do now in the new round? Shouldn't we look whether we can build an event. // TODO: compute pending events. @@ -345,10 +349,12 @@ pure def driver(es: DriverState, input: DriverInput) : (DriverState, ConsensusOu match input { | ProposalDInput(proposal) => val res = handleProposal(es, proposal) + val newState = res._1 + val conOut = res._2 match res._2 { - | DecidedOutput(value) => decided(res._1, res._2, value) - | SkipRoundOutput(round) => skip(res._1, round) - | _ => res + | DecidedOutput(v) => decided(newState, conOut, v) + | SkipRoundOutput(r) => skip(newState, r) + | _ => (newState, conOut) } | VoteDInput(vote) => match vote.voteType { @@ -357,40 +363,46 @@ pure def driver(es: DriverState, input: DriverInput) : (DriverState, ConsensusOu val newES = { ...es, bk: res.bookkeeper, voteKeeperOutput: res.output} // only a commit event can come here. val cons_res = precommit(newES, vote, res.output) - match cons_res._2 { - | DecidedOutput(value) => decided(cons_res._1, cons_res._2, value) // CHECK: second argument to `decided` was `res._2` of type VoteKeeperOutput - | SkipRoundOutput(round) => skip(cons_res._1, round) - | _ => cons_res // CHECK: this was `res` of type VoteKeeperOutput + val newState = cons_res._1 + val conOut = cons_res._2 + match conOut { + | DecidedOutput(v) => decided(newState, conOut, v) // CHECK: second argument to `decided` was `res._2` of type VoteKeeperOutput + | SkipRoundOutput(r) => skip(newState, r) + | _ => (newState, conOut) // CHECK: originally this was `res` of type VoteKeeperOutput } | Prevote => val res = applyVote(es.bk, vote, es.valset.get(vote.srcAddress), es.cs.round) val newES = { ...es, bk: res.bookkeeper, voteKeeperOutput: res.output} // only a commit event can come here. val cons_res = prevote(newES, res.output) + val newState = cons_res._1 + val conOut = cons_res._2 match cons_res._2 { // TODO: dead branch. But we should put this after consensus call logic into a function - | DecidedOutput(value) => decided(cons_res._1, cons_res._2, value) // CHECK: second argument to `decided` was `res._2` of type VoteKeeperOutput - | SkipRoundOutput(round) => skip(cons_res._1, round) - | _ => cons_res // CHECK: this was `res` of type VoteKeeperOutput + | DecidedOutput(v) => decided(newState, conOut, v) // CHECK: second argument to `decided` was `res._2` of type VoteKeeperOutput + | SkipRoundOutput(r) => skip(newState, r) + | _ => (newState, conOut) // CHECK: originally this was `res` of type VoteKeeperOutput } } | TimeoutDInput(timeout) => val res = handleTimeout(es, timeout) + val newState = res._1 + val conOut = res._2 // result should be vote or skip - match res._2 { + match conOut { | SkipRoundOutput(round) => - skip(res._1, round) + skip(newState, round) // skip starts a new round. This may involve getValue. If we choose to move the getValue // logic out of the driver, we wouldn't call skip here but add a (to be defined) // DriverInput - | _ => res + | _ => (newState, conOut) } | StartDInput => - skip ({ ...es, started: true}, 0) - | PendingDInput(_) => - handlePendingInput(es) // CHECK: input not used? - | SetNextProposedValueDInput(value) => - es.setValue(Val(value)) + skip ({ ...es, started: true }, 0) + | PendingDInput(_) => // CHECK: why input is not used? + handlePendingInput(es) + | SetNextProposedValueDInput(v) => + es.setValue(Val(v)) | _ => (es, NoConsensusOutput) } diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/Quint/statemachineTest.qnt index a8a218b9d..e54e54cc6 100644 --- a/Specs/Quint/statemachineTest.qnt +++ b/Specs/Quint/statemachineTest.qnt @@ -126,7 +126,7 @@ action valStepCommand(v: Address, command: str) : bool = // _histSimple' = (v, input._2.name, res._2.name) } -run DecidingRunTest = { +run DecidingRunTest = init .then(setNextValueToPropose("v2", "a block")) .then(valStepCommand("v1", "start")) @@ -168,9 +168,7 @@ run DecidingRunTest = { assert(system.get("v3").es.chain.head() == Val("a block")), system' = system, _hist' = _hist - }) -} - + }) run TimeoutRunTest = { init