You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
40 lines
1.2 KiB
40 lines
1.2 KiB
---------------------- MODULE MC_n4_f2_amnesia -------------------------------
|
|
EXTENDS Sequences
|
|
|
|
CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
|
|
|
|
\* the variables declared in TendermintAcc3
|
|
VARIABLES
|
|
round, step, decision, lockedValue, lockedRound, validValue, validRound,
|
|
msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
|
|
|
|
\* the variable declared in TendermintAccTrace3
|
|
VARIABLE
|
|
toReplay
|
|
|
|
\* old apalache annotations, fix with the new release
|
|
a <: b == a
|
|
|
|
INSTANCE TendermintAccTrace_004_draft WITH
|
|
Corr <- {"c1", "c2"},
|
|
Faulty <- {"f3", "f4"},
|
|
N <- 4,
|
|
T <- 1,
|
|
ValidValues <- { "v0", "v1" },
|
|
InvalidValues <- {"v2"},
|
|
MaxRound <- 2,
|
|
Trace <- <<
|
|
"UponProposalInPropose",
|
|
"UponProposalInPrevoteOrCommitAndPrevote",
|
|
"UponProposalInPrecommitNoDecision",
|
|
"OnRoundCatchup",
|
|
"UponProposalInPropose",
|
|
"UponProposalInPrevoteOrCommitAndPrevote",
|
|
"UponProposalInPrecommitNoDecision"
|
|
>> <: Seq(STRING)
|
|
|
|
\* run Apalache with --cinit=ConstInit
|
|
ConstInit == \* the proposer is arbitrary -- works for safety
|
|
Proposer \in [Rounds -> AllProcs]
|
|
|
|
=============================================================================
|