Is ENABLED P always stuttering-insensitive?

[Andrew Helwer]

In general, action-level expressions that contain primed variables have to be boxed in [][expr]_vars or <><<expr>>_vars to ensure stuttering insensitivity. SANY will rightfully complain if you try to write an unboxed expression like [](x' = 0), although this relies on syntactic pattern-matching instead of a full stuttering sensitivity checker. ENABLED expressions are curious counterexamples to this. TLC will happily check the expression ENABLED (x' = 0) as an ordinary invariant. Are ENABLED expressions thus always stuttering-insensitive?

Andrew Helwer

[Stephan Merz]

For any action A, ENABLED A is a state predicate that is true in those states s that have a successor state t such that A holds of (s,t). Since it is enabled over a single state, ENABLED A is stuttering insensitive.

Stephan

On 26 Jan 2026, at 01:18, Andrew Helwer <andrew...@gmail.com> wrote:

In general, action-level expressions that contain primed variables have to be boxed in [][expr]_vars or <><<expr>>_vars to ensure stuttering insensitivity. SANY will rightfully complain if you try to write an unboxed expression like [](x' = 0), although this relies on syntactic pattern-matching instead of a full stuttering sensitivity checker. ENABLED expressions are curious counterexamples to this. TLC will happily check the expression ENABLED (x' = 0) as an ordinary invariant. Are ENABLED expressions thus always stuttering-insensitive?

Andrew Helwer

--
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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUW4NW%2B_nY4QoJMNhQgCTFVo4%3DjvrY9R%3D6ZHDyn0Z1zobg%40mail.gmail.com.

[Andrew Helwer]

Thanks, Stephan! I guess that makes ENABLED a fairly unique operator. Every other operator either raises the level of its operands (like [] or ' or <>) or leaves them unchanged (=>, =, etc.) but ENABLED is the only one that seems to take an action-level expression and decrease it to a state-level expression.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/894DD133-24EC-4276-8065-D234BC305085%40gmail.com.