Re: [tlaplus] Stuttering: abstraction vs. implementation

You are right: any TLA+ formula is insensitive to adding or removing a finite number of stuttering steps, and this implies (by the fact that safety properties are closed) that a safety specification tolerates adding indefinite stuttering. For the last observation, note that actions are modeled extensionally (as predicates over two states). If A and B are two actions that relate states s and t, there is no way of knowing which of them occurred, and this is true in particular if s and t agree on all variables of interest.

Stephan

On 29 Mar 2026, at 00:29, Younes <younesagma@xxxxxxxxx> wrote:

Hello,
I may be thinking about this the wrong way, but here’s my current understanding of stuttering on the implementation side. A real implementation step counts as “stuttering” only if, at the level of the spec, nothing observable changed. That seems to imply a few things: a safety spec by itself still allows the system to keep “doing nothing” forever unless progress is stated separately; stopping/termination is modeled as repeating the same final state forever; and if two different real events leave the abstract state unchanged, TLA+ will not distinguish them unless that difference is modeled explicitly. Is that basically right, or is there an important subtlety I’m missing?

--
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/58e1e6ab-9e7c-4053-a988-f919154b5d8bn%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/A7785E71-63C9-4028-BF4C-00B70C01330E%40gmail.com.