improve production of weak automata for persitence formulas
ltl2tgba '(a W c) & FGa'
returns an automaton that is tagged as inherently-weak.
Questions: since the translation detects that the input is a persistence formula, why do we only declare the result as inherently-weak, are there cases where the output is not weak? Could we ensure some weak output?
Note: in the above example we could easily detect that the automaton is very-weak, which implies weak.
Better tagging of automata as weak will improve the performance of products (#350 (closed)).