diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index 9f0b9edd2b10..206781513918 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -1332,7 +1332,9 @@ PermittedLogChangesProp == \* Established leader adding new entries \/ /\ state[i] = Leader /\ state[i]' = Leader - /\ IsPrefix(log[i], log[i]') + /\ Len(log[i]') >= Len(log[i]) + \* Reconfiguration replaces the last entry + \* /\ IsPrefix(log[i], log[i]') \* Newly elected leader is truncating its log \/ /\ state[i] = Candidate /\ state[i]' = Leader