[tlaplus] Inductive Invariants and Counterexamples in TLAPS

[Willy Schultz <will62794@xxxxxxxxx>]

Have there been any previous attempts to incorporate counterexample generation into TLAPS? For example, say we are trying to prove an inductive invariant, Ind. If it is not inductive, it is helpful to get a counterexample to induction i.e. some state that satisfies Ind but which can reach a state violating Ind via some protocol transition. Recently, I have been using the probabilistic method of checking inductive invariance described in [1], and it has seemed to work surprisingly well. Of course, it only works on finite protocol instances, but this is still very helpful when debugging an inductive invariant.

I am curious about whether this could be done with TLAPS, though, since TLAPS can produce an SMT encoding of a TLA+ invariant and transition relation. In theory, it seems that the probabilistic method is solving something at least as hard as satisfiability, since it first needs to generate states that satisfy some arbitrary predicate, Ind. It takes a completely "dumb" approach, though, and just randomly samples states and checks to see if they satisfy Ind. I would think, though, that state of the art SMT solvers would be able to outperform the efficiency of this technique. So, it would seem TLAPS would be well suited to handle this problem, since it is able to generate an SMT encoding that can be handed to a solver. 

Presumably, Apalache [2] is another candidate for this task, since it also produces an SMT encoding that can be given to an SMT solver. Their OOPSLA '19 paper [3] claims that it can prove certain inductive invariants automatically, and that it can detect invariant violations quickly as well. I suppose it would be interesting to compare the performance of the probabilistic method for finding inductiveness violations with Apalache, and/or compare Apalache with TLAPS. I suppose the details of the SMT encoding can make a significant difference in performance here? Tools like Ivy [4] are supposed to be fast at inductive invariant checking because they restrict the input language in a rather spartan way. It would seem that TLA+ seems cannot utilize similar ideas due to its expressiveness.

In general, I would be interested to hear others' thoughts on this, if they worked on or considered these problems in the past.

[1] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

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

[3] https://forsyte.at/wp-content/uploads/kkt-oopsla19.pdf

[4] https://cs.stanford.edu/~padon/ivy.pdf

-- 
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/546a3817-a702-4930-bb51-1af83da9238en%40googlegroups.com.