Hello Spot Team, I recently came across your tool while searching for existing implementations to convert an LTL formula with finite semantics into a finite automata together with rendering it pictorially (e.g., using graphviz tool) - I was wondering if you have any examples of how this could be accomplished when the end goal is also to plot the automaton using GraphViz? I did read through https://spot.lrde.epita.fr/tut11.html (Translating an LTL formula into a monitor) and https://spot.lrde.epita.fr/tut12.html (Working with LTL formulas with finite semantics), but I am not sure if the output is already compliant with Graphviz's required format or some parsing is required (my knowledge of Graphviz is also fairly limited).
Thanks, Amit
Amit Bhatia Raytheon Technologies Research Center Berkeley, CA Amit.Bhatia2@rtx.commailto:Amit.Bhatia2@rtx.com
"Bhatia, Amit RTX" amit.bhatia2@rtx.com
I was wondering if you have any examples of how this could be accomplished when the end goal is also to plot the automaton using GraphViz? I did read through https://spot.lrde.epita.fr/ tut11.html (Translating an LTL formula into a monitor) and https:// spot.lrde.epita.fr/tut12.html (Working with LTL formulas with finite semantics), but I am not sure if the output is already compliant with Graphviz’s required format or some parsing is required (my knowledge of Graphviz is also fairly limited).
Hi Amit,
The pictures displayed on tut12.html are rendered by GraphViz.
The code shown produce automata in the HOA format, but you can change it to produce it in a format suitable for GraphViz: add --dot to the autfilt command in the shell version, replace to_str('hoa') by to_str('dot') in the Python version, or print_hoa(...) by print_dot(...) in the C++ version.)
Some discussion about the different output formats and how to customize the GraphViz output can also be found at https://spot.lrde.epita.fr/oaut.html
-
Alexandre Duret-Lutz -
Bhatia, Amit RTX