Too many acceptance sets used. The limit is 32.

gaperez64 / acacia-bonsai

A minimal implementation of reactive synthesis via universal co-Buchi automata using antichains

GNU General Public License v3.0

4 stars 3 forks source link

Too many acceptance sets used. The limit is 32. #31

Closed gaperez64 closed 1 year ago

gaperez64 commented 1 year ago

We inherit this issue from spot I think. For an example of this, see https://www.starexec.org/starexec/secure/details/pair.jsp?id=612430256

gaperez64 commented 1 year ago

Philipp says this can be set during configuration of spot with --enable-max-accsets=N where N is a multiple of 32

gaperez64 commented 1 year ago

Should now be fixed in https://github.com/gaperez64/acacia-bonsai/blob/3dd17ba2e79e3191592a6293f538fabf2a575ef2/subprojects/packagefiles/spot/meson.build#L20

test pending

gaperez64 commented 1 year ago

This indeed works but now there is an assertion in the forward saturation algorithm which checks that we don't have too many accepting states which causes an error (on some of the same benchmarks). At least we now have an acacia error instead of a spot error, I'll close this for now and open another for the new issue.