Remove invariant

achamayou · May 8, 2024 · 0f88142 · 0f88142
1 parent 4720ac1
commit 0f88142
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git 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
+ALIAS 
+    TraceAlias
diff --git 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 ==