| 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C8237799-0683-447A-8DD2-02BB72369ADD%40gmail.com. |