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

[venkateshpra...@xxxxxxxxx]

Stephan, 

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