21 Nov
2019
21 Nov
'19
4:59 a.m.
Hello,
We are using the Python bindings in Spot to translate LTL to monitors, as
described at https://spot.lrde.epita.fr/tut11.html.
We have a question: Is it possible to set an option that will preserve all
the atomic propositions, even when they cannot affect the automaton? For
example, with the formula "Ga & Fb", the resulting monitor would not
include "b".
Is there a way to do this?
Thanks,
Dominick