Merge branch 'main' into trace_after_too

achamayou · Oct 31, 2023 · 9a99b03 · 9a99b03
2 parents d0bac95 + 6fe397f
commit 9a99b03
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.