25 Sep
2018
25 Sep
'18
9:59 a.m.
On Sun, Sep 16, 2018 at 11:50 AM Andreas Tollkötter
<andreas.tollkoetter(a)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
--
Alexandre Duret-Lutz