synthesis tools that may be useful

[johnyf]

I would like to note some relevant work that could potentially be of use here, either as synthesizers (some from Slugsin), or for bitblasting / higher level constructs:

• omega: includes a bitblaster from first-order temporal logic to Slugsin syntax. It can be used to flatten formulae and then either pass them to slugs, or the 2nd tool listed below.

  omega comes with GR(1) and Rabin(1) solvers in pure Python, so no installation needed, no CUDD. At an intermediate level, it can take input in Slugsin syntax.

• Another solver: that scales to larger problems than slugs (experiments and measurements in the linked repository). It has been based on slugs and gr1c. Written in Python using dd as Cython bindings to CUDD, it runs with Slugsin as input, so it can be called as an external program with the same interface. Like omega, it can run also w/o CUDD, using the pure Python implementation of BDDs in dd. (there are several changes to be released for this solver).
• gr1c: A well-maintained synthesizer written in C using CUDD. It takes input from somewhat different syntax that Slugsin.
• openpromela: An extension of Promela that allows for describing synthesis problems. It flattens open Promela specs to first-order temporal logic, and uses omega from there on. Used to have slugs as backend, now uses omega.
• tulip-control: a project of which the previous are part of, and also a wider-scope toolbox that employs discrete synthesis and polytopic abstraction algorithms to generate controllers for hybrid systems. gr1c is the C-level solver used in tulip, and its fixpoint implementation is faster than slugs (it's current strategy construction algorithm returns an enumerated strategy). tulip has a backend [tulip.dumpsmach] to dump strategies as Python programs.
• Termite's synthesizer (Haskell): I think that this synthesizer corresponds to this paper, and thus includes GR(1), though I have not tried running it.

I am noting the above in hope that they may help as external tools or previous experiments, in case it may avoid duplication of effort.

[leepike]

Thanks a lot for the references! We knew about some, but not others you mentioned, and we've read some of your work.

We're mostly focused on high-level language design rather than the particular GR(1) solver we compile to.

It might be useful to chat offline, if you're willing.

[johnyf]

Yes, sure, my email is jfilippidis@gmail.com.