5 Oct
2021
5 Oct
'21
10:59 a.m.
Roei Nahum <roeina(a)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=deb…
just make sure you compile it with './configure --disable-devel ...'
Alexandre