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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 23 Jun 2014 12:44:32 -0700 (PDT)*References*: <3192db97-2a0c-4dc0-aac8-094340086a00@googlegroups.com>

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

**Follow-Ups**:**Re: Parsing Error in Consensus.tla***From:*ka...@xxxxxxxxxxxxxxx

**References**:**Parsing Error in Consensus.tla***From:*Christian Spann

- Prev by Date:
**Re: [tlaplus] Parsing Error in Consensus.tla** - Next by Date:
**Re: Parsing Error in Consensus.tla** - Previous by thread:
**Re: [tlaplus] Parsing Error in Consensus.tla** - Next by thread:
**Re: Parsing Error in Consensus.tla** - Index(es):