missing increment in AppendEntriesBatchsize

microsoft · Jan 9, 2024 · ed6a9a2 · ed6a9a2
1 parent feb9d68
commit ed6a9a2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -451,7 +451,7 @@ CommittedTermPrefix(i, x) ==
 AppendEntriesBatchsize(i, j) ==
     \* The Leader is modeled to send zero to one entries per AppendEntriesRequest.
      \* This can be redefined to send bigger batches of entries.
-    {sentIndex[i][j]}
+    {sentIndex[i][j] + 1}
 
 
 PlausibleSucessorNodes(i) ==