Thank you for the interesting question. We made a few experiments on counter-example generation for TLAPS a few years ago, and the results were quite disappointing. My conclusion at the time was that we would need to produce a different encoding for producing counter-examples than the one that we use for proving. Indeed, since the formulas that we produce do not fall within the decidable fragments that SMT solvers can handle – due to the heavy use of quantifiers that arise from set theory – the results that we get from SMT solvers are either UNSAT (indicating that the original proof obligation is valid) or timeout but almost never SAT (which would lead to a counter-example).
Other proof assistants provide tools for counter-example generation (e.g., nitpick and nunchaku in Isabelle) that are useful in practice, so I remain convinced that this could also be done for TLAPS, but we do not currently have the manpower to investigate this. If somebody is interested, I'd be happy to discuss this further.
And as you mention, Apalache is effective for checking inductive invariants or producing counter-examples to their inductiveness.
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/098CDFDE-4740-47DF-92EE-93D3A7B07A13%40gmail.com.