Exploration of state-space by TLC in the simulation mode

[Aman Shaikh]

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

[Stephan Merz]

I believe your description is correct, and so it is neither depth-first nor breadth-first search but random exploration.

Stephan

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

[Aman Shaikh]

Ah, I see. Thanks Stephan.

aman