Skip to content

5nizza/party-elli

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

PARTY

Implementation of the SMT based Bounded Synthesis and its friends. The framework contains several tools related to the bounded synthesis:

  • elli.py: Bounded Synthesis Tool
  • query_elli.py: produce SMT queries generated by Elli
  • rally_elli_int.py and rally_elli_bool.py: two Elli variations for SYNTCOMP
  • star.py: Bounded Synthesis for CTL* based on our CAV'17 paper
  • ctl_to_ltl.py: translator of CTL* specifications to LTL (works for synthesis only), based on our SYNT'17 paper
  • kid.py: non-SMT based Bounded Synthesis (also from Schewe/Finkbeiner paper)
  • rally_kid_aiger.py: version of kid for SYNTCOMP that won 2017 competition.
  • ltl_to_aiger.py: converter of the LTL specification into AIGER specification (the same as used by kid)
  • and a few other scripts.

This readme has general information. CAV'17 and SYNT'17 specific information is in CAV-readme and SYNT-readme.

System Requirements

I tested on the following machine, but it likely works with other configurations:

  • Ubuntu 16.04
  • python 3 (version 3.5)
  • Z3 (version 4.5.1: link)
  • SPOT (version 2.5.1: link)
  • python packages: sympy, python-graph-core, python-graph-dot (install them for example using pip3)
  • There are many other dependencies, they will become clear later.

As for SPOT: I use it via python bindings and it is installed system-wide on my machine, but it can also be installed locally (would need some path tweaking).

To Configure

Once you installed all dependencies, configure PARTY. Call ./configure.py and then modify the created file config.py with necessary paths. There are many dependencies.

To Run

This depends on what you want to run.

To run an LTL synthesizer:

./elli.py --help

The input format is Acacia+ and TLSF for most of the tools.

Tests

The test scripts start with test_. Also run nosetests3. All tests should pass.

Notes

  • The encoder for LTL is in synthesis/buchi_cobuchi_encoder.py and synthesis/cobuchi_encoder.py.

Citing

As for other tools, choose the closest, in your opinion, match.

Authors and Contacts

Ayrat Khalimov.\ Also thanks to: Roderick Bloem and Swen Jacobs.\

Please report bugs here or directly gmail me at ayrat.khalimov.

About

SMT based bounded synthesis

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages