15 Oct
2021
15 Oct
'21
9:21 a.m.
"Bhatia, Amit RTX" <amit.bhatia2(a)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