Align leadership state naming with implementation (#5823)

tla/consensus/MCccfraft.cfg

@@ -23,7 +23,7 @@ CONSTANTS
     Candidate = Candidate
     Leader = Leader
     RetiredLeader = RetiredLeader
-    Pending = Pending
+    None = None
 
     RequestVoteRequest = RequestVoteRequest
     RequestVoteResponse = RequestVoteResponse

tla/consensus/MCccfraftAtomicReconfig.cfg

@@ -23,7 +23,7 @@ CONSTANTS
     Candidate = Candidate
     Leader = Leader
     RetiredLeader = RetiredLeader
-    Pending = Pending
+    None = None
 
     RequestVoteRequest = RequestVoteRequest
     RequestVoteResponse = RequestVoteResponse

tla/consensus/MCccfraftWithReconfig.cfg

@@ -23,7 +23,7 @@ CONSTANTS
     Candidate = Candidate
     Leader = Leader
     RetiredLeader = RetiredLeader
-    Pending = Pending
+    None = None
 
     RequestVoteRequest = RequestVoteRequest
     RequestVoteResponse = RequestVoteResponse

tla/consensus/SIMCoverageccfraft.cfg

@@ -9,7 +9,7 @@ CONSTANTS
     Candidate = Candidate
     Leader = Leader
     RetiredLeader = RetiredLeader
-    Pending = Pending
+    None = None
 
     RequestVoteRequest = RequestVoteRequest
     RequestVoteResponse = RequestVoteResponse

tla/consensus/SIMccfraft.cfg

@@ -9,7 +9,7 @@ CONSTANTS
     Candidate = Candidate
     Leader = Leader
     RetiredLeader = RetiredLeader
-    Pending = Pending
+    None = None
 
     RequestVoteRequest = RequestVoteRequest
     RequestVoteResponse = RequestVoteResponse

tla/consensus/Traceccfraft.cfg

@@ -51,7 +51,7 @@ CONSTANTS
     Candidate = Candidate
     Leader = Leader
     RetiredLeader = RetiredLeader
-    Pending = Pending
+    None = None
 
     RequestVoteRequest = RequestVoteRequest
     RequestVoteResponse = RequestVoteResponse

tla/consensus/Traceccfraft.tla

@@ -8,7 +8,7 @@ RaftMsgType ==
     "raft_propose_request_vote" :> ProposeVoteRequest
 
 LeadershipState ==
-    Leader :> "Leader" @@ Follower :> "Follower" @@ Candidate :> "Candidate" @@ Pending :> "Pending"
+    Leader :> "Leader" @@ Follower :> "Follower" @@ Candidate :> "Candidate" @@ None :> "None"
 
 \* In:  <<[idx |-> 0, nodes |-> [0 |-> [address |-> ":"]], rid |-> 0]>>
 \* Out: (0 :> {0})
@@ -380,16 +380,16 @@ TraceNext ==
 
 RaftDriverQuirks ==
     \* The "nodes" command in raft scenarios causes N consecutive "add_configuration" log lines to be emitted,
-     \* where N is determined by the "nodes" parameter. At this stage, the nodes are in the "Pending" state.
+     \* where N is determined by the "nodes" parameter. At this stage, the nodes are in the "None" state.
      \* However, the enablement condition of "ccfraft!Timeout" is only true for nodes in the "Candidate" or 
      \* "Follower" state. Therefore, we include this action to address this quirk in the raft_driver.
     \/ /\ IsEvent("add_configuration")
-       /\ state[logline.msg.state.node_id] = Pending
+       /\ state[logline.msg.state.node_id] = None
        /\ configurations' = [ configurations EXCEPT ![logline.msg.state.node_id] = ToConfigurations(<<logline.msg.new_configuration>>)]
        /\ state' = [ state EXCEPT ![logline.msg.state.node_id] = Follower ]
        /\ UNCHANGED <<reconfigurationCount, removedFromConfiguration, messageVars, currentTerm, votedFor, candidateVars, leaderVars, logVars>>    
     \/ /\ IsEvent("become_follower")
-       /\ state[logline.msg.state.node_id] = Pending
+       /\ state[logline.msg.state.node_id] = None
        /\ configurations[logline.msg.state.node_id] = ToConfigurations(logline.msg.configurations)
        /\ state' = [ state EXCEPT ![logline.msg.state.node_id] = Follower ]
        /\ UNCHANGED <<reconfigurationVars, removedFromConfiguration, messageVars, currentTerm, votedFor, candidateVars, leaderVars, logVars>>

tla/consensus/ccfraft.tla

@@ -48,21 +48,19 @@ CONSTANTS
     \*          /\ state[s] = Leader
     \*          /\  CurrentConfiguration(s) \ CurrentConfiguration(s)' = {s}
     \*          => state'[s] = RetiredLeader]_state
+    \* TODO: this should be split into a separate membership_state, as in
+    \* the implementation.
     RetiredLeader,
-    \* The node has passed attestation checks, but is waiting for member confirmation, 
-    \* and just isn't part of any configurations at all, nor has a communication channel
-    \* with other nodes in the network.
-    \*
-    \* More formally:
-    \*   \A i \in Servers : state[i] = Pending => i \notin { GetServerSet(s) : s \in Servers}
-    Pending
+    \* Initial state for a joiner node, until it has received a first message
+    \* from another node.
+    None
 
 States == {
     Follower,
     Candidate,
     Leader,
     RetiredLeader,
-    Pending
+    None
     }
 
 \* Message types:
@@ -497,7 +495,7 @@ InitMessagesVars ==
 
 InitServerVars ==
     /\ currentTerm = [i \in Servers |-> 0]
-    /\ state       = [i \in Servers |-> IF i \in configurations[i][0] THEN Follower ELSE Pending]
+    /\ state       = [i \in Servers |-> IF i \in configurations[i][0] THEN Follower ELSE None]
     /\ votedFor    = [i \in Servers |-> Nil]
 
 InitCandidateVars ==
@@ -907,7 +905,7 @@ NoConflictAppendEntriesRequest(i, j, m) ==
         /\ configurations' = 
                 [configurations EXCEPT ![i] = RestrictDomain(new_configs, LAMBDA c : c >= new_conf_index)]
         \* If we added a new configuration that we are in and were pending, we are now follower
-        /\ IF /\ state[i] = Pending
+        /\ IF /\ state[i] = None
               /\ \E conf_index \in DOMAIN(new_configs) : i \in new_configs[conf_index]
            THEN state' = [state EXCEPT ![i] = Follower ]
            ELSE UNCHANGED state
@@ -923,7 +921,7 @@ NoConflictAppendEntriesRequest(i, j, m) ==
 AcceptAppendEntriesRequest(i, j, logOk, m) ==
     \* accept request
     /\ m.term = currentTerm[i]
-    /\ state[i] \in {Follower, Pending}
+    /\ state[i] \in {Follower, None}
     /\ logOk
     /\ LET index == m.prevLogIndex + 1
        IN \/ AppendEntriesAlreadyDone(i, j, index, m)
@@ -993,12 +991,12 @@ DropResponseWhenNotInState(i, j, m) ==
 DropIgnoredMessage(i,j,m) ==
     \* Drop messages if...
     /\
-       \* .. recipient is still Pending..
-       \/ /\ state[i] = Pending
+       \* .. recipient is still None..
+       \/ /\ state[i] = None
           \* .. and the message is anything other than an append entries request
           /\ m.type /= AppendEntriesRequest
-       \*  OR if message is to a server that has surpassed the Pending stage ..
-       \/ /\ state[i] /= Pending
+       \*  OR if message is to a server that has surpassed the None stage ..
+       \/ /\ state[i] /= None
         \* .. and it comes from a server outside of the configuration
           /\ \lnot IsInServerSet(j, i)
        \*  OR if recipient is RetiredLeader and this is not a request to vote
@@ -1325,7 +1323,7 @@ MonotonicMatchIndexProp ==
 PermittedLogChangesProp ==
     [][\A i \in Servers :
         log[i] # log[i]' =>
-            \/ state[i]' = Pending
+            \/ state[i]' = None
             \/ state[i]' = Follower
             \* Established leader adding new entries
             \/ /\ state[i] = Leader
@@ -1347,16 +1345,16 @@ PermittedLogChangesProp ==
 
 StateTransitionsProp ==
     [][\A i \in Servers :
-        /\ state[i] = Pending => state[i]' \in {Pending, Follower}
+        /\ state[i] = None => state[i]' \in {None, Follower}
         /\ state[i] = Follower => state[i]' \in {Follower, Candidate}
         /\ state[i] = Candidate => state[i]' \in {Follower, Candidate, Leader}
         /\ state[i] = Leader => state[i]' \in {Follower, Leader, RetiredLeader}
         /\ state[i] = RetiredLeader => state[i]' = RetiredLeader
         ]_vars
 
 PendingBecomesFollowerProp ==
-    \* A pending node that becomes part of any configuration immediately transitions to Follower.
-    [][\A s \in { s \in Servers : state[s] = Pending } : 
+    \* A pending node that becomes aware it is part of a configuration immediately transitions to Follower.
+    [][\A s \in { s \in Servers : state[s] = None } : 
             s \in GetServerSet(s)' => 
                 state[s]' = Follower]_vars