mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-08-21 22:56:22 +00:00
Code Issues Packages Projects Releases Wiki Activity

PBTS: TLA+ aggreement consensus property fixed

Browse Source
This commit is contained in:
Daniel Cason
2022-05-02 17:30:27 +02:00
committed by Daniel
parent f48ef7981a
commit 36db3e5129
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
+3 -3
View File
@@ -518,9 +518,9 @@ AgreementOnValue ==
\A p, q \in Corr:
/\ decision[p] /= NilDecision
/\ decision[q] /= NilDecision
=> \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds :
/\ decision[p] = Decision(v, t1, r1)
/\ decision[q] = Decision(v, t2, r2)
=> \E v \in ValidValues, t \in Timestamps, r1 \in Rounds, r2 \in Rounds :
/\ decision[p] = Decision(v, t, r1)
/\ decision[q] = Decision(v, t, r2)
\* [PBTS-INV-TIME-AGR.0]
AgreementOnTime ==