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

Re: [tlaplus] "Broken" proofs after tlaps upgrade

Saksam is right about improvements to provers often breaking some
proofs.  However, I'm afraid that people may find more previously
successful proofs breaking than they should.  This is because there
were bugs in the previous version that could have allowed TLAPS to
prove false assertions.  Fixing those bugs has made it not prove some
things it used to.  We believe it is unlikely that any assertions
people actually proved with the previous version were not true.
However, if you find that this did happen, please send us the proof in
which it did.  We will add it to our regression tests to help us
make sure that those bugs do not reappear.

We apologize for this, and we are working to make the prover again
prove the correct assertions that it used to.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d12e8639-c40a-486f-a1c1-db82027f3480%40googlegroups.com.