Construction of temporal logic contracts for distributed systems, starting from GR(1) specifications. This implementation is experimental, so expect changes.
The dependencies are listed in the file requirements.txt. Installing a
suitable version of the package dd can be done as follows.
pip uninstall --yes dd
pip install cython
pip download --no-dependencies dd==0.5.1
tar xzf dd-*.tar.gz
cd dd-*/
export CUDD_VERSION=3.0.0
export CUDD_GZ=cudd-${CUDD_VERSION}.tar.gz
curl -sSL https://sourceforge.net/projects/cudd-mirror/files/${CUDD_GZ}/download > ${CUDD_GZ}
tar -xzf ${CUDD_GZ}
python -c 'from download import make_cudd; make_cudd()'
python setup.py install --cuddThese steps will download and build the C library CUDD, and then build and
install dd, including the Cython module dd.cudd. The steps are based on
this .travis.yml.
The repository contract_maker requires dd==0.5.1 (as listed in the file
requirements.txt), and the above steps correspond to that version of dd.
Filippidis I., Murray R.M.
Layering assume-guarantee contracts for hierarchical system design
Proceedings of the IEEE
Volume 106, Number 9, pages 1616--1654, 2018
DOI
Filippidis I., Murray R.M.
Symbolic construction of GR(1) contracts for systems with full information
The 2016 American Control Conference (ACC)
Boston, MA, July 6--8, 2016
pages 782--789, DOI
Filippidis I., Murray R.M.
Symbolic construction of GR(1) contracts for synchronous systems with full information
ArXiv CoRR abs/1508.02705, August, 2015
(technical report with proofs and more details)
BSD-3, see file LICENSE.