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?
--