[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.