[tlaplus] About the definition of stuttering, and about liveness checking

[n s <nedsri1988@xxxxxxxxx>]

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

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/394e47df-ac88-4e03-90f5-303d11658669n%40googlegroups.com.