Is there a way to dump error trace as a dot format file?

[Benedict Xu]

I checked current-tools.pdf but didn't find such an option.

I also didn't find such an option on the TLC model checking results page.

The full dot format file is usually quite big. From time to time, I'm just interested in graphviz the error trace and share it with other folks easily.

Maybe there is a way to get the error trace from the full dot format dump?

[Markus Alexander Kuppe]

Hi Benedict,

newer builds of TLC can dump a trace in two pre-defined formats (TLA+ and Json) and allow you to define your own formats. Look for “dumptrace” at https://github.com/tlaplus/tlaplus/blob/master/general/docs/current-tools.md#command-line-options. Adding support for GraphViz would essentially require writing a GraphViz module that serializes a counterexample defined in TLA+ into GraphViz.

Markus

[Benedict Xu]

Thanks, Markus. Having a support for dot format will be great. Should I file a feature request for this?

[Hillel Wayne]

It may be easier to dump as TLA+ or JSON and then convert that dump to Graphviz with another tool.

H

--
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/6c9f9ee1-59bb-463c-a43c-981e4302857fn%40googlegroups.com.

[Markus Alexander Kuppe]

Yes, please open an issue on the CommunityModules [1].  Additionally, a GraphViz module could prove beneficial in generating animations [2], among other potential applications.

M.

[1] https://github.com/tlaplus/CommunityModules/issues
[2] https://github.com/will62794/tlaplus_animation