Browse Source

non-critical bugfix in the TLA+ spec (found by new version of apalache) (#244)

pull/7804/head
Igor Konnov 4 years ago
committed by GitHub
parent
commit
2f590a6392
No known key found for this signature in database GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
  1. +1
    -1
      rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla

+ 1
- 1
rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla View File

@ -332,7 +332,7 @@ OnQuorumOfNilPrevotes(p) ==
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
/\ evidence' = PV \union evidence
/\ BroadcastPrecommit(p, round[p], Id(NilValue))
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
validRound, decision, msgsPropose, msgsPrevote>>
/\ action' = "OnQuorumOfNilPrevotes"


Loading…
Cancel
Save