From ed6a9a28b042fc73afb9fa6070e4cce561821ee8 Mon Sep 17 00:00:00 2001 From: Heidi Howard <1835251+heidihoward@users.noreply.github.com> Date: Tue, 9 Jan 2024 10:54:25 +0000 Subject: [PATCH] missing increment in AppendEntriesBatchsize --- tla/consensus/ccfraft.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index 489d5ad182fe..e22e218e0f02 100644 --- 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) ==