[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Parsing Error in Consensus.tla
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.
On Friday, July 1, 2016 at 12:55:05 AM UTC-7, kaie wrote:
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).