State graph of distinct states

47 views
Skip to first unread message

Jam

unread,
Oct 14, 2019, 3:54:02 PM10/14/19
to tlaplus
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.

Hillel Wayne

unread,
Oct 14, 2019, 4:44:36 PM10/14/19
to tla...@googlegroups.com

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 tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/021b7e89-5722-4f92-80ea-3aa963a8df6f%40googlegroups.com.

Jam

unread,
Oct 14, 2019, 4:53:31 PM10/14/19
to tlaplus
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!
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

Markus Kuppe

unread,
Oct 14, 2019, 5:11:53 PM10/14/19
to tla...@googlegroups.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
Reply all
Reply to author
Forward
0 new messages