[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Parsing Error in Consensus.tla

The formula in step <2>1 should read

  Inv /\ [][Next]_vars => []Inv

It should indeed never have been accepted by the parser because the formula that appears in your quote is not a legal temporal formula.

I'm not sure where that module comes from: it's not one of the example modules that are distributed with the TLA+ proof system (in examples/consensus or examples/paxos). If you took it from the distribution, I'd be grateful of a pointer so that we can fix that.

More generally, temporal invariant proofs in TLAPS rely on a PTL decision procedure rather than on explicit rule applications. It looks to me that this was an early sketch of how temporal proofs might be written.

Best regards and sorry for the confusion,


On 23 Jun 2014, at 14:42, Christian Spann <cspanns....@xxxxxxxxx> wrote:

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 
    (* 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

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

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.