On Sun, Sep 16, 2018 at 11:50 AM Andreas Tollkötter andreas.tollkoetter@rwth-aachen.de wrote:

Hello,

with the currently newest version of Spot 2.6.1, the following behavior occurred for me, which I would call a bug. I attached a DOT file of a deterministic parity automaton which was written by "autfilt --dot --highlight-languages". What is notable that (among other pairs), states 10 and 66 are marked as language-equivalent states. Their "a1"-successors, 30 and 62 are not equivalent however, so something must be wrong here. I assume a potential cause is that there are a total of 18 non-trivial equivalence classes but only 16 different colors defined to be used by Spot, so some are used for multiple classes? If that is the case, I feel like there should be at least a warning output by "autfilt" when this happens.

Hi Andreas,

Yes. The code is split in two parts. spot::highlight_languages(aut) attach a unique (color) number to each group of 2+ states that represent the same language. Then spot::print_dot(aut) uses that to color the states, but as it has only a palette of 16 colors, they wrap around. We should probably teach print_dot() to be more verbose when this happens. E.g., add a "[n]" marker (with n replaced by the color number) near to each state when the highest color number is larger than 16.

In the meantime, you can get an accurate list of language numbers by using "autfilt -H1.1 --highlight-lang..." (look at the "spot.highlight-states:" property, it's followed by a list of the form state1 color1 state2 color2 ...) Or by using the output of language_map(aut) in Python