Hi Pierre,

Pierre Ganty pierre.ganty@imdea.org writes:

When invoking `autfilt sub.aut --included-in=sup.aut` on the two enclosed Buchi automata with Spot 2.10 I am getting:

Too many acceptance sets used.  The limit is 32.

Complementing sup.aut is done via determinization to parity automata. If the parity automaton requires more colors than supported, the above exception is raised. You could compile spot with --enable-max-accsets=64 or more and see if it helps, but on such a large automaton I suspect the run time of determinization will be prohibitive.

With Spot 2.9.7 I was getting a non-terminating execution.

Spot 2.9.x was trying to simplify sup.aut with some simulation-based reduction before determinizing it, but our simulation-based reduction is very slow on large automata. Spot 2.10 is no longer performing simulation-based reductions on automata that have more than 4096 states (sup.aut has 21396 states); it jumps straight into the determinization in this case.

If Spot 2.9.x was given enough time to do the initial reduction (hours? days? years? who knows!), it would then have failed in the determinization with the same error. So this is progress: Spot 2.10 is failing faster :-)

Alexandre