Discussion: Apalache found counter-example for invariant that was claimed proved via TLC→TLAPS

[Weining Cao]

Hi everyone,

I am working with a protocol specification in TLA⁺. In a previous work, an inductive invariant Inv was claimed to be proven using the TLC → TLAPS tool chain (i.e., Init ⇒ Inv and Inv ∧ Next ⇒ Inv′).

Recently I ran the same specification and the same invariant with Apalache (one-step inductive check) and got a counter-example (state s → state s′ where Inv(s) holds but Inv(s′) fails). Note: s is actually not reachable (in the original modeling assumptions).

My questions to the community:
Does this counter-example necessarily mean that the invariant Inv is too weak or missing assumptions?
Or could it mean that the Apalache model is more general/wider than the TLAPS proof assumptions (for example, not restricting to “only reachable states” or loosening type/constant constraints)?
In situations like this, do practitioners treat the Apalache counter-example first as a “false positive” (i.e., tool/model difference) or immediately as a signal to strengthen the invariant?
Has anyone encountered the situation “invariant proved by TLAPS but counter-example found by Apalache”?

Thanks for your time and advice!

[Stephan Merz]

Hello,

I am assuming that the counter-example produced by Apalache is legitimate. You can also try to use TLC to check if an invariant is inductive by indicating the invariant predicate as the initial state predicate, i.e. writing

INIT Inv

INVARIANT Inv

in the config file. (This works only if TLC can enumerate the states satisfying the invariant, Apalache is indeed better suited to this task.)

Could you please check if the proof of Inv /\ [Next]_vars => Inv’ is still accepted by the current version of TLAPS [1] and, if so, open an issue on GitHub [2]?

And indeed, if the source state of the counter-example is unreachable, this indicates that the invariant is too weak.

Thank you,

Stephan

[1] https://github.com/tlaplus/tlapm, build from source as described in DEVELOPING.md

[2] https://github.com/tlaplus/tlapm/issues

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c1468469-ee09-428e-9645-c7c47833fe44n%40googlegroups.com.

[Igor Konnov]

Hi Weining Cao,

Seconding what Stephan wrote. The most important question is whether
the counterexample produced by Apalache looks feasible to you. The
prestate does not have to be reachable from the initial states, as
inductive invariants usually over-approximate the set of the initial
states. It would definitely help us to know whether Apalache or TLAPS
has a bug in your case.

Best,
Igor

> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/E6AE8F7B-D35E-4C8F-9CED-D3D2769A3A89%40gmail.com.