The x' = x action will result in a stuttering step. Deadlock means no action in your system is enabled. So if you define a stuttering action then your system will never deadlock. It is common in specs to define a stuttering action to indicate program termination once your algorithm has succeeded, so that it won't be mistaken as deadlock.
On Wednesday, October 9, 2024 at 3:08:21 PM UTC-4 n s wrote:
This post is regarding a confusion that's been at the back of my mind for a while. The Specifying Systems book says that stuttering step is defined as one that leaves unchanged all the variables appearing in the formula (ie the spec). If I have a spec with one variable x and a step like "x' = x", this does not change x yet I don't believe its considered a stuttering step. So how does the definition exclude steps such as this? I ask this because stuttering shows up in various places such as what constitutes a finite trace, what is deadlock, etc. so I'd like to know how transitions such as the above are not considered deadlock for example.
A somewhat related question is regarding the line in 14.3.5 (Limitations of Liveness Checking) "To get TLC to terminate, we must provide a constraint that limits it to generating a finite number of reachable states" I was surprised to see this. This seems more akin to bounded liveness checking than true checking. Does TLC not look for lassos?
thanks