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

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


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)?