Skip to content

Commit

Permalink
Update tla/consensus/ccfraft.tla
Browse files Browse the repository at this point in the history
Co-authored-by: Heidi Howard <[email protected]>
  • Loading branch information
2 people authored and lemmy committed Jan 5, 2024
1 parent 51bb7b1 commit 8f06c5f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion tla/consensus/ccfraft.tla
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 8f06c5f

Please sign in to comment.