diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla index ab9297751447..dc98d11e0ef0 100644 --- a/tla/ccfraft.tla +++ b/tla/ccfraft.tla @@ -755,10 +755,10 @@ AdvanceCommitIndex(i) == IN Send(msg) /\ UNCHANGED << currentTerm, votedFor, reconfigurationCount, removedFromConfiguration >> \* Otherwise, states remain unchanged - ELSE UNCHANGED <> + ELSE UNCHANGED <> \* Otherwise, Configuration and states remain unchanged - ELSE UNCHANGED <> - /\ UNCHANGED <> + ELSE UNCHANGED <> + /\ UNCHANGED <> \* CCF: RetiredLeader server i notifies the current commit level to server j \* This allows to retire gracefully instead of deadlocking the system through removing itself from the network.