From 903c5668dbd12ee26fa4a171fa0fac73e297e2aa Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Wed, 4 Sep 2024 06:52:34 -0700
Subject: [PATCH] Mitigate state-space explosion of two byzantine actions to
 prevent TLC from attempting to generate sets that are too large.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 MCpbft.cfg |  7 ++++++-
 MCpbft.tla | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 1 deletion(-)

diff --git a/MCpbft.cfg b/MCpbft.cfg
index 9b43991..583b68b 100644
--- a/MCpbft.cfg
+++ b/MCpbft.cfg
@@ -1,10 +1,15 @@
 SPECIFICATION SpecByz
 
 CONSTANT 
-\*  Init <- MCInit
+    Init <- MCInit
     ViewChange <- MCViewChange
     GenerateO <- MC_GenerateO
 
+    \* -simulate and -generate will encounter too large sets (subsets) unless those two
+    \* actions are redefined to randomly choose a smaller number of subsets.
+    InjectViewChange <- SimInjectViewChange
+    InjectNewView <- SimInjectNewView
+
 CONSTANTS
     R <- MC_R
     ByzR <- MC_ByzR
diff --git a/MCpbft.tla b/MCpbft.tla
index 6d76dfb..912382f 100644
--- a/MCpbft.tla
+++ b/MCpbft.tla
@@ -103,5 +103,45 @@ MC_GenerateO(V,i,v) ==
         maxs == Max0({ppm.n: ppm \in ppms}) IN
     {[v |-> v, p |-> i, n |-> sn, d |-> GetDigest(ppms,sn)] : sn \in (mins+1)..maxs}
 
+-------
+
+
+MCRandomSetOfSubsets(S) ==
+    (* Up to 2^8 subsets of S. *)
+    IF Cardinality(S) <= 8
+    \* Exhaustively generate all subsets up to and including 512 elements.
+    THEN SUBSET S
+    \* Constraints RandomSetOfSubsets(k,n,S) operator:
+    \* k < 2^|S| and n \in 0..Cardinality(S)
+    \* see https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/Randomization.tla
+    ELSE RandomSetOfSubsets(2^8, Cardinality(S) \div 2, S)
+
+SimInjectViewChange(i) ==
+    /\ \E v \in Views, n \in (SeqNums \cup {0}), 
+            c \in MCRandomSetOfSubsets(msgs.checkpoint), 
+            p \in MCRandomSetOfSubsets([preprepare : msgs.preprepare, prepare : MCRandomSetOfSubsets(msgs.prepare)]) :
+        \* Any replica that receive a view change message will check that the checkpoint/prepare proofs are valid
+        \* Therefore, we do not need to brother injecting view change messages with invalid proofs
+        /\ ValidCheckpointProof(c, n)
+        /\ \A pp \in p: ValidPrepareProof(pp, n)
+        /\ msgs' = [msgs EXCEPT !.viewchange = @ \cup {[
+            v |-> v,
+            n |-> n,
+            c |-> c,
+            p |-> p,
+            i |-> i]}]
+    /\ UNCHANGED <<mlogs, views, states, sCheckpoint, vChange>>
+
+SimInjectNewView(i) ==
+    /\ \E v \in Views, vc \in MCRandomSetOfSubsets(msgs.viewchange), o \in MCRandomSetOfSubsets(msgs.preprepare) : 
+        /\ i = v % N
+        /\ \A vcm \in vc: ValidViewChange(vcm, v)
+        /\ o = GenerateO(vc, i, v)
+        /\ msgs' = [msgs EXCEPT !.newview = @ \cup {[
+            v |-> v,
+            vc |-> vc,
+            o |-> o,
+            p |-> i]}]
+    /\ UNCHANGED <<mlogs, views, states, sCheckpoint, vChange>>
 
 =====