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>