Skip to content

Commit

Permalink
Restrict initial configuration in ccfraft.tla to a single node (#5778)
Browse files Browse the repository at this point in the history
  • Loading branch information
heidihoward authored Oct 27, 2023
1 parent dc69318 commit 115d1af
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions tla/consensus/ccfraft.tla
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 115d1af

Please sign in to comment.