From 4431bd3f8cc9f08f28b569bd6eaddb2e443f00c2 Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Thu, 2 Nov 2023 10:36:45 +0000
Subject: [PATCH] Tweak PermittedLogChangesProp to permit a little more

---
 tla/consensus/ccfraft.tla | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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