[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] About single process system, fairness, and depth-first search option

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,

On 19 Dec 2016, at 21:54, venkateshpra...@xxxxxxxxx wrote:


So, how does TLC deal with systems with finite executions?  Specifically, the system above reaches the "Done" location/state where there is no outgoing transition (or there is a self-looping transition that is always enabled).  In such states, does TLC treat the absence of out-going transition (or self-looping transitions) as stuttering?

How about the difference between (1) and (2)?  Why does checking DFS option result in no error while unchecking DFS result in error (under the same unspecified fairness conditions)?

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.