Re: [tlaplus] Is ENABLED P always stuttering-insensitive?

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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.helwer@xxxxxxxxx> 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUW4NW%2B_nY4QoJMNhQgCTFVo4%3DjvrY9R%3D6ZHDyn0Z1zobg%40mail.gmail.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/894DD133-24EC-4276-8065-D234BC305085%40gmail.com.