diff --git a/tests/raft_scenarios/replicate_deprecated b/tests/raft_scenarios/replicate_deprecated index 68c601a8b0a5..8d198afe29c9 100644 --- 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 index 566cca9efe25..851e532d039f 100644 --- 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 ]