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 self-loops. This is a problem if the automaton is later passed to sbacc()
(for transformation to state-based acceptance), because all these different self-loops will product an extra state. (The state-based versions of these automata have respectively 28 and 49 states.)
One easy optimization we could apply is that for each sub-acceptance-formula 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()
)