Strengthen implication to biimplication.

#22 (comment) Signed-off-by: Markus Alexander Kuppe <[email protected]>
heidihoward · Dec 17, 2024 · 3aaf753 · 3aaf753
1 parent 6a26659
commit 3aaf753
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pirateship.tla b/pirateship.tla
@@ -140,7 +140,7 @@ TypeOK ==
     /\ view \in [R -> Views]
     /\ log \in [R -> Log]
     /\ \A l \in Range(log):
-        \A i \in DOMAIN l: l[i].byzQC = {} => l[i].byzQCVotes = {}
+        \A i \in DOMAIN l: l[i].byzQC = {} <=> l[i].byzQCVotes = {}
     /\ \A r, s \in R:
         \A i \in DOMAIN network[r][s]: network[r][s][i] \in Messages
     /\ primary \in [R -> BOOLEAN]