From ba22ce999e6334ab3bf19f571c70db9c90475cc7 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Mon, 8 Jan 2024 18:07:38 +0000 Subject: [PATCH] always define nextIndex --- tla/consensus/ccfraft.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index 6feb8fec8ada..82ca34588614 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -647,7 +647,8 @@ ChangeConfigurationInt(i, newConfiguration) == /\ \A s \in newConfiguration: s \notin removedFromConfiguration \* See raft.h:2401, nodes are only sent future entries initially, they will NACK if necessary. \* This is because they are expected to start from a fairly recent snapshot, not from scratch. - /\ \A addedNode \in (newConfiguration \ CurrentConfiguration(i)) : nextIndex' = [nextIndex EXCEPT ![i][addedNode] = Len(log[i]) + 1] + /\ LET addedNodes == newConfiguration \ CurrentConfiguration(i) + IN IF Cardinality(addedNodes) > 0 THEN \A addedNode \in addedNodes : nextIndex' = [nextIndex EXCEPT ![i][addedNode] = Len(log[i]) + 1] ELSE nextIndex' = nextIndex \* Keep track of running reconfigurations to limit state space /\ reconfigurationCount' = reconfigurationCount + 1 /\ removedFromConfiguration' = removedFromConfiguration \cup (CurrentConfiguration(i) \ newConfiguration)