search

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

Inconsistent answers when using incremental K values #18

Closed gaperez64 closed 3 months ago

gaperez64 commented 1 year ago

./src/acacia-bonsai -f "G (a && b)" --ins a --outs b -K 150 This gives UNREALIZABLE as would be expected, but then: ./src/acacia-bonsai -f "G (a && b)" --ins a --outs b -M 10 -I 10 -K 200 This gives REALIZABLE and only switches to UNREALIZABLE when the minimum value -M is large enough to find that it is UNREALIZABLE (129 in this case) And actually, when specifying only a single value with -K, any value until 127 gives UNKNOWN, any value starting from 129 gives UNREALIZABLE, and 128.. says REALIZABLE. ./src/acacia-bonsai -f "G (a && b)" --ins a --outs b -K 128 gives REALIZABLE This is all especially strange considering with -M 10 and -I 10, I would think it tries 10, 20, 30, ... so it wouldn't even try 128.

gaperez64 commented 1 year ago

This was found by @ncharl

gaperez64 commented 1 year ago

After discussing with @michaelcadilhac, 128 is clearly too high a value and AB should have just complained about that instead of trying to continue and (almost surely) end up with an overflow somewhere. This should still be fixed, but it's probably not a bug.