mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-07-20 15:02:33 +00:00
Code Issues Packages Projects Releases Wiki Activity

Generators

Browse Source
This commit is contained in:
Kukovec
2022-05-05 13:08:48 +02:00
parent 92f287f7d3
commit 89e71f2e45
3 changed files with 35 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/consensus/proposer-based-timestamp/tla/MC_PBT_2C_2F.tla
+2 -1
View File
@@ -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
spec/consensus/proposer-based-timestamp/tla/MC_PBT_3C_1F.tla
+2 -1
View File
@@ -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
spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
+31 -9
View File
@@ -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 |-> {}]