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.com<mailto:Amit.Bhatia2@rtx.com>