message: Decompose `Receive` action to see sub-action names in counterexamples.
diff: @@ -879,29 +879,52 @@ UpdateCommitIndex(i,j,m) ==
  votedFor, candidateVars, leaderVars, log, clientRequests, committedLog>>
  \* Receive a message.
  -Receive ==
  - \E m \in messages :
  - LET i == m.mdest
  - j == m.msource
  - IN
  - \/ /\ m.mtype = NotifyCommitMessage
  - /\ UpdateCommitIndex(i,j,m)
  - /\ Discard(m)
  +
  +RcvDropIgnoredMessage ==
  \* Drop any message that are to be ignored by the recipient
  - \/ DropIgnoredMessage(i,j,m)
  + \E m \in messages : DropIgnoredMessage(m.mdest,m.msource,m)
  +
  +RcvUpdateTerm ==
  \* Any RPC with a newer term causes the recipient to advance
  \* its term first. Responses with stale terms are ignored.
  - \/ UpdateTerm(i, j, m)
  - \/ /\ m.mtype = RequestVoteRequest
  - /\ HandleRequestVoteRequest(i, j, m)
  - \/ /\ m.mtype = RequestVoteResponse
  - /\ \/ DropStaleResponse(i, j, m)
  - \/ HandleRequestVoteResponse(i, j, m)
  - \/ /\ m.mtype = AppendEntriesRequest
  - /\ HandleAppendEntriesRequest(i, j, m)
  - \/ /\ m.mtype = AppendEntriesResponse
  - /\ \/ DropStaleResponse(i, j, m)
  - \/ HandleAppendEntriesResponse(i, j, m)
  + \E m \in messages : UpdateTerm(m.mdest, m.msource, m)
  +
  +RcvRequestVoteRequest ==
  + \E m \in messages :
  + /\ m.mtype = RequestVoteRequest
  + /\ HandleRequestVoteRequest(m.mdest, m.msource, m)
  +
  +RcvRequestVoteResponse ==
  + \E m \in messages :
  + /\ m.mtype = RequestVoteResponse
  + /\ \/ HandleRequestVoteResponse(m.mdest, m.msource, m)
  + \/ DropStaleResponse(m.mdest, m.msource, m)
  +
  +RcvAppendEntriesRequest ==
  + \E m \in messages :
  + /\ m.mtype = AppendEntriesRequest
  + /\ HandleAppendEntriesRequest(m.mdest, m.msource, m)
  +
  +RcvAppendEntriesResponse ==
  + \E m \in messages :
  + /\ m.mtype = AppendEntriesResponse
  + /\ \/ HandleAppendEntriesResponse(m.mdest, m.msource, m)
  + \/ DropStaleResponse(m.mdest, m.msource, m)
  +
  +RcvUpdateCommitIndex ==
  + \E m \in messages :
  + /\ m.mtype = NotifyCommitMessage
  + /\ UpdateCommitIndex(m.mdest, m.msource, m)
  + /\ Discard(m)
  +
  +Receive ==
  + \/ RcvDropIgnoredMessage
  + \/ RcvUpdateTerm
  + \/ RcvRequestVoteRequest
  + \/ RcvRequestVoteResponse
  + \/ RcvAppendEntriesRequest
  + \/ RcvAppendEntriesResponse
  + \/ RcvUpdateCommitIndex
  \* End of message handlers.
  ----
  