Knor, a symbolic synthesis tool for HOA parity automata.
|eHOA parser||Reading eHOA files, parser based on HOA-TOOLS by Guillermo Perez|
|Conversion to game||Three different methods to convert the parity automaton into a parity game: (1) a naive explicit construction, (2) a BDD-supported explicit construction, (3) a fully symbolic construction|
|Explicit solving||Solving the symbolic parity game explicitly using Oink|
|Symbolic solving||Solving the symbolic parity game symbolically using an internal solver based on Sylvan|
|Bisimulation minimization||Using symbolic bisimulation minimization to reduce the number of states after solving the parity game, similar to SigrefMC|
|Translation to controller||Synthesizing the controller as AIG from the strategy BDD either using ITE or ISOP to compute the logic network, and either a logarithmic or a one-hot encoding of the state|
|Post-synthesis compression||Compressing the AIG after synthesis using ABC|
Knor depends on
bison to generate the eHOA parser, as well as on the
boost libraries for C++.
Compile Knor using the following command line:
mkdir build cd build cmake -DCMAKE_BUILD_TYPE=Release .. make
knor --help to get a list of parameters.
--verbose, Knor will write some information to standard error, such as the time it takes for each step of the process.
If invoked without a filename, Knor will attempt to read an eHOA file from
Knor returns value 10 if the specification is realizable, and value 20 if the specification is unrealizable.
Example command line:
./knor ../examples/amba_decomposed_arbiter_10.tlsf.ehoa --bisim --onehot --compress -a -v > controller.aag
--naivefor the naive explicit splitting procedure, which is not recommended but possible for the purpose of comparing it with the BDD-based procedures.
--explicitfor the BDD-supported explicit parity game construction, which is not recommended but possible for the purpose of comparing it with the fully symbolic construction.
- By default, the fully symbolic construction is used.
- Recommendation: no option, so the fully symbolic construction is used.
Printing the game
--print-gameto print the constructed parity game to standard output, and terminate instead of continuing with solving the parity game.
Solving the game
--symto run the internal symbolic parity game solver. This is the default option; using
- You can select an explicit solver for the parity game solving, e.g.,
--fpjare recommended solvers for most games, but
--rtlare suitable for artificial hard games. See further the documentation of Oink.
--symunless the game is an artificial hard game, then
--realto not do synthesis, only check realizability.
--bisimto minimize the state space using bisimulation minimization prior to synthesis.
--onehotto encode the states using one-hot encoding instead of logarithmic encoding.
--isopto use ZDD covers for the conversion to AIG. By default, a direct conversion based on ITE (Shannon expansion) is used.
--bestto automatically find the smallest result of combinations of
--compressto compress the AIG after construction using ABC.
--bisim --onehotto get a fast result, or
--best --compressto get the best result;
--bisim --onehot --compressgives reasonably good results.
Output of AIG controller
-ato write the result to ascii AIGER format.
-bto write the result to binary AIGER format.
- Recommendation: use
-afor the SYNTCOMP competition and
-bfor smaller output size.
HOA is the Hanoi Omega Automata file format that supports finite automata for languages on infinite words. eHOA is HOA extended to record which atomic propositions are controllable, thus supporting synthesis. See:
- Guillermo A. Pérez (2019). The Extended HOA Format for Synthesis. In CoRR, http://arxiv.org/abs/1912.05793.
For the SYNTCOMP competition, the
prepare_se.sh script prepares a gzipped tarball
knor.tar.gz which can be uploaded to the StarExec environment.
HOA-TOOLS is licensed under GPL v3. Sylvan and Oink are licensed under Apache 2.0. Thus Knor is licensed under GPL v3.