I will note that I'm pretty sure the formula [](\A t \in TaskId: t \in FinalizedTask => t' \in FinalizedTask) is coincidentally stuttering insensitive even when not boxed, simply because it states that something does not change and things do not change in stuttering steps. Still, it is a good habit to box properties involving primed variables.On Wed, Nov 26, 2025 at 1:31 PM Andrew Helwer <andrew...@xxxxxxxxx> wrote: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.AndrewOn Wed, Nov 26, 2025 at 12:42 PM Quentin DELAMEA <qdel...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/a6b6effd-2e5b-42ec-96e6-91f47b4efdadn%40googlegroups.com.