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

*From*: Jam <wawrzynchonewicz@xxxxxxxxx>*Date*: Mon, 14 Oct 2019 12:54:01 -0700 (PDT)

Hello. I am trying to visualize the state graph generated during model checking of my model. I have gotten everything to work, but I have a problem where the generated graph uses all found states instead of the more obvious choice of distinct states. I have not found any settings or documentation on how to influence the graph generation process. Is this possible? I have read something about the "optional parameters of dump" in this issue, but I have not found any documentation on where to specify these flags, or what other flags there may be.

-- The graph that I'm generating is too large for TLC to complete on its own (I get graphviz errors), however i found that it still generates the .dot files which i use to generate the graph images myself. By searching this file i found that the amount of nodes is the same as the amount of all found states in the model checking results. This makes the graph look very unreadable.

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/021b7e89-5722-4f92-80ea-3aa963a8df6f%40googlegroups.com.

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

- Prev by Date:
**[tlaplus] Re: Ideas for model-checking probabilistic consensus systems?** - Next by Date:
**Re: [tlaplus] State graph of distinct states** - Previous by thread:
**Re: [tlaplus] Current TLA Proof Rules** - Next by thread:
**Re: [tlaplus] State graph of distinct states** - Index(es):