Conversation
* The file was actually moved to the PBTS spec repository
There was a problem hiding this comment.
Review
Great work! It is the first time I am reviewing this spec, so I went through everything (not only the changes introduced in this PR). I have opened issue #8628 with my feedback, to avoid polluting this PR with comments unrelated to the PR itself.
josef-widder
left a comment
There was a problem hiding this comment.
The log for the experiments and the readme that explains how to run them looks great, Thanks @Kukovec !
|
This pull request has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Thank you for your contributions. |
|
I moved this PR to the draft state because:
I assume this PR is from v0.36 milestone, so I will complete it by then. |
|
This pull request has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. Thank you for your contributions. |
I will let this PR be closed and start a new one. |
* Originally part of tendermint/tendermint#8600 * Ignoring large and temporary intermediate/ directories * Duplicated files were removed
Addresses #2019. [Spec entry point (rendered)](https://github.com/cometbft/cometbft/blob/cason/pbts-review/spec/consensus/proposer-based-timestamp/README.md) For some reason, Git is not tracking the renamed filed `pbts-algorithm*.md` properly. A better diff as follows: git diff --word-diff main:spec/consensus/proposer-based-timestamp/pbts-algorithm_002_draft.md cason/pbts-review:spec/consensus/proposer-based-timestamp/pbts-algorithm.md Relevant changes are accompanied by comments from the author. ### TLA+ verification A second contribution of this PR is to add the most recent TLA+ specification of consensus with PBTS, plus scripts, configurations, and the results of performed experiments. This was a manual backport of the content of the legacy `main-pbts` branch, as in tendermint/tendermint#8600. #### PR checklist - [ ] ~Tests written/updated~ - [ ] ~Changelog entry added in `.changelog` (we use [unclog](https://github.com/informalsystems/unclog) to manage our changelog)~ - [x] Updated relevant documentation (`docs/` or `spec/`) and code comments --------- Co-authored-by: glnro <8335464+glnro@users.noreply.github.com>
This PR updates the specification of PBTS, considering its implementation and availability in
v0.36.No actual technical content is included, but a general re-organization of the documentation of PBTS. In addition, the TLA+ specification was re-organized and some documentation for running the model checker was introduced.
Closes #8591.