Weak fairness requires that an action must eventually occur if it is always enabled. In the case of termination or deadlock, no action is enabled anymore. Again, the formula [][Next]_vars allows for transitions that do not change vars, hence stuttering may always occur, and it must occur if Next cannot be true. In other words, finite executions are represented as infinite behaviors with infinite stuttering from some point onwards. You will have noticed that the PlusCal translator adds the disjunct \/ (* Disjunct to prevent deadlock on termination *) (pc = "Done" /\ UNCHANGED vars) to the definition of Next, which represents an explicit stuttering transition in the case of termination, beyond the implicit stuttering transition that comes from the definition of Spec. As explained in the comment, this disjunct eliminates the TLC error message about a deadlock because TLC can construct a successor state when the program has terminated. (This error message could confuse beginners when checking programs that may terminate.) However, the action <<Next>>_vars, which is short-hand notation for (Next /\ vars' # vars) is not enabled when pc="Done", and therefore WF_vars(Next), which abbreviates (<>[]ENABLED <<Next>>_vars) => ([]<><<Next>>_vars) still allows infinite stuttering to happen, independently of the presence of that disjunct. In fact, you cannot require the occurrence of stuttering transitions using TLA+. As for your question about depth-first vs. breath-first search, in my experiments depth-first search never finished on your example in the sense that the progress bar was still being displayed without any notable processor activity. Maybe a TLC expert can explain what's happening. I cannot tell what the "result" of these runs was. Hope this helps, Stephan
|