| 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
On 29 Oct 2025, at 05:25, 'Weining Cao' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
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.
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/E6AE8F7B-D35E-4C8F-9CED-D3D2769A3A89%40gmail.com.
|