diff --git a/rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla b/rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla index bb214bf9b..9d3a543d4 100644 --- a/rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla +++ b/rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla @@ -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 <> /\ action' = "OnQuorumOfNilPrevotes"