[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] State graph of distinct states

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).


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.