[Spot] Potential Bug in Spot?

Alexandre Duret-Lutz adl at lrde.epita.fr
Tue Sep 25 09:59:11 CEST 2018


On Sun, Sep 16, 2018 at 11:50 AM Andreas Tollk├Âtter
<andreas.tollkoetter at 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


More information about the Spot mailing list