Re: Parsing Error in Consensus.tla

["ka...@xxxxxxxxxxxxxxx" <ka...@xxxxxxxxxxxxxxx>]

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