always define nextIndex

microsoft · Jan 8, 2024 · ba22ce9 · ba22ce9
1 parent da84648
commit ba22ce9
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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)