IsRcvProposeVoteRequest does not define the successor state(s). (#5799)

microsoft · Oct 31, 2023 · 6fe397f · 6fe397f
1 parent af21407
commit 6fe397f
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla
@@ -340,6 +340,7 @@ IsRcvProposeVoteRequest ==
            j == logline.msg.to_node_id
        IN /\ \E m \in Network!Messages':
                 /\ m.type = ProposeVoteRequest
+                /\ RcvProposeVoteRequest(i, j)
                 /\ m.type = RaftMsgType[logline.msg.packet.msg]
                 /\ m.term = logline.msg.packet.term
                 \* There is now one more message of this type.