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