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

Antichain size is not correct #20

Closed gaperez64 closed 1 year ago

gaperez64 commented 1 year ago

An antichain of size 5 reports a size of six. This bug was found by @ncharl

Reproduce by running:

acacia-bonsai -f "(G (i1 -> (F o1))) && (G (i1 -> (F o2))) && (G (!(o1 && o2))) && (G (o1 -> !(X o2)))" --ins i1 --outs o1,o2 -v -v -v
michaelcadilhac commented 1 year ago

I suspect this is because

https://github.com/gaperez64/acacia-bonsai/blob/5ffd8f994d2348759b721f64d9fa3c9b5b8a8607/src/downsets/vector_backed_bin.hh#L83

… does not decrease size. (Maybe see also other downset implementations with the same bug.)

gaperez64 commented 1 year ago

Yes, that was the problem. I fixed it in that downset implementation along with one other which also used _size instead of the size of some container. See commit 41c8db783d9d39fb73952430ecbc082f6df6ce18 (and subsequent commits where the same is done in a different fashion)