Clean votekeeper spec #69
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
josef-widder
added a commit
that referenced
this pull request
Nov 15, 2023
… voteKeeper (#40) * executor start * PreCommit function * TODOs * line 28 is in the books * prevote, precommit, and timeout done. proposal missing * starting to put things together for state machine * a somewhat complete version of the executor logic * state machine, but needs to be debugged * moving statemachine. problem with chooseSome * it moves * more things moving * some problem with bookkeeper * more things move * I have seen a Polka * cleanup * cleaning * successful test of statemachine * before consensus return refactor * first pending event added * cleaned consensus * commit to merge with Manuel's updated votekeeper * to merge Daniel's comment * executor start * PreCommit function * TODOs * line 28 is in the books * prevote, precommit, and timeout done. proposal missing * starting to put things together for state machine * a somewhat complete version of the executor logic * state machine, but needs to be debugged * moving statemachine. problem with chooseSome * it moves * more things moving * some problem with bookkeeper * more things move * I have seen a Polka * cleanup * cleaning * successful test of statemachine * before consensus return refactor * first pending event added * cleaned consensus * commit to merge with Manuel's updated votekeeper * to merge Daniel's comment * addressed Daniel's comments * addressed Daniel's comments and run tests * completed the timeout test * clean up and comments * added checks for increasing round numbers * added hash function checks * valset error thrown in test fixed * added action and logic to get value from the outside into the system * comments following the discussion on where to put the reponsibility for getValue * transformed that executed events into list * added an asynchronous execution environment * added round number checks to ProposalMsg * test for disagreement in asynchronous setting * Parameterization of the Asynchronous model * Typecheck all Quint specs on CI and run test for `consensustest.qnt` * Update Specs/Quint/AsyncModels.qnt Co-authored-by: Romain Ruetschi <[email protected]> * added a type invariant * updated syntax to Quint 0.14.4 * moved bookkeeper statemachine out for modularity * Update Quint test job * commented a line that failed a test. Need to discuss with Manu * Run test on all Quint files * Use script to run all tests even in the presence of failures * fixed the logic and the test for Precommit,Nil * Update Specs/Quint/voteBookkeeperTest.qnt Signed-off-by: Josef Widder <[email protected]> Co-authored-by: Hernán Vanzetto <[email protected]> * rename files for test CI * Update .github/workflows/quint.yml * renamed one more file with a test * module renamed * start with a test where a process enters round 1 and messages are already around * added todos * Pass over the votekeeper spec (#69) Co-authored-by: Josef Widder <[email protected]> --------- Co-authored-by: Romain Ruetschi <[email protected]> Co-authored-by: Hernán Vanzetto <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Typos, comments, new spells, a small refactoring with the new functions
hasQuorumOnValueandhasQuorumOnAny, and a general cleaning for better readability.