Hi Agost,
here are the instructions to run TLC and generate an "action space coverage" graph:
* Save the graph in a file named "MySpec_actions.dot" by running TLC with the following command:
-simulate num=N,stats=[basic|full] MySpec.tla
* Replace 'N' with a reasonable number of behaviors to generate.
* Choose either "basic" or "full" for the 'stats' parameter, depending on the desired level of detail in the generated graph.
* Open “MySpec_actions.dot" with the GraphViz tools.
Markus
> --
> 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/CAFG8yPTdN%2B42OjzjAFRbjpzBb-RL6cwC21pBFbntFip5x%2Bz6CQ%40mail.gmail.com.