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.