[Spot] Re: Bug when checking for automata emptiness in print_hoa()

"Beutner, Raven" <raven.beutner@cispa.de> writes:

Dear spot Team,

I think I have found a bug in the emptiness checker of spot.

Thank you for the report, Raven. It's actually a bug in the automaton parser: Spot supports only one initial state, so if you give it a HOA file with multiple initial state, those will be merged to obtain an equivalent automaton. However that merging code was written with transition-based acceptance in mind and did not work correctly will with state-based automata. https://gitlab.lre.epita.fr/spot/spot/-/issues/522