crome-synthesis

LTL Synthesis Tool

Given an LTL formula the tool: 1) breaks it down in conjunctions of independent formulas, 2) synthesize them into Mealy machines concurrently, 4) runs the Mealy machine in parallel even in presence of multiple fix points.

Documentation available here.

Installation

We use pdm to most of the dependencies, and conda. Make sure they are installed on your system.

To setup the environment, simply run:

make setup

The setup script will:

• Pull all the submodule dependencies
• Install all the dependecies via pdm
• Create a new conda environment and isntall the conda dependencies

NOTE: If it fails for some reason, you'll need to install PDM manually.

You can install it with:

python3 -m pip install --user pipx
pipx install pdm

Now you can try running make setup again, or simply pdm install.

NOTE: Conda for Mac with Apple Silicon

Some of the packages in conda do not support arm64 architecture. To install all the dependencies correctly on a Mac with Apple Silicon, make sure that you are running conda for x86_64 architecture.

You can install miniconda for MacOSX x86_64 by running the following commands

curl -L https://repo.anaconda.com/miniconda/Miniconda3-latest-MacOSX-x86_64.sh > Miniconda3-latest-MacOSX-x86_64.sh

sh Miniforge3-MacOSX-arm64.sh

Activate conda enviornmnet

conda activate ./.venv

NOTE: Working with PEP 582 With PEP 582, dependencies will be installed into pypackages directory under the project root. With PEP 582 enabled globally, you can also use the project interpreter to run scripts directly. Check pdm documentation on PEP 582. To configure VSCode to support PEP 582, open .vscode/settings.json (create one if it does not exist) and add the following entries:

{
  "python.autoComplete.extraPaths": ["__pypackages__/3.10/lib"],
  "python.analysis.extraPaths": ["__pypackages__/3.10/lib"]
}

Usage

Check the examples folder

Run make help to see all the available commands

Docker

You can directly run the project by running the docker image on any platform

docker run -it --platform linux/x86_64 pmallozzi/crome-synthesis:latest

Building the image

To build the image you can run the following command

docker buildx build --platform linux/x86_64 -t [DOCKERUSERNAME]/[PROJECT]:[TAG] --push .

License

MIT

Features and Credits

• Fully typed with annotations and checked with mypy, PEP561 compatible