20 Apr
2020
20 Apr
'20
12:13 p.m.
On Sun, Apr 19, 2020 at 6:33 PM Reed Oei <reedoei2(a)illinois.edu> wrote:
Thanks for the response. I decided to look into the
isuse a little bit, and it seems like the problem is mainly in apply_rec() in bddop.c. I
was able to rewrite it into a stack-based version, which seems to have fixed the crashing
(though postprocessing still takes forever, which is the original result I was expecting,
anyway). I also tried my new version on the command from that issue you linked
(https://gitlab.lrde.epita.fr/spot/spot/-/issues/396), and that also works now, though it
takes about 4-5 hours to finish.
It's probably not the ideal implementation, but I attached a patch file containing
the fix, if you are interested. It seems to work (all the tests pass), and it's about
the same speed in most cases.
Hi Reed !
Thank you very much for this implementation! I've pushed it on a
branch and updated the issue with some comments until we can improve
upon this patch. Clearly this kind of implementation needs to be
generalized to all recursive BDD functions, but it's encouraging that
the original issue can be fixed only by changing apply_rec. Unless
you are willing to do it, I'll do it eventually, but that will be
after the release of Spot 2.9 (which we hope will by the end of the
month).
Best regards,
--
Alexandre Duret-Lutz