Merge branch 'main' into tla-off-by-one

microsoft · Jan 8, 2024 · 1003ab4 · 1003ab4
2 parents 114acae + 6734750
commit 1003ab4
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -552,6 +552,7 @@ AppendEntries(i, j) ==
     \* No messages to itself and sender is primary
     /\ state[i] = Leader
     /\ i /= j
+    /\ j \in GetServerSet(i)
     \* AppendEntries must be sent for historical entries, unless
     \* snapshots are used. Whether the node is in configuration at
     \* that index makes no difference.