From 89e71f2e45a4539af9c4c138fb2416e2abf261a2 Mon Sep 17 00:00:00 2001
From: Kukovec <jure.kukovec@gmail.com>
Date: Thu, 5 May 2022 13:08:48 +0200
Subject: [PATCH] Generators

---
 .../tla/MC_PBT_2C_2F.tla                      |  3 +-
 .../tla/MC_PBT_3C_1F.tla                      |  3 +-
 .../tla/TendermintPBT_002_draft.tla           | 40 ++++++++++++++-----
 3 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla
index 393342821..345201c3a 100644
--- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla
@@ -62,7 +62,8 @@ INSTANCE TendermintPBT_002_draft WITH
   MinTimestamp <- 2,
   Delay <- 2,        
   Precision <- 2,
-  PreloadAllFaultyMsgs <- FALSE
+  PreloadAllFaultyMsgs <- TRUE,
+  N_GEN <- 5
 
 \* run Apalache with --cinit=CInit
 CInit == \* the proposer is arbitrary -- works for safety
diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla
index 2bedb48db..594615132 100644
--- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla
@@ -62,7 +62,8 @@ INSTANCE TendermintPBT_002_draft WITH
   MinTimestamp <- 2,
   Delay <- 2,        
   Precision <- 2,
-  PreloadAllFaultyMsgs <- FALSE
+  PreloadAllFaultyMsgs <- TRUE,
+  N_GEN <- 5
 
 \* run Apalache with --cinit=CInit
 CInit == \* the proposer is arbitrary -- works for safety
diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
index 436b9286c..6296b7ca4 100644
--- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
@@ -50,7 +50,9 @@ ASSUME(N = Cardinality(Corr \union Faulty))
 \* Modeling parameter
 CONSTANTS
   \* @type: Bool;
-  PreloadAllFaultyMsgs
+  PreloadAllFaultyMsgs,
+  \* @type: Int;
+  N_GEN
 
 (*************************** DEFINITIONS ************************************)
 \* @type: Set(PROCESS);
@@ -84,8 +86,8 @@ ArbitraryProposer == Proposer \in [Rounds -> AllProcs]
 CorrectProposer == Proposer \in [Rounds -> Corr]
 CyclicalProposer == 
   LET ProcOrder ==
-    LET App(s,e) == Append(s,e) \* can't call-by-name for built-in operators
-    IN ApaFoldSet(Append, <<>>, AllProcs)
+    LET App(s,e) == Append(s,e)
+    IN ApaFoldSet(App, <<>>, AllProcs)
   IN Proposer = [ r \in Rounds |-> ProcOrder[1 + (r % N)] ]
 
 ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
@@ -285,14 +287,34 @@ BenignRoundsInMessages(msgfun) ==
     \A m \in msgfun[r]:
       r = m.round
 
+\* @type: (ROUND -> Set(MESSAGE), Set(MESSAGE)) => Bool;
+BenignAndSubset(msgfun, set) == 
+  /\ \A r \in Rounds: 
+    \* The generated values belong to SUBSET set
+    /\ msgfun[r] \subseteq set
+    \* the message function never contains a message for a wrong round
+    /\ \A m \in msgfun[r]: r = m.round
+
+InitGen == 
+  /\ msgsPropose \in [Rounds -> Gen(N_GEN)]
+  /\ msgsPrevote \in [Rounds -> Gen(N_GEN)]
+  /\ msgsPrecommit \in [Rounds -> Gen(N_GEN)]
+  /\ BenignAndSubset(msgsPropose, AllFaultyProposals)
+  /\ BenignAndSubset(msgsPrevote, AllFaultyPrevotes)
+  /\ BenignAndSubset(msgsPrecommit, AllFaultyPrecommits)
+
+InitPreloadAllMsgs ==
+  /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
+  /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
+  /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
+  /\ BenignRoundsInMessages(msgsPropose)
+  /\ BenignRoundsInMessages(msgsPrevote)
+  /\ BenignRoundsInMessages(msgsPrecommit)
+
 InitMsgs ==
   \/ /\ PreloadAllFaultyMsgs
-     /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
-     /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
-     /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
-     /\ BenignRoundsInMessages(msgsPropose)
-     /\ BenignRoundsInMessages(msgsPrevote)
-     /\ BenignRoundsInMessages(msgsPrecommit)
+     \* /\ InitPreloadAllMsgs
+     /\ InitGen
   \/ /\ ~PreloadAllFaultyMsgs
      /\ msgsPropose = [r \in Rounds |-> {}]
      /\ msgsPrevote = [r \in Rounds |-> {}]