First quint draft that is somewhat complete with consensus, executor, voteKeeper #40
Conversation
|
Looks like there are some conflicts in the vote keeper spec |
I fixed it. Also I needed to move out the votekeeper state machine into another file for modularity (we have the bookkeeper spec stored differently in the asynchonous state machine.) |
Specs/Quint/voteBookkeeper.qnt
Outdated
| @@ -116,13 +116,17 @@ module voteBookkeeper { | |||
| else if (voteType == "Prevote" and threshold.name == "Any") {round: round, name: "PolkaAny", value: "null"} | |||
| else if (voteType == "Precommit" and threshold.name == "Value") {round: round, name: "PrecommitValue", value: threshold.value} | |||
| else if (voteType == "Precommit" and threshold.name == "Any") {round: round, name: "PrecommitAny", value: "null"} | |||
| // Josef's addition | |||
| // else if (voteType == "Precommit" and threshold.name == "Nil") {round: round, name: "PrecommitAny", value: "null"} | |||
There was a problem hiding this comment.
@angbrav, I added this line at some point, because this case wasn't caught back then. With the line, one of your tests are failing. I wonder whether we need it, or whether the logic ensures that Nil precommits are counted under the Any thresholds.
If you don't know the answer, perhaps it makes sense to discuss on a call ;-)
There was a problem hiding this comment.
Look like there is another failure in statemachine.qnt:
/home/runner/work/malachite/malachite/Specs/Quint/statemachine.qnt:216:9 - error: [QNT508] Assertion failed
216: assert(system.get("v4").es.cs.round == 1),
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
There was a problem hiding this comment.
Thanks for pointing this out. I tried it locally: @angbrav 's tests work with line 120 commented out, my tests fail with the line commented out (and vice versa). We need to figure out what behavior we want.
There was a problem hiding this comment.
I just had a call with @angbrav and we fixed it and commited. line 120 is now part of the spec, and we fixed the test to the expected behavior.
.github/workflows/quint.yml
Outdated
| with: | ||
| node-version: "18" | ||
| - run: npm install -g @informalsystems/quint | ||
| - run: bash Scripts/quint-forall.sh test Specs/Quint/*.qnt |
There was a problem hiding this comment.
@romac , CI is complaining about failed tests: I guess we shouldn't run "quint test" on statemachineAsync.qnt as it has some const, and quint complains about "Uninitialized const validator". Indeed, AsyncModels.qnt imports statemachineAsync.qnt and gives values to these consts. Not sure what is the best way to set it up here so that ignores statemachineAsync.qnt.
There was a problem hiding this comment.
I have change the line to only run test on *Test.qnt and renamed the files that contain tests.
Signed-off-by: Josef Widder <josef@informal.systems> Co-authored-by: Hernán Vanzetto <15466498+hvanz@users.noreply.github.com>
Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>
I would in particular welcome feedback on the executor and what tests to add.