Update tla/consensus/MCccfraft.tla

Co-authored-by: Heidi Howard <[email protected]>
microsoft · Oct 1, 2024 · 65aacf7 · 65aacf7
1 parent 5fc533a
commit 65aacf7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -143,7 +143,7 @@ DebugNotTooManySigsInv ==
 
 \* The inital log is up to 4 entries long + one log entry per request/reconfiguration + one signature per request/reconfiguration or new view (no consecutive sigs except across views)
 MaxLogLength == 
-    4 + ((MaxRequestCount + Len(Configurations)) * 2) + (StartTerm + MaxTermCount)
+    4 + ((MaxRequestCount + Len(Configurations)) * 2) + MaxTermCount
 
 MappingToAbs == 
   INSTANCE abs WITH