From 36db3e5129d19d3e69b5a8f7e9f8224f3097bb07 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 2 May 2022 15:28:50 +0200 Subject: [PATCH] PBTS: TLA+ aggreement consensus property fixed --- .../tla/TendermintPBT_001_draft.tla | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla index 2bcdecb27..a10695f39 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla @@ -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 ==