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

*From*: Jam <wawrzynchonewicz@xxxxxxxxx>*Date*: Mon, 14 Oct 2019 13:53:31 -0700 (PDT)*References*: <021b7e89-5722-4f92-80ea-3aa963a8df6f@googlegroups.com> <1c80acb0-6811-7d3c-3cb1-11e1be0c6354@gmail.com>

Hi. I just wanted to post about this. By an unlikely coincidence, the number of occurrences of "fontcolor" (which i now realize also incorrectly counts the edges) was the same as the number of all states in my state space. It matched so i didnt give it another thought. There are only 155 states in total but its still a pretty weird coincidence. Anyway, I will still leave this question here in case somebody else would like to know about the dump options that you explained. Thank you for the answer!

On Monday, October 14, 2019 at 10:44:36 PM UTC+2, Hillel Wayne wrote:

-- On Monday, October 14, 2019 at 10:44:36 PM UTC+2, Hillel Wayne wrote:

Hi Jam,

TLC generates the graph of the distinct states. The difference between "states" and "distinct states" is that "states" also includes also counts when two different behaviors reach the same state at some point. That would show up as additional edges, not additional nodes.

To get a dump of the state graph, you can generate a dumpfile by adding -

dump path_to_fileunderTLC Options > Parameters > TLC command line parameters. You can read about other TLC parameters here.H

On 10/14/19 2:54 PM, Jam wrote:

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/021b7e89-5722- .4f92-80ea-3aa963a8df6f% 40googlegroups.com

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/7822df53-5429-4b45-bc95-86b88bf4e4e8%40googlegroups.com.

**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:
**Re: [tlaplus] State graph of distinct states** - Previous by thread:
**Re: [tlaplus] State graph of distinct states** - Next by thread:
**Re: [tlaplus] State graph of distinct states** - Index(es):