This library provides a simple set of primitives to manipulate Linear Temporal Logic (LTL)-based Assume/Guarantee (A/G)contracts. It allows the definition of new contracts, compute compositions, and check for refinement, consistency, and compatibility.
This library is used as a building block for a larger project: PyCo.
To use this library, you need to have nuXmv 1.1.1 installed on your system.
This project can be installed as a python package, and can be used by importing it in your python source files.
To install the library, go to the root folder of the project and modify setup.cfg to match your configuration. Then, from a command line, run
pip install -e .This last command will install all the required python dependencies.
To make sure the installation has been successful, you can run some tests by running from a command line, always in the project root folder:
python -m pytestAfter executing the last command, you should get a message saying that all the tests were passed.
If you are looking for the code used for our SCP submission, you are looking for the code in this branch (or this pre-release). That branch contains the code used in the experimental section of the paper. That code, however, is somewhat different than the rest of this repo, and some commands referenced in this README might not work. This version requires nuXmv 1.1.1.
Please acknowledge the use of pycolite by citing this Github repository and the article:
Iannopollo A., Tripakis S., Sangiovanni-Vincentelli A. (2017) Constrained Synthesis from Component Libraries. In: Kouchnarenko O., Khosravi R. (eds) Formal Aspects of Component Software. FACS 2016. Lecture Notes in Computer Science, vol 10231. Springer, Cham
or, in Bibtex format:
@Inbook{Iannopollo2017,
author="Iannopollo, Antonio
and Tripakis, Stavros
and Sangiovanni-Vincentelli, Alberto",
editor="Kouchnarenko, Olga
and Khosravi, Ramtin",
title="Constrained Synthesis from Component Libraries",
bookTitle="Formal Aspects of Component Software: 13th International Conference, FACS 2016, Besan{\c{c}}on, France, October 19-21, 2016, Revised Selected Papers",
year="2017",
publisher="Springer International Publishing",
address="Cham",
pages="92--110",
isbn="978-3-319-57666-4",
doi="10.1007/978-3-319-57666-4_7",
url="http://dx.doi.org/10.1007/978-3-319-57666-4_7"
}Alternatively, you can cite this repo directly as:
This project is released under the GPLv3 license. For more information, see LICENSE.