mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-05-19 21:51:31 +00:00
Code Issues Packages Projects Releases Wiki Activity

PBTS/tla: aggreement on time removed because implicit

Browse Source
This commit is contained in:
Daniel Cason
2022-05-02 15:29:59 +02:00
parent e94e9ed5e5
commit 8062db960b
1 changed files with 0 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
View File

@@ -522,14 +522,6 @@ AgreementOnValue ==
/\ decision[p] = Decision(v, t, r1)
/\ decision[q] = Decision(v, t, r2)
\* [PBTS-INV-TIME-AGR.0]
AgreementOnTime ==
\A p, q \in Corr:
\A v1 \in ValidValues, v2 \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r \in Rounds :
/\ decision[p] = Decision(v1, t1, r)
/\ decision[q] = Decision(v2, t2, r)
=> t1 = t2
\* [PBTS-CONSENSUS-TIME-VALID.0]
ConsensusTimeValid ==
\A p \in Corr, t \in Timestamps :