reactive_contracts

Author

Tung Phan-Minh

Description

Automatic synthesis of reactive contracts and implementations

Instructions

1. Requirements: slugs, sympy, numpy, graphviz
2. Update paths in the "run" script
3. cd to source directory
4. Execute ./run N to run a random simulation for N (integer) time steps.
5. Execute python complete_three_islands.py to generate a clean animation from the simulation trace.

License

This is free software released under the terms of the BSD 3-Clause License (http://opensource.org/licenses/BSD-3-Clause). There is no warranty; not even for merchantability or fitness for a particular purpose. Consult LICENSE for copying conditions.

When code is modified or re-distributed, the LICENSE file should accompany the code or any subset of it, however small. As an alternative, the LICENSE text can be copied within files, if so desired.
https://github.com/tungminhphan/reactive_contracts/blob/master/contracts/connexions/assume.png

An example of an automatically generated reactive GR(1) contract