simplification of colors based on acceptance condition
Consider the following two automata:
ltl3tela D 1 '(G!a  G!b  G!c) & (FG!a2  GFb2  GFc2) & (GFc2  FG!b2  GFa2)'
ltl2tgba D G '(G!a  G!b  G!c) & (FG!a2  GFb2  GFc2) & (GFc2  FG!b2  GFa2)'
The automata have roughly the same structure, except that ltl2tgba
outputs many more selfloops. This is a problem if the automaton is later passed to sbacc()
(for transformation to statebased acceptance), because all these different selfloops will product an extra state. (The statebased versions of these automata have respectively 28 and 49 states.)
One easy optimization we could apply is that for each subacceptanceformula of the from Fin(x)Inf(y)
where x appear only once in the entire formula, we can remove x from every transition that have y. I believe applying that on the second automaton is enough to get a result isomorphic to the first one.
I've thought about two directions we can generalize this rule.

On way is to generalize the type of patterns we can recognize. For instance with
(Inf(y₁)&Inf(y₂)&...&Inf(yₙ))Fin(x₁)Fin(x₂)...Fin(xₙ)
, for each xᵢ that appears only once in the acceptance condition, we can remove xᵢ from every transition where y₁,y₂,...,yₙ are all present. But another type of patterns is that anytime a subformula has the shape of a parity max or parity min acceptance condition (up to a suitable renumbering of colors), then we can simplify each transition by keeping the max/min of the relevant colors (making sure not to erase colors that are also used elsewhere in the acceptance condition). Maybe a rule that generalize these two patterns is to say that if we have(Inf(y₁)&Inf(y₂)&...&Inf(yₙ))  f(x₁,...,xₙ)
we can remove all xᵢ from transitions where y₁,y₂,...,yₙ are all present assuming that those xᵢ are only used once in the acceptance condition. We also need a dual rule with(Fin(y₁)Fin(y₂)...Fin(yₙ))&f(x₁,...,xₙ)
. 
Another way is to not consider transitions individually but cycles. Using the
Fin(x)Inf(y)
pattern for simplicity, we can remove x from all transitions on a cycle that necessarily sees y. (This could be found by finding the transitions that are not part of any SCC once transition labeled by y are removed, or maybe withpropagate_marks_vector()
)