The synthesis tool takes as input a TLSF or extended HOA file and outputs REALIZABLE or UNREALIZABLE, and an AIGER model. A brief description is available in the SYNTCOMP report https://arxiv.org/pdf/2206.00251.pdf; the tool re-invents the ideas of Ruediger Ehlers from symbolic bounded synthesis and others.

Dependencies should be placed into folder third_parties. I use the versions below but the tool probably also works with other versions. Make sure to modify CmakeLists.txt to use your paths to these dependencies.

• modified aiger-1.9.4, get it from https://github.com/5nizza/aisy/tree/master/aiger_swig
• cudd-3.0.0
• spot-2.13.1
• spdlog-1.12.0
• pstreams, version 1.0.3
• args: version 6.4.6
• googletest version 1.14.0
  You need to download the source code together with its own CMakeLists.txt.
• It assumes syfco is in your path and callable.

Here is how third_parties look on my machine after downloading/installation of all dependencies:

aiger-1.9.4
args-6.4.6
cudd-3.0.0
googletest-release-1.14.0
pstreams-1.0.3
spdlog-1.12.0
spot-2.13.1
spot-install-prefix

After downloading all the dependencies, building and installing spot, and building cudd, do:

• mkdir build
• cd build
• cmake .. (or cmake .. -DCMAKE_BUILD_TYPE=Debug for version with debug symbols, default is Release)
• make (or make VERBOSE=1 if you want to see compilation flags)

The resulting SDF binaries will be placed in folder build/bin/. You can run them with -help argument.

Note: there are tests, but they require having TLSF-AIGER model checker, and use a path hard-coded in the code. I use IIMC, combine_aiger, and this script. See also tests/tests_synt.cpp for details.

Sometimes SPOT can throw the following error message:

Too many acceptance sets used.  The limit is 32.

To lessen the problem, increase the limit when compiling SPOT (replace with your own paths):

./configure --enable-max-accsets=128 --prefix /home/art/software/sdf-hoa-master/third_parties/spot-install-prefix --disable-devel
make
make install

The above limit of 128 results in much smaller number of errors.

🐾