Re: [tlaplus] Prove properties of the form [](P => []P) with TLAPS

Minor point but formulas like [](P') are not - in general - stuttering insensitive. A formula F is stuttering insensitive if, for all possible behaviors, F satisfies a behavior if and only if F satisfies the same behavior with stuttering steps arbitrarily added or removed. All TLA+ formulas are supposed to be stuttering insensitive, but we currently don't have a fully-functional stuttering sensitivity checker. All of this is to say that the canonical stuttering-sensitive way to write your property would be [][\A t \in TaskId: t \in FinalizedTask => t' \in FinalizedTask]_vars, where [P]_v is a shorthand for P \/ UNCHANGED v. This is a bit easier to reason about than your formula and proving it should resemble an ordinary inductive proof of any [] property.

Andrew

On Wed, Nov 26, 2025 at 12:42 PM Quentin DELAMEA <qdelamea@xxxxxxxxx> wrote:

Hello everyone,

I am new to TLAPS and am trying to prove the properties of a basic spec I wrote. One of the properties is of the following form:
\A x \in S: [](P(x) => []P'(x))

I found an example of a proof for a similar property in the AsyncTerminationDetection_proof.tla module for the Quiescence property in the Examples repository.

Here is the proof that is provided:

THEOREM Stability == Init /\ [][Next]_vars => Quiescence
<1>. TypeOK /\ terminated /\ [Next]_vars => terminated'
BY DEF TypeOK, terminated, Next, DetectTermination, Terminate, RcvMsg, SendMsg, vars
<1>. QED BY TypeCorrect, PTL DEF Quiescence

I admit that I don't understand this proof and would like to have more details so that I can adapt it to my case. Also, how do I handle the case where property P depends on x?

The property I am trying to prove is:

\A t \in TaskId: [](t \in FinalizedTask => [](t \in FinalizedTask))

where TaskId is a constant set and FinalizedTask is a set that can evolve with the next-state action.

Thank you for your help,

Quentin

--
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/a6b6effd-2e5b-42ec-96e6-91f47b4efdadn%40googlegroups.com.