On Sun, Apr 19, 2020 at 6:33 PM Reed Oei reedoei2@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,