Refactor Traceccfraft to reuse IsRequestVoteRequest. (#6104)

.gitignore

@@ -45,3 +45,4 @@ tests/perf-system/analyzer/*.png
 **/*.ipynb*
 scripts/azure_deployment/.env
 tests/external_executor/executors/ccf/protobuf/*.proto
+.env

scripts/TLAi-linter.genai.js

@@ -20,12 +20,14 @@ Explain any consistencies and inconsistencies you may find.  Report inconsistent
 ## TLA+ Syntax Hints
 - A formula [A]_v is called a temporal formula, and is shorthand for the formula A \/ v' = v.  In other words, the formula is true if A is true or if the value of v remains unchanged.  Usually, v is a tuple of the spec's variables.
 - The symbol \`#\` is alternative syntax used for inequality in TLA+; the other symbol is \`/=\".
+- There a no assignments in TLA: \`x = 23\` and \`x' = 42\` are formula that assert that x equals 23 in the current state and 42 in a successor state.  Moreover, one may write \`x = 42 /\ x = 23\` which equals false but does not assign to x twice.
 
 ## TLA+ Semantics Hints
 - Do NOT add any invariants or properties to the behavior specification Spec or any of its subformulas.  This would change THEOREM Spec => Inv into THEOREM Spec /\ Inv => Inv, which is vacuously true.
 - TLA+ specs are always stuttering insensitive, i.e., the next-state relation is always [A]_v.  In other words, one cannot write a stuttering sensitive specification.
 
 ## TLA+ Convention Hints
+- Trivial or obvious formulas and sub-formulas are typically not commented.
 - The type correctness invariant is typically called TypeOK.
 - Users can employ TLA labels as a means to conceptually associate a comment with a sub-formula like a specific disjunct or conjunct of a TLA formula. Even though these labels have no other function, they facilitate referencing particular parts of the formula from a comment.
 

tla/consensus/Traceccfraft.tla

@@ -335,12 +335,9 @@ IsSendRequestVote ==
            j == logline.msg.to_node_id
        IN /\ RequestVote(i, j)
           /\ \E m \in Network!Messages':
-                /\ m.type = RequestVoteRequest
-                /\ m.type = RaftMsgType[logline.msg.packet.msg]
-                /\ m.term = logline.msg.packet.term
-                /\ m.lastCommittableIndex = logline.msg.packet.last_committable_idx
-                /\ m.lastCommittableTerm = logline.msg.packet.term_of_last_committable_idx
-                \* There is now one more message of this type.
+                \* Assert that as a result of RequestVote above, the variable messages is changed to contain
+                \* a RequestVoteRequest message sent from i to j.
+                /\ IsRequestVoteRequest(m, j, i, logline)
                 /\ Network!OneMoreMessage(m)
     /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id)
     /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
@@ -353,12 +350,7 @@ IsRcvRequestVoteRequest ==
        /\ LET i == logline.msg.state.node_id
               j == logline.msg.from_node_id
           IN \E m \in Network!MessagesTo(i, j):
-               /\ m.type = RequestVoteRequest
-               /\ m.dest   = i
-               /\ m.source = j
-               /\ m.term = logline.msg.packet.term
-               /\ m.lastCommittableIndex = logline.msg.packet.last_committable_idx
-               /\ m.lastCommittableTerm = logline.msg.packet.term_of_last_committable_idx
+               /\ IsRequestVoteRequest(m, i, j, logline)
                /\ \/ HandleRequestVoteRequest(i, j, m)
                   \* Below formula is a decomposed TraceRcvUpdateTermReqVote step, i.e.,
                   \* a (ccfraft!UpdateTerm \cdot ccfraft!HandleRequestVoteRequest) step.