From 0f88142bbc323b377ba602f507266701bd1eac6b Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Wed, 8 May 2024 16:29:19 +0000
Subject: [PATCH] Remove invariant

---
 tla/consensus/Traceccfraft.cfg | 7 +++----
 tla/consensus/Traceccfraft.tla | 3 ---
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg
index 613b6b173608..00cdeba9c11f 100644
--- a/tla/consensus/Traceccfraft.cfg
+++ b/tla/consensus/Traceccfraft.cfg
@@ -28,9 +28,8 @@ PROPERTIES
 PROPERTIES
     TraceMatched
 
-INVARIANTS 
+INVARIANT 
     TraceDifferentialInv
-    CommittableIndicesIsConstantSpaceInv
 
 CONSTRAINT
     TraceMatchesConstraints
@@ -93,5 +92,5 @@ CONSTANTS
     NodeFour = "3"
     NodeFive = "4"
 
-\* ALIAS 
-\*     TraceAlias
\ No newline at end of file
+ALIAS 
+    TraceAlias
\ No newline at end of file
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
index ae1ba925f1df..b4afe1119f3c 100644
--- a/tla/consensus/Traceccfraft.tla
+++ b/tla/consensus/Traceccfraft.tla
@@ -522,9 +522,6 @@ TraceMatchesConstraints ==
     /\ MembershipStateConsistentInv
     /\ CommitCommittableIndices
 
-CommittableIndicesIsConstantSpaceInv ==
-    "committable_indices" \in DOMAIN logline.msg.state => Len(logline.msg.state.committable_indices) <= 2
-
 -------------------------------------------------------------------------------------
 
 TraceDifferentialInv ==