From bea77abe836e9377b01dab983c9aecd340ae650e Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Fri, 5 Jan 2024 11:53:42 +0000 Subject: [PATCH] Update tla/consensus/ccfraft.tla Co-authored-by: Heidi Howard <1835251+heidihoward@users.noreply.github.com> --- 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 5e0ae60c6b21..566cca9efe25 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -680,7 +680,7 @@ AdvanceCommitIndex(i) == IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum \* The function find_highest_possible_committable_index in raft.h returns the largest committable index \* in the current term (Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf explains why it has - \* to be the *current* term). Finding the largest index is an (mplementation-level) optimization that + \* to be the *current* term). Finding the largest index is an (implementation-level) optimization that \* reduces the number of AdvanceCommitIndex calls, but this optimization also shrinks this spec's state-space. \* \* Theoretically, any committable index in the current term works, i.e., highestCommittableIndex could be