Re: [tlaplus] Exploring TLC checkpoint states

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 08.01.2016 14:27, Jaak Ristioja wrote:
> A model checking run seems to be taking too long to complete. Is it
> somehow possible to explore the graph of visited states using the
> periodical checkpoint data?

Hi Jaak,

what makes you think it is taking longer than expected? Is TLC still
making progress and does it find new distinct states? What does the
graph of the state queue size look like? It usually reassembles a parabola.

The checkpoint data is pretty much useless with regards to your problem.
You can however, look at the end of the state queue file. It contains
the unexplored states in Java-serialized form. However, you would have
to roll your own implementation that deserializes N states from the
state queue file.

Cheers
Markus