refactor: use create_justification in the quint specification as in the informal spec #218
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.
What ❔
create_justification
instart_new_view
, instead of passing justifications directly.get_justification(view)
withcreate_justification()
inreplica.rs
to reflect the discussed changes.Why ❔
The pseudo code specification uses
create_justification
instart_new_view
andproposer_step
. The Quint specification was passing a justification directly instart_new_view
. These two approaches are not entirely equivalent.A falsy invariant
high_commit_and_timeout_qc_example
demonstrates that it's possible for a replica to have bothhigh_timeout_qc
andhigh_commit_qc
to have the same view. The model checker found an execution that demonstrates it.