mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-09-28 10:45:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

disable PrecommitsLockValue and weaken Accountability

Browse Source
This commit is contained in:
Igor Konnov
2022-08-23 18:24:52 +02:00
parent e15483dcc6
commit 31b8021672
2 changed files with 1 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/light-client/accountability/TendermintAccInv_004_draft.tla
+1 -1
View File
@@ -369,11 +369,11 @@ Inv ==
/\ IfSentPrecommitThenSentPrevote
/\ IfSentPrecommitThenReceivedTwoThirds
/\ AllNoEquivocationByCorrect
/\ PrecommitsLockValue
/\ RelockValueIfEnoughPrevotes
/\ AllIfValidRoundThenTwoThirds
/\ AllValidAndLocked
/\ AllIfValidRoundThenProposal
\*/\ PrecommitsLockValue
\* this is the inductive invariant we like to check
TypedInv == TypeOK /\ Inv
spec/light-client/accountability/TendermintAcc_004_draft.tla
-1
View File
@@ -495,7 +495,6 @@ EquivocationBy(p) ==
/\ m2.src = p
/\ m1.round = m2.round
IN
\/ EquivocationIn(evidencePropose)
\/ EquivocationIn(evidencePrevote)
\/ EquivocationIn(evidencePrecommit)