Tweak PermittedLogChangesProp to permit a little more

achamayou · Nov 2, 2023 · 4431bd3 · 4431bd3
1 parent c5af7d9
commit 4431bd3
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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