From 4de357953942f6e68849d977bbdca97b95444007 Mon Sep 17 00:00:00 2001 From: Josef Widder Date: Wed, 29 Nov 2023 16:09:43 +0100 Subject: [PATCH] DSL --- Specs/Quint/TendermintDSL.qnt | 48 +++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 Specs/Quint/TendermintDSL.qnt diff --git a/Specs/Quint/TendermintDSL.qnt b/Specs/Quint/TendermintDSL.qnt new file mode 100644 index 000000000..a07d729a2 --- /dev/null +++ b/Specs/Quint/TendermintDSL.qnt @@ -0,0 +1,48 @@ +// -*- mode: Bluespec; -*- + +module TendermintDSL { + +import statemachineAsync.* from "./statemachineAsync" +export statemachineAsync.* + +val validatorList = validators.fold(List(), (s, x) => s.append(x)) +val correctList = Correct.fold(List(), (s, x) => s.append(x)) +val faultyList = Faulty.fold(List(), (s, x) => s.append(x)) + +run ListTakeAStep (active) = { + active.length().reps(i => valStep(active[i])) +} + +run ListDeliverProposal (active, proposalMsg) = { + active.length().reps(i => deliverProposal(active[i], proposalMsg)) +} + +run ListDeliverSomeProposal (active) = { + active.length().reps(i => deliverSomeProposal(active[i])) +} + +run ProcessDeliverAllVotes (cstep, recepient, fromList, valset, h, r, value) = { + fromList.length().reps(i => deliverVote(recepient, { src: fromList[i], height: h, round: r, step: cstep, id: value })) +} + +run ListDeliverAllVotes (cstep, fromList, toList, valset, h, r, value) = { + toList.length().reps(i => ProcessDeliverAllVotes (cstep, toList[i], fromList, valset, h, r, value)) +} + + +run everyoneReceivesProposal (active, valList, valset, h, r, value) = { + val p = Proposer (valset, h, r) + setNextValueToPropose(p, value) + .then(ListTakeAStep(active)) + .then(all { + assert(true), + ListDeliverSomeProposal(active) + }) + .then(ListTakeAStep(active)) +} + + + + + +} \ No newline at end of file