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

[tlaplus] Checking Inductiveness with TLAPS

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.