|Trivial answer: TLAPS can prove |
TRUE /\ Next => TRUE'
for any formula Next.
More seriously, I would not expect this kind of problem to be proved automatically for anything but small specs and simple invariants. More importantly in practice, TLAPS is of no help when your invariant is not inductive (which is the case when you start a proof), and model checking can help you debug your invariant over small domains before you prove it in general.
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/39880BF5-35A4-4BB0-BDE2-492D85CFF993%40gmail.com.