Hi
In the simulation mode, here's my understanding of how TLC explores the state-space of a specification. It starts with an initial state and then explores a behavior by going through a sequence of actions upto the -depth parameter. Each action in the sequence is chosen at random. Once TLC is done with one behavior, it starts again from the initial state and explores another behavior. It continues doing this till the user askes it to stop.
To me, this seems like a depth-first exploration of the state-space (as opposed to breadth-first exploration employed in the model checking mode). Is my understanding correct?
thx
aman