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

Re: Parsing Error in Consensus.tla

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.