"Beutner, Raven" <raven.beutner(a)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