Roei Nahum roeina@nvidia.com writes:
Hi Roei,
When working with version 2.9.4 of Spot, I got an endless runtime when I tried to create a small BA of this formula: (!(G({(a)} |=> {(b)[*32]})))
Thanks to your help, I understood that there was a bug in the mechanism that should avoid the WDBA-minimization in cases it creates to much additional states. (alexandre opened an issue for me – https://gitlab.lrde.epita.fr/spot/spot/-/issues/443)
Was this bug fixed in any of the later versions?
Not in any released 2.9.x version, because the fix relies on some new feature. However the current development version is fixed.
Sorry 2.10 is taking so long to get out ; it is a unusually large update. It this point we are just polishing things an hope to have something ready by the end of the month.
I met some additional problematic formulas. Currently, my only option to process such formulas is to avoid the WDBA-minimization step.
Would you be able to test if they work well with the development version of Spot? You can download the tarball from https://gitlab.lrde.epita.fr/spot/spot/-/jobs/artifacts/next/browse?job=debi... just make sure you compile it with './configure --disable-devel ...'
Alexandre