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

["'Weining Cao' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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!

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