Unify MaxCrashQuorum and MaxByzQuorum into MaxQuorum.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

pirateship.tla

@@ -184,19 +184,11 @@ HighestQCOverQC(l) ==
 Max2(a,b) == IF a > b THEN a ELSE b
 Min2(a,b) == IF a < b THEN a ELSE b
 
-MaxCrashQuorum(l, m, default) == 
+MaxQuorum(Q, 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
-            ELSE IF \E q \in BQ: \A n \in q: m[n] >= i
+            ELSE IF \E q \in Q: \A n \in q: m[n] >= i
                  THEN i ELSE RMaxQuorum(i-1)
     IN RMaxQuorum(Len(l))
 
@@ -308,7 +300,7 @@ ReceiveVote(p, r) ==
     /\ network' = [network EXCEPT ![p][r] = Tail(network[p][r])]
     /\ crashCommitIndex' = 
         [crashCommitIndex EXCEPT ![p] = 
-            MaxCrashQuorum(log[p], prepareQC'[p], @)]
+            MaxQuorum(CQ, log[p], prepareQC'[p], @)]
     /\ UNCHANGED <<view, log, primary, byzCommitIndex, byzActions>>
 
 MaxCrashQC(l,p) ==
@@ -317,8 +309,8 @@ MaxCrashQC(l,p) ==
     ELSE {}
 
 MaxByzQC(l, m) == 
-    IF MaxByzQuorum(l, m, 0) > HighestByzQC(l)
-    THEN {MaxByzQuorum(l, m, 0)}
+    IF MaxQuorum(BQ, l, m, 0) > HighestByzQC(l)
+    THEN {MaxQuorum(BQ, l, m, 0)}
     ELSE {}
 
 \* Primary p sends AppendEntries to all replicas