From 31b80216726d85b96ff8bcd006667b21f8baebf7 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@informal.systems>
Date: Tue, 23 Aug 2022 18:24:52 +0200
Subject: [PATCH] disable PrecommitsLockValue and weaken Accountability

---
 spec/light-client/accountability/TendermintAccInv_004_draft.tla | 2 +-
 spec/light-client/accountability/TendermintAcc_004_draft.tla    | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
index 5c8092583..0ab99545b 100644
--- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
@@ -369,11 +369,11 @@ Inv ==
     /\ IfSentPrecommitThenSentPrevote
     /\ IfSentPrecommitThenReceivedTwoThirds
     /\ AllNoEquivocationByCorrect
-    /\ PrecommitsLockValue
     /\ RelockValueIfEnoughPrevotes
     /\ AllIfValidRoundThenTwoThirds
     /\ AllValidAndLocked
     /\ AllIfValidRoundThenProposal
+    \*/\ PrecommitsLockValue
 
 \* this is the inductive invariant we like to check
 TypedInv == TypeOK /\ Inv
diff --git a/spec/light-client/accountability/TendermintAcc_004_draft.tla b/spec/light-client/accountability/TendermintAcc_004_draft.tla
index e9f3c03df..ef72b06c7 100644
--- a/spec/light-client/accountability/TendermintAcc_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAcc_004_draft.tla
@@ -495,7 +495,6 @@ EquivocationBy(p) ==
               /\ m2.src = p
               /\ m1.round = m2.round
     IN
-    \/ EquivocationIn(evidencePropose)
     \/ EquivocationIn(evidencePrevote)
     \/ EquivocationIn(evidencePrecommit)