17 Nov
2021
17 Nov
'21
3:52 p.m.
Hi Pierre,
Pierre Ganty <pierre.ganty(a)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