Update pirateship.tla

heidihoward · Dec 17, 2024 · 9f6d53b · 9f6d53b
1 parent 4ec8048
commit 9f6d53b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pirateship.tla b/pirateship.tla
@@ -447,7 +447,7 @@ BecomePrimary(r) ==
 \* Note that replicas must always discard messages as the pairwise channels are ordered so a replica may need to discard an out-of-date message to process a more recent one
 DiscardMessages ==
     /\ \E s,r \in R:
-            network' = [network EXCEPT ![r][s] = SelectSeq(@, LAMBDA m: m.view >= view[r])]
+            network' = [network EXCEPT ![r][s] = SelectSeq(@, LAMBDA m: ~(m.view < view[r] \/ (m.view = view[r] /\ m.type = "ViewChange" /\ primary[r])))]
     /\ UNCHANGED <<view, log, primary, prepareQC, crashCommitIndex, byzCommitIndex, byzActions, viewStable>>
 
 ----