Hi,
Could you add a command-line option for ltl2tgba to invert the input formula before
computing the automaton?
Yes, it's trivial to do externally, but there are good reasons to have this option:
* this would remove an extra step from model checking toolchains (where the automaton is
built for the negation of a formula)
* if the formula goes through a toolchain, it's better to keep equivalence all the
way through to the automata, so that the user can easily see that the property has not
been broken by transformations, and also comprehend any formula-related diagnostics logged
by the tools.
Thanks,
Victor.