some case where simulation-based reduction is slow
The following are cases extracted from the same Pecan run mentioned in #566 (closed) and coming from an email from @pierreganty. On these automata, running autfilt --small
takes increasingly more time, because of simulation-based reductions.
postproc126.hoa.xz postproc144.hoa.xz postproc162.hoa.xz
% autfilt --small postproc1{26,44,62}.hoa --stats='%S->%s (%X APs, %r seconds)'
126->16 (16 APs, 4.2536 seconds)
144->18 (18 APs, 18.7157 seconds)
162->20 (20 APs, 140.485 seconds)
I have a couple of extra larger automata, but the files start to be very large and I don't think it is necessary to attach them here.
Running valgrind --tool=callgrind
on the smallest of these three shows the following profile
Beware that the time reported with %r
above do not take parsing into account, but the above profile does.
On the profile, we can see that 91.5% of the time is spent doing 4 simulation-based reductions (2 forward, 2 backward), and that 35% of the time is in merge_edges()
. I suspect we have a lot of edges to merge, because build_results
uses minterms_of
to iterate over the 2^AP possible labels. Surely this can be improved. Maybe we don't need to merge any edges between iterations of the simulation-based reductions: can we wait the end? Second, we should probably be able to replace the minterms_of
iteration by an iteration a label basis computed by the edge_separator
introduced for #566 (closed). Actually the label basis of the automaton was used to declare aliases in the HOA file to shorten it greatly: there are only 90 of them in this automaton, so that's really small compared to 2^16.