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.
MarkusOn 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?