Parsing Error in Consensus.tla

[Christian Spann]

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

[Stephan Merz]

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,

Stephan

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

Note: in posting this, I may have inadvertently deleted another posting.
If I deleted your posting, please feel free to re-post.

The error message says

  => has both temporal formula and action as arguments

The [] in the formula means that the entire formula is a TLA+ temporal
formula.  However, the subformula [Next]_vars, which is an action
formula, is not a legal TLA temporal formula.  Hence the entire
formula is illegal.  (The construct [N]_v can appear in a temporal
formula only in a subformula [][N]_v .)

The [] in the formula is spurious, and it should read

   <2>1. Inv /\ [Next]_vars => Inv

Earlier versions of the parser did not catch that error; the check for
it was not added until October 2013.  Apparently, the proof was not
rerun with the current version.  TLAPS assumes that proofs have been
successfully parsed by the Toolbox.  Since the "proof" of that step is
PROOF OMITTED, there is no reason TLAPS should have found the error.

Leslie

[Leslie Lamport]

First of all, Stephan is correct that the [] should be added to [Next]_vars rather than removed from []Inv.

Second, I see that the proof actually was rerun through the provers in November 2013 and the error
corrected in my own copy.  However, I failed to update the version on the Web.  The proofs need additional
changes to keep up with changes to the prover.  I will try to get new versions of those files on the Web
as soon as I can.

Leslie

[Andrew Wilcox]

fyi, http://research.microsoft.com/en-us/um/people/lamport/tla/Consensus.tla found at http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html does still contain the typo:

[Leslie Lamport]

Thanks for the reminder.  I just corrected the error in the copy on the Web.  I still don't know how it happened, because I believe that file is one that the prover was run on.   I have newer versions that I should post.  But  I believe that the files on the Web are the ones mentioned in published paper, so they should be kept where they are.

Leslie

On Monday, June 27, 2016 at 6:20:23 PM UTC-7, Andrew Wilcox wrote:

[ka...@cse.unsw.edu.au]

On Tuesday, June 24, 2014 at 5:44:33 AM UTC+10, Leslie Lamport wrote:

[...] 

The [] in the formula is spurious, and it should read

   <2>1. Inv /\ [Next]_vars => Inv

Not sure why it's missing but I believe there ought to be prime at the very end:

   <2>1. Inv /\ [Next]_vars => Inv'

to make it interesting (and sufficiently strong for the following invariant proof).

Kai

[Leslie Lamport]

On Monday, June 23, 2014 at 3:59:50 PM UTC-7 I corrected my earlier email and wrote that the formula should be

   <2>1. Inv /\ [][Next]_vars => []Inv

The formula you are looking for is the statement of LEMMA InductiveInvariance.

Leslie