About the definition of stuttering, and about liveness checking

[n s]

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

[Andrew Helwer]

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.

Andrew Helwer

[Stephan Merz]

Perhaps the confusion is related to what TLC considers to be a stuttering step and what it considers to be a deadlock. A TLA+ spec in canonical form is written as

Init /\ [][Next]_vars /\ L

where vars is a tuple that includes all the variables occurring in the specification. This specification allows for stuttering steps where vars’ = vars. In particular, every state has itself as a successor state, and so it would seem that no state is deadlocked.

TLC takes the pragmatically useful decision to flag a state s as deadlocked if no state s’ exists such that (s,s’) |= Next. In particular, TLC will not consider s to be a deadlock state if Next includes a disjunct that implies vars’ = vars, although all transitions leading to successors satisfying this disjunct are indeed stuttering transitions in the sense of TLA+. For example, the PlusCal translator generates such a disjunct for states where the algorithm has terminated (reached the implicit "Done" label). You could say that TLC makes a distinction between stuttering transitions that are explicitly allowed by Next and those that are implicit in the subscript vars.

For your second question, TLC can only check finite state spaces, independently of checking safety or liveness properties. In many cases, it is not enough to provide explicit constants for specification parameters, but you also need to impose a constraint such as bounding the length of a buffer etc. In this sense, TLC does bounded checking. However, within this bounded state space, TLC does full exploration, and in particular tries to compute lassos as counter-examples for liveness properties.

Hope this helps,

Stephan

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