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_file under TLC 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