Re: [tlaplus] State graph of distinct states

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

On 14.10.19 13:43, Hillel Wayne wrote:
> To get a dump of the state graph, you can generate a dumpfile by adding
> -dump path_to_fileunder TLC Options > Parameters > TLC command line
> parameters. You can read about other TLC parameters here
> <https://lamport.azurewebsites.net/tla/tlc-options.html>.


In order for TLC to generate the dump in dot/gv format, the command is
actually "-dump dot path_to_file" (note the "dot").

The command above is automatically set if one checks "Visualize state
graph..." on the "TLC Options" page of a Model:  With a model with name
"Model_1", path_to_file will be Spec.toolbox/Model_1/Model_1.dot from
where the dump can be opened with e.g. xdot, Gephi, or Cytoscape (should
the Toolbox's built-in visualization timeout).

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4c40a1e3-9892-3bc4-9149-fb4c78c010fe%40lemmster.de.