diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index bea8c646f3cb..cccc3e6744d9 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -504,8 +504,8 @@ InitReconfigurationVars == \* https://microsoft.github.io/CCF/main/operations/ledger_snapshot.html#join-or-recover-from-snapshot) or some stale configuration \* such as the initial configuration. A node's configuration is *never* "empty", i.e., the equivalent of configuration[node] = {} here. \* For simplicity, the set of servers/nodes all have the same initial configuration at startup. - /\ \E c \in SUBSET Servers \ {{}}: - configurations = [i \in Servers |-> [ j \in {0} |-> c ] ] + /\ \E s \in Servers: + configurations = [i \in Servers |-> 0 :> {s} ] InitMessagesVars == /\ Network!InitMessageVar