[tlaplus] Checking Inductiveness with TLAPS

[Willy Schultz <will62794@xxxxxxxxx>]

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.