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

[tlaplus] Re: Is there a way to dump error trace as a dot format file?

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
On Tuesday, February 28, 2023 at 12:12:19 PM UTC-8 gonad...@xxxxxxxxx wrote:

Thanks, Markus. Having a support for dot format will be great. Should I file a feature request for this?
On Tuesday, February 28, 2023 at 1:16:40 AM UTC+1 Markus Alexander Kuppe wrote:
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

On Monday, February 27, 2023 at 3:41:32 PM UTC-8 gonad...@xxxxxxxxx wrote:
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?

--
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/2df7657f-32d2-4efc-a86f-a78efe9032a5n%40googlegroups.com.