Re: [tlaplus] Checking Inductiveness with TLAPS

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.

On 8 Jun 2021, at 18:54, Willy Schultz <will62794@xxxxxxxxx> wrote:

Is it theoretically possible to use TLAPS to check an inductive invariant over an unbounded domain? That is, can I ask TLAPS to try proving Ind /\ Next => Ind' without any help? I know that, in general, the problem may be too hard for TLAPS (i.e. the backend solver) to handle on its own, but I am curious if this may be feasible for simple inductive invariants. I could also try Apalache [1], but my understanding was that it still only works over finite (i.e. bounded) domains.

[1] https://github.com/informalsystems/apalache

--
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/a9472149-49a3-4386-8a25-9b856b6ddde0n%40googlegroups.com.