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

Add compositional solving for realizability #29

Closed ncharl closed 1 year ago

ncharl commented 1 year ago

This PR adds composition to compose multiple formulas when checking realizability. Multiple formulas can be passed with multiple -f, or by putting the formulas on different lines when passing them through stdin. Example: acacia-bonsai -f 'G (!(g1 & g2))' -f 'G (r1 -> (F g1))' -f 'G (r2 -> (F g2))' --ins r1,r2 --outs g1,g2 The number of workers used is the number of hardware threads by default, but can be changed with -j, e.g. -j 1 to use a single worker process. The 11 synthesis tests can also be run with composition using meson test --suite comp.

gaperez64 commented 1 year ago

@ncharl : I cleaned up the test scripts a bit. If we resolve the conflicts above, my next task is to accept this pull request.

ncharl commented 1 year ago

Sounds good! This also (partially) fixes #22, I did not fully check all code but at least some of the hardcoded char types are changed now. Should that issue be closed then, or not yet?