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

Implement compositional algorithm #13

Closed gaperez64 closed 1 year ago

gaperez64 commented 2 years ago

This seems to be one of the last things Acacia+ does support and we don't. Syfco is able to give us a list of formulas, but we have to modify our algorithm to be able to treat each as a subproblem. Subsequently, aggregation has to be implemented. That's in essence a product of subautomata and then re-launching the algorithm on the product --- the starting point is not the all-k vector though, rather the product of the safe regions computed for the subautomata.

gaperez64 commented 1 year ago

@ncharl is on this starting this week

gaperez64 commented 1 year ago

Done, merging the pull request #29 added this functionality