Skip to content

Commit

Permalink
refactored tests from asyncModelsTest except disagreement
Browse files Browse the repository at this point in the history
  • Loading branch information
josef-widder committed Dec 11, 2023
1 parent f040dbc commit b71b527
Show file tree
Hide file tree
Showing 4 changed files with 85 additions and 18 deletions.
4 changes: 3 additions & 1 deletion Specs/Quint/TendermintDSL.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,10 @@ run onlyProposerReceivesProposal (active, valList, valset, h, r, value) = {
})
}

// TODO: add valid round
run everyoneReceivesProposal (active, valList, valset, h, r, value) = {
val p = Proposer (valset, h, r)
val propMsg = { height: h, proposal: value, round: r, src: p, validRound: -1 }
setNextValueToPropose(p, value)
.then(ListTakeAStep(active))
.then(all{ // after new round an empty step to clean step "propose"
Expand All @@ -60,7 +62,7 @@ run everyoneReceivesProposal (active, valList, valset, h, r, value) = {
})
.then(all {
assert(true),
ListDeliverSomeProposal(active)
ListDeliverProposal(active, propMsg)
})
.then(ListTakeAStep(active))
.then(all{
Expand Down
2 changes: 1 addition & 1 deletion Specs/Quint/asyncModelsTest.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ run ThreeDecideInRound1V4stillinZeroOld = {
})
}

run DecideForFutureRoundTest = {
run DecideForFutureRoundOld = {
ThreeDecideInRound1V4stillinZeroOld
.then(N4F0::deliverProposal("v4", { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
.then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
Expand Down
88 changes: 72 additions & 16 deletions Specs/Quint/someMultiRoundRuns.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ run AllButOneDecideInR1WhileSlowInR0 = {
val nextProposer = Proposer (validatorSet, 0, 1)
val thisProposer = Proposer (validatorSet, 0, 0)
init
.then(reps(2, _ => valStep(slow))) // enter round 0 and consume step change
.then(onlyProposerReceivesProposal(others, validatorList, validatorSet, 0, 0, "blue"))

// receive all prevotes
Expand All @@ -28,22 +29,77 @@ run AllButOneDecideInR1WhileSlowInR0 = {
ListTakeAStep(others)
})
.then( ListDeliverAllVotes ("Precommit", others, others, validatorSet, 0, 0, "nil"))

// // 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
// })
.then(others.length().reps(_ => ListTakeAStep(others)))
// Others now go to next round on timeoutPrecommit
.then(all{
assert(SetFromList(others).forall(proc => system.get(proc).timeout.contains(("TimeoutPrecommit", 0, 0)))),
everyoneReceivesProposal (others, validatorList, validatorSet, 0, 1, "green")
})
.then(fromPrevoteToPrecommit (others, others, validatorList, validatorSet, 0, 1, "green"))
.then(ListDeliverAllVotes("Precommit", others, others, validatorSet, 0, 1, "green"))
.then(others.length().reps(_ => ListTakeAStep(correctList)))
.then(all {
assert(SetFromList(others).forall(proc => system.get(proc).es.chain.head() == "green")),
unchangedAll
})
}

run DecideForFutureRoundRun = {
val nextProposer = Proposer (validatorSet, 0, 1)
AllButOneDecideInR1WhileSlowInR0
.then(deliverProposal(slow, { height: 0, proposal: "green", round: 1, src: nextProposer, validRound: -1 }))
.then(valStep(slow))
.then(ProcessDeliverAllVotes("Precommit", slow, others, validatorSet, 0, 1, "green"))
.then(2.reps(_ => valStep(slow))) // TODO parameterize the 2 away
.then(all { // slow skipped to round 1
assert(system.get(slow).es.pendingStepChange == "propose" and system.get(slow).es.cs.round == 1),
valStep(slow) // now it processes the step change and discovers the proposal -> it prevotes
})
.then(all {
assert(system.get(slow).es.pendingStepChange == "Prevote"),
valStep(slow) // now it consumes the step change, but nothing happens
})
.then(valStep(slow)) // it receives the final precommit and decides
.then(all {
assert(validators.forall(proc => system.get(proc).es.chain.head() == "green")),
unchangedAll
})
}

run DecideForFutureRoundPrecommitFirstRun = {
val nextProposer = Proposer (validatorSet, 0, 1)
AllButOneDecideInR1WhileSlowInR0
.then(ProcessDeliverAllVotes("Precommit", slow, others, validatorSet, 0, 1, "green"))
.then(2.reps(_ => valStep(slow))) // TODO parameterize the 2 away
.then(all { // slow skipped to round 1
assert(system.get(slow).es.pendingStepChange == "propose" and system.get(slow).es.cs.round == 1),
valStep(slow) // now it processes the step change but nothing happens
})
.then(valStep(slow)) // it receives the final precommit
.then(all {
assert(system.get(slow).timeout.contains(("TimeoutPrecommit", 0, 1))),
deliverProposal(slow, { height: 0, proposal: "green", round: 1, src: nextProposer, validRound: -1 })
})
.then(valStep(slow)) // receive proposal and decide
.then(all {
assert(validators.forall(proc => system.get(proc).es.chain.head() == "green")),
unchangedAll
})
}

run RoundswitchRun = {
AllButOneDecideInR1WhileSlowInR0
.then(deliverVote(slow, { height: 0, id: "green", round: 1, src: "v1", step: "Precommit" }))
.then(deliverVote(slow, { height: 0, id: "green", round: 1, src: "v2", step: "Prevote" })) //TODO parameterize to F
.then(valStep(slow))
.then(all {
assert(system.get(slow).es.cs.round == 0),
valStep(slow)})
.then(all {
assert(system.get(slow).es.cs.round == 1),
unchangedAll
})
}


}
9 changes: 9 additions & 0 deletions Specs/Quint/someMultiRoundTest.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,16 @@ run AllButOneTest = {
N4F0::AllButOneDecideInR1WhileSlowInR0
}

run DecideFutureRoundTest = {
N4F0::DecideForFutureRoundRun
}

run DecideForFutureRoundPrecommitFirstTest = {
N4F0::DecideForFutureRoundPrecommitFirstRun
}

run RoundswitchTest = {
N4F0::RoundswitchRun
}

}

0 comments on commit b71b527

Please sign in to comment.