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

[tlaplus] Exploration of state-space by TLC in the simulation mode


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?


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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CA%2B13N%3DuGRXcNLs1%2BjVDWRMbYhHMqh0XZ8iD0qiXed8MCims-0w%40mail.gmail.com.