lemmy
commented
1 year ago We need a Graphviz module that defines an operator such as DotDiGraph with a graph and two lambdas as parameters that converts the graph into a string, formatted in dot notation. The input graph will be defined in the usual way, i.e., [vertices: V, edges: E] with V a set of elements and E a set of sequences/tuples, s.t. e \in E and e[1] \in V and e[2] \in V. The two lambdas format the label of a v \in V and e \in E, respectively (the labels of an edge e can be passed as its third, fourth, ... component):
DotDiGraph(G, VL(_), EL(_)) ==
....
Foo ==
DotDiGraph(SomeG, LAMBDA v: ToString(v.name), LAMBDA e: ToString(e[3]) \o "\n" \o ToString(e[4]))
To handle bigger graphs and because TLA+ string manipulation is limited, the DotDiGraph module will be overridden by a Java module override that actually converts the input graph into dot notation.
Given such a Graphviz module, "dumptrace" functionality can be implemented with almost no effort by passing TLC's Counterexample graph (impl) to the DotDiGraph operator and serializing its output to a file with IOUtils!Serialize.
Possibly related:
https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla https://github.com/nano-o/TLA-Library/blob/master/DiGraph.tla
Benedicto
Today the toolbox support dumping a trace in two pre-defined formats (TLA+ and Json) via the “dumptrace” option: https://github.com/tlaplus/tlaplus/blob/master/general/docs/current-tools.md#command-line-options.
Adding a support for GraphViz's DOT format will be super useful.
It would essentially require writing a GraphViz module that serializes a counterexample defined in TLA+ into GraphViz.