Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TLA+: Forking cases for tendermint #496

Merged
merged 6 commits into from
Sep 24, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 31 additions & 0 deletions docs/spec/tendermint-fork-cases/001indinv-apalache.csv
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
no,filename,tool,timeout,init,inv,next,args
1,MC_n4_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
2,MC_n4_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
3,MC_n4_f3.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
4,MC_n5_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
5,MC_n5_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
6,MC_n7_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
7,MC_n7_f3.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
8,MC_n7_f4.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
9,MC_n10_f3.tla,apalache,24h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
10,MC_n10_f4.tla,apalache,24h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
11,MC_n4_f1.tla,apalache,10h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
12,MC_n4_f2.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
13,MC_n4_f3.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
14,MC_n5_f1.tla,apalache,10h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
15,MC_n5_f2.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
16,MC_n7_f2.tla,apalache,10h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
17,MC_n7_f3.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
18,MC_n7_f4.tla,apalache,10h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
19,MC_n10_f3.tla,apalache,24h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
20,MC_n10_f4.tla,apalache,24h,TypedInv,AgreementOrEquivocationOrAmnesia,,--length=0 --cinit=ConstInit
21,MC_n4_f1.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
22,MC_n4_f2.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
23,MC_n4_f3.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
24,MC_n5_f1.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
25,MC_n5_f2.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
26,MC_n7_f2.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
27,MC_n7_f3.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
28,MC_n7_f4.tla,apalache,10h,Init,TypedInv,,--length=0 --cinit=ConstInit
29,MC_n10_f3.tla,apalache,24h,Init,TypedInv,,--length=0 --cinit=ConstInit
30,MC_n10_f4.tla,apalache,24h,Init,TypedInv,,--length=0 --cinit=ConstInit
8 changes: 8 additions & 0 deletions docs/spec/tendermint-fork-cases/001indinv-apalache.ini
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# a configuration file for apalache-tests/scripts/mk-run.py

[apalache-unstable]
more_args=

[apalache-card]
more_args=

26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n10_f3.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n10_f3 -------------------------------
konnov marked this conversation as resolved.
Show resolved Hide resolved
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3", "c4", "c5", "c6", "c7"},
Defective <- {} <: {STRING},
Byzantine <- {"f8", "f9", "f10"},
N <- 10,
T <- 3,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n10_f4.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n10_f4 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3", "c4", "c5", "c6"},
Defective <- {"f7"},
Byzantine <- {"f8", "f9", "f10"},
N <- 10,
T <- 3,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n4_f1.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n4_f1 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3"},
Defective <- {} <: {STRING},
Byzantine <- {"f1"},
N <- 4,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n4_f2.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n4_f2 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2"},
Defective <- {"f3"},
Byzantine <- {"f4"},
N <- 4,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n4_f3.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n4_f3 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1"},
Defective <- {"a2", "a3"},
Byzantine <- {"f4"},
N <- 4,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n5_f1.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n5_f1 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3", "c4"},
Defective <- {} <: {STRING},
Byzantine <- {"f5"},
N <- 5,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n5_f2.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n5_f2 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3"},
Defective <- {"a4"},
Byzantine <- {"f5"},
N <- 5,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n7_f2.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n7_f2 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3", "c4", "c5"},
Defective <- {} <: {STRING},
Byzantine <- {"f6", "f7"},
N <- 7,
T <- 2,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n7_f3.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n7_f3 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3", "c4"},
Defective <- {"f5"},
Byzantine <- {"f6", "f7"},
N <- 7,
T <- 2,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
26 changes: 26 additions & 0 deletions docs/spec/tendermint-fork-cases/MC_n7_f4.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
----------------------------- MODULE MC_n7_f4 -------------------------------
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

\* an operator for type annotations
a <: b == a

INSTANCE TendermintAccDebug3 WITH
Corr <- {"c1", "c2", "c3"},
Defective <- {"f4", "f5"},
Byzantine <- {"f6", "f7"},
N <- 7,
T <- 2,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 2

\* run Apalache with --cinit=ConstInit
ConstInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]

=============================================================================
Loading