# Parsing Error in Consensus.tla

Dear TLA+-Community,

I have an up-to-date version of the TLA-Toolbox [1] installed and imported Mr. Lamports Consensus.tla in order to learn how to model distributed algorithms with TLA+/PlusCal. TLA+ or the Toolbox seems to have improved/changed because the file is now parsed with an error.

line 203, col 9 to line 203, col 35 of module Consensus

=> has both temporal formula and action as arguments

Where line 203 is: <2>1. Inv /\ [Next]_vars => []Inv

How can this be fixed? Sorry if the solution is obvious, but I am an absolute beginner
in this field.

The respective section of Consensus.tla is:

(***************************************************************************)
(* TLAPS does not yet handle temporal logic reasoning.  Therefore, proofs  *)
(* of temporal steps are omitted.  However, we indicate in comments what   *)
(* we expect the proofs to look like when TLAPS does prove temporal        *)
(* formulas.                                                               *)
(***************************************************************************)
THEOREM Invariance == Spec => []Inv
<1>1.  Init => Inv
\* We usually have to use SimpleArithmetic to prove facts about numbers,
\* but 0 \leq 1 is simple enough that Isabelle can prove it by itself.
BY EmptySetCardinality, 0 \leq 1 DEF Init, Inv, TypeOK

<1>2.  QED
<2>1. Inv /\ [Next]_vars => []Inv
\*    BY InductiveInvariance, RuleINV1
PROOF OMITTED
(***********************************************************************)
(* RuleInv1 is defined in the TLAPS module by                          *)
(*                                                                     *)
(*    THEOREM RuleINV1 == ASSUME STATE I, STATE F,  ACTION N,          *)
(*                               I /\ [N]_F => I'                      *)
(*                        PROVE  I /\ [][N]_F => []I                   *)
(***********************************************************************)
<2>2. QED
\*    BY <1>1, <2>1
PROOF OMITTED

Best regards,
Christian Spann

[1] This is Version 1.4.8 of 25 February 2014 and includes:
- SANY Version 2.1 of 24 February 2014
- TLC Version 2.05 of 23 July 2013
- PlusCal Version 1.8 of 2 April 2013
- TLATeX Version 1.0 of 12 April 2013