From 8737003f9462eebfda36ed45091834d9113d3d2d Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@informal.systems>
Date: Tue, 16 Aug 2022 18:24:52 +0200
Subject: [PATCH] fix one part of the inductive invariant with Josef

---
 .../accountability/TendermintAccInv_004_draft.tla | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
index 5f9bfcf4e..875d4ecfa 100644
--- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
@@ -13,6 +13,7 @@ EXTENDS TendermintAcc_004_draft
 
 (************************** TYPE INVARIANT ***********************************)
 (* first, we define the sets of all potential messages *)
+\* @type: Set($proposeMsg);
 AllProposals ==
   [type: {"PROPOSAL"},
    src: AllProcs,
@@ -20,12 +21,14 @@ AllProposals ==
    proposal: ValuesOrNil,
    validRound: RoundsOrNil]
 
+\* @type: Set($preMsg);
 AllPrevotes ==
   [type: {"PREVOTE"},
    src: AllProcs,
    round: Rounds,
    id: ValuesOrNil]
 
+\* @type: Set($preMsg);
 AllPrecommits ==
   [type: {"PRECOMMIT"},
    src: AllProcs,
@@ -278,12 +281,14 @@ Senders(M) == { m.src: m \in M }
 \* then in the future rounds there are less than 2T + 1 prevotes for another value
 PrecommitsLockValue ==
   \A r \in Rounds:
-    \A v \in ValidValues \union {NilValue}:
-      \/ LET Precommits ==  {m \in msgsPrecommit[r]: m.id = v}
-        IN
-        Cardinality(Senders(Precommits)) < THRESHOLD1
+    \A v \in ValidValues:
+      \/ LET Precommits == {
+            m \in msgsPrecommit[r]: m.id = v /\ m.src \in Corr
+         }
+         IN
+         Cardinality(Senders(Precommits)) < THRESHOLD1
       \/ \A fr \in { rr \in Rounds: rr > r }:  \* future rounds
-          \A w \in (ValuesOrNil) \ {v}:
+          \A w \in ValuesOrNil \ {v}:
             LET Prevotes == {m \in msgsPrevote[fr]: m.id = w}
             IN
             Cardinality(Senders(Prevotes)) < THRESHOLD2