Running it with the basic option on the faulty alarm clock spec from the article where the Ring action is never enabled gives this:
Best,
Agost
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
> On Apr 3, 2023, at 2:26 PM, Agost Biro <agostbiro@xxxxxxxxx> wrote:
>
> Hello,
>
> I read in the Current and Future Tools for Interactive TLA+ article that TLC can make a graph of actions that enable other actions, but it's not documented or integrated into the GUI. I'm wondering if anyone has more info on this? A code example would be most welcome.
>
> Best regards,
> Agost
>
>
> --
> 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/CAFG8yPTdN%2B42OjzjAFRbjpzBb-RL6cwC21pBFbntFip5x%2Bz6CQ%40mail.gmail.com.
--
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/C73E6DFC-0AF0-422E-8D51-9B6402E042EF%40lemmster.de.