From 2f590a6392b8441b0347edd658c244cc4794ae7f Mon Sep 17 00:00:00 2001
From: Igor Konnov <konnov@forsyte.at>
Date: Thu, 21 Jan 2021 11:50:06 +0100
Subject: [PATCH] non-critical bugfix in the TLA+ spec (found by new version of
 apalache) (#244)

---
 rust-spec/tendermint-accountability/TendermintAcc_004_draft.tla | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 <<round, lockedValue, lockedRound, validValue,
                   validRound, decision, msgsPropose, msgsPrevote>>
     /\ action' = "OnQuorumOfNilPrevotes"