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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Mon, 14 Oct 2019 14:11:45 -0700*References*: <021b7e89-5722-4f92-80ea-3aa963a8df6f@googlegroups.com> <1c80acb0-6811-7d3c-3cb1-11e1be0c6354@gmail.com>

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.

**References**:**[tlaplus] State graph of distinct states***From:*Jam

**Re: [tlaplus] State graph of distinct states***From:*Hillel Wayne

- Prev by Date:
**Re: [tlaplus] State graph of distinct states** - Next by Date:
**[tlaplus] Beginner Question: Working with the Prisoners Example** - Previous by thread:
**Re: [tlaplus] State graph of distinct states** - Next by thread:
**[tlaplus] Beginner Question: Working with the Prisoners Example** - Index(es):