a case where reduce_parity() causes more colours
Consider the following three formulas, converted to deterministic Streett automata by ltl2tgba 2.7.5:
ltl2tgba-2.7.5 -G -D '(GFp0 | FGp1)' '(GF!p1 | FGp2)' '(GF!p2 | FG!p0)'
It's easy to see that since the colors in each automata are synchronized with a different atomic proposition, when we take the conjunction of the three formulas we can use an acceptance condition with only three colors (as many as atomic propositions). This is was ltl2tgba 2.7.5 used to produce:
ltl2tgba-2.7.5 -G -D '(GFp0 | FGp1) & (GF!p1 | FGp2) & (GF!p2 | FG!p0)'
Internally the product generated from the previous 3 automata uses 6 colors, but because we can form 3 pairs of colors that evolve together (along with the matching atomic proposition), duplicate colors are removed and their number reduced to 3.
In Spot 2.8, we introduced the
reduce_parity() function, which takes any parity automaton and rewrite it to use the minimal number of colors. In these cases, since
Fin(1)|Inf(0) is also
parity min 2, the
reduce_parity() function is called to attempt to reduce the number of colors. Here, the numbers of colors stay the same, but interpreted as a parity min acceptance, it makes no sense to keep a transition labeled by both ⓿ and ❶: we keep the smallest color, ⓿, and merge the two transitions with this color in a single edge.
The result is:
ltl2tgba -G -D '(GFp0 | FGp1)' '(GF!p1 | FGp2)' '(GF!p2 | FG!p0)'
So far this does not look bad, however we have lost the synchronization between letters and colors. Therefore when we translate the conjunction of these three formulas, we are no longer able to find duplicate colors in the resulting product, which now uses 6 colors.
ltl2tgba -G -D '(GFp0 | FGp1) & (GF!p1 | FGp2) & (GF!p2 | FG!p0)'
This regression in the number of colors output was reported by Juraj Major. The conjunction formula is ψ₆ is section 5 of our ATVA'19 paper.