Merge branch 'main' into align

pirateship.tla

@@ -188,7 +188,15 @@ HighestQCOverQC(l) ==
 Max2(a,b) == IF a > b THEN a ELSE b
 Min2(a,b) == IF a < b THEN a ELSE b
 
-MaxQuorum(l, m, default) == 
+MaxCrashQuorum(l, m, default) == 
+    LET RECURSIVE RMaxQuorum(_)
+        RMaxQuorum(i) ==
+            IF i = default THEN default
+            ELSE IF \E q \in CQ: \A n \in q: m[n] >= i
+                 THEN i ELSE RMaxQuorum(i-1)
+    IN RMaxQuorum(Len(l))
+
+MaxByzQuorum(l, m, default) == 
     LET RECURSIVE RMaxQuorum(_)
         RMaxQuorum(i) ==
             IF i = default THEN default
@@ -313,7 +321,7 @@ ReceiveVote(p, r) ==
     \* If view is stable, then the primary can update its commit indexes
     /\ IF viewStable'[p]
         THEN crashCommitIndex' = [crashCommitIndex EXCEPT ![p] = 
-                MaxQuorum(log[p], prepareQC'[p], @)]
+                MaxCrashQuorum(log[p], prepareQC'[p], @)]
         ELSE UNCHANGED crashCommitIndex
     /\ UNCHANGED <<view, log, primary, byzCommitIndex, byzActions>>
 
@@ -323,8 +331,8 @@ MaxCrashQC(l,p) ==
     ELSE {}
 
 MaxByzQC(l, m) == 
-    IF MaxQuorum(l, m, 0) > HighestByzQC(l)
-    THEN {MaxQuorum(l, m, 0)}
+    IF MaxByzQuorum(l, m, 0) > HighestByzQC(l)
+    THEN {MaxByzQuorum(l, m, 0)}
     ELSE {}
 
 \* Primary p sends AppendEntries to all replicas