From 8062db960b4ac07117778253efdfbe3e72ff3b89 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 2 May 2022 15:29:59 +0200 Subject: [PATCH] PBTS/tla: aggreement on time removed because implicit --- .../tla/TendermintPBT_001_draft.tla | 8 -------- 1 file changed, 8 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 a10695f39..eeec32e9c 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla @@ -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 :