You are correct those formulas are stuttering insensitive. It still might be easier to prove the [][\A t \in TaskId: t \in FinalizedTask => t \in FinalizedTask']_vars formula, though. It implies your intended formula, and can also be easily analyzed at the level of a single step. Here is a derivation:
WTS [][P => P']_v => [](P => []P):
Some theorems:
(a) [][]P = []P
(b) [](P => Q) => ([]P => []Q)
(c) []P => P
(d) (P /\ []P') => []P
[][P => P']_v [intro start]
[](P => P' \/ v' = v) [by definition of [P]_v]
[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P') \/ v' = v) [long expansion of =>]
[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P') \/ P = P') [P = P' if variables are unchanged]
[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P') \/ (P /\ P') \/ (~P /\ ~P')) [expanding = for boolean predicates]
[]((~P /\ P') \/ (~P /\ ~P') \/ (P /\ P')) [dropping duplicate (P /\ P') and (~P /\ ~P')]
[](P => P') [contracting definition of =>; we've incidentally shown here our starting formula is stuttering-insensitive]
[][](P => P') [by theorem (a)]
[]([]P => []P') [implication by theorem (b)]
[](P => []P') [implication by theorem (c)]
[](~P \/ (P /\ []P')) [expanding definition of =>]
[](~P \/ []P) [implication by theorem (d)]
[](P => []P) [contracting definition of =>; goal reached!]
Andrew
Hi Andrew,
Thank you for response. I made a mistake when typing the message that changes its entire meaning. There is no prime on P.
I am interested in the properties of the form:
[](P => []P) and \A x \in S: [](P(x) => []P(x))
It seems to me that these formulas are valid (insensitive to stuttering).
Quentin
On Wednesday, November 26, 2025 at 10:35:19 PM UTC+1 Andrew Helwer wrote:
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.
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
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.
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/00c1252f-6b80-499d-8f8f-dfb434d3f07an%40googlegroups.com.