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.