Re: [tlaplus] Graph of actions that enable other actions

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.