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