On Mon, Mar 30, 2020 at 2:15 PM Reed Oei <reedoei2@illinois.edu> wrote:
Hello,
I am encountering a bug where Spot segfaults when I try to postprocess a relatively large automaton. I have uploaded the file to http://reedoei.com/files/smaller-inner.aut.zip; it has 113930 states and 1537155 edges. I tried to come up with a smaller example but was having trouble doing so. Below is the sequence of commands, using the Python bindings, to reproduce this bug for me:
import spot A = spot.automaton('smaller-inner.aut') B = A.postprocess('BA', 'Deterministic', 'Low') # Crashes here B.save('postprocessed.aut')
I also tried using various other others for postprocess such as Small and Low, or Any and High (because Any and Low/Medium does nothing).
Hi Reed, This is a HUGE automaton to pass to postprocess. Running % autfilt --det --low smaller-inner.aut did not finish within 20 minutes, so I interrupted it and noticed the code was busy in the simulation-based reduction code. The simulation-based reduction is notoriously slow: it uses a BDD-based representation that requires one variable per equivalence classe (maybe the number of states), and when too many variables are used, it's possible that the garbage collection for the BuDDy library crashes with a stack overflow (see https://gitlab.lrde.epita.fr/spot/spot/-/issues/396 ) Maybe that's the crash you got. You can disable simulation-based reductions with % autfilt -x simul=0,ba-simul=0,det-simul=0 --det --low smaller-inner.aut but this also did not finish withing 20 minutes. When I interrupted it it was stuck in the determinization code. Running an exponential algorithm on an automaton with soo many states is unlikely to finish quickly. Running the same command without requiring a determinisation, and without simulation-based reductions worked and reduced the automaton to 107083 states: % autfilt -x simul=0,ba-simul=0 --small --low smaller-inner.aut -- Alexandre Duret-Lutz