nextIndex unchanged on AE ACK

microsoft · Jan 8, 2024 · effaa85 · effaa85
1 parent ed9e178
commit effaa85
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/tests/raft_scenarios/replicate_deprecated b/tests/raft_scenarios/replicate_deprecated
@@ -13,6 +13,7 @@ dispatch_all
 state_all
 replicate,1,helloworld
 emit_signature,1
+emit_signature,1
 periodic_all,10
 dispatch_all
 periodic_all,1

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -921,7 +921,7 @@ HandleAppendEntriesResponse(i, j, m) ==
           /\ m.success \* successful
           \* max(...) because why would we ever want to go backwards on a success response?!
           /\ matchIndex' = [matchIndex EXCEPT ![i][j] = max(@, m.lastLogIndex)]
-          /\ nextIndex'  = [nextIndex  EXCEPT ![i][j] = max(@, m.lastLogIndex + 1)]
+          /\ UNCHANGED nextIndex
        \/ /\ \lnot m.success \* not successful
           /\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
              IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(min(tm, nextIndex[i][j]-1), matchIndex[i][j]) + 1 ]