Build Status

Floras: Flow-Based Reactive Test Synthesis for Autonomous Systems

Detailed installation instruction and the user's guide can be found in the floras documentation.

Requirements

Floras requires Python>=3.10,<3.13 and a C++17-compliant compiler (for example g++>=7.0 or clang++>=5.0). You can check the versions by running python --version and gcc --version.

Pre-installing Graphviz

Please pre-install graphviz and pygraphviz. If you are using a Mac, please install it via brew and pip:

brew install graphviz
pip install pygraphviz

On Ubuntu, please install graphviz using these commands:

sudo apt-get install graphviz graphviz-dev
pip install pygraphviz

Installing Floras

To install floras, please clone the repository:

git clone https://github.com/tulip-control/floras.git

We are using pdm to manage the dependencies.

pip install pdm

Navigate to the repo to install floras and all required dependencies:

cd floras
pdm install

Next, install spot by running:

pdm run python get_spot.py

If you are using conda, instead of the above command, you can install spot directly from conda-forge (this is faster). This does not work on MacOS, please use the above command to build spot in that case.

conda install -c conda-forge spot

If the spot installation does not work, please install it according to the instructions on the spot website.

To enter the virtual environment created by pdm:

$(pdm venv activate)

You can test your installation by running the following command:

pdm install -G tests
pdm run pytest -v tests

If these instructions don't work for you, you can find more information about the installation process and troubleshooting, please visit the floras documentation.

You can also build the documentation by running:

pdm install -G docs
pdm run mkdocs build

The floras repository contains implementations of the algorithms developed in the following paper:

Josefine B. Graebener*, Apurva S. Badithela*, Denizalp Goktas, Wyatt Ubellacker, Eric V. Mazumdar, Aaron D. Ames, and Richard M. Murray. "Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems with Temporal Logic Specifications." ArXiv abs/2404.09888 (2024).