1

When using TLA+ and TLC, if I want to generate a visualizable state graph, I can check the checkbox of "TLC options"->"feature"->"Visualize state graph after completion of model checking". This can generate a pdf file of the state graph as well as a dot file which represents the structure of the state graph.

However, the dot file does not include the label information of the edge, which means it does not shows whether action is applied when the system transfers from one state to another.

So, the question is, how to make TLC add label information for action name in its producted dot file?

I am using TLAToolbox-1.7.1-win32.

fwhdzh
  • 21
  • 3

1 Answers1

1

You can edit "TLC options"->"Parameters"->"TLC command line parameters" and add

-dump dot,actionlabels example

This will produce a dot file named example.dot which includes the action name as the label of an edge.

If you use this, the TLC will not produce pdf file of state graph anymore. However, you can produce the graph yourself with the dot file.

fwhdzh
  • 21
  • 3