-
Notifications
You must be signed in to change notification settings - Fork 15
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix(spec): agreement for multiple heights #749
Conversation
nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes)) | ||
deliverVote(v, vote), | ||
val props = propBuffer.get(v).union(AllFaultyProposals) | ||
all{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is a deliverSomeProposal
action in this file, with the same issue: it does not test if there is a proposal buffer to deliver.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This method, however, does not delivery faulty proposals.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The method is used in:
- ./tests/decideForPastRound/decideForPastRoundrun.qnt
- tests/line42/line42run.qnt
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the issue is solved.
I am not sure, however, where and how this invariant is actually tested.
nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes)) | ||
deliverVote(v, vote), | ||
val props = propBuffer.get(v).union(AllFaultyProposals) | ||
all{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This method, however, does not delivery faulty proposals.
nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes)) | ||
deliverVote(v, vote), | ||
val props = propBuffer.get(v).union(AllFaultyProposals) | ||
all{ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The method is used in:
- ./tests/decideForPastRound/decideForPastRoundrun.qnt
- tests/line42/line42run.qnt
Closes: #744
PR author checklist
For all contributors
For external contributors