Tempest is a shield synthesis tool built as a fork of Storm, a probabilistic model checker. It extends Storm's model checking with the prerequisites for synthesizing shields from probabilistic models.
Tempest inherits Storm's dependencies. Install them by following the official Storm documentation:
https://www.stormchecker.org/documentation/obtain-storm/dependencies.html
The recommended build uses Ninja for faster incremental compilation. If Ninja is not available, plain CMake (Make backend) works as a drop-in alternative.
With Ninja (recommended):
# Clone the repository
git clone <tempest-repo-url>
cd tempest
# Configure
cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -GNinja -DSTORM_BUILD_TESTS=OFF
# Build
ninja -C build -j$(nproc)With CMake / Make:
git clone <tempest-repo-url>
cd tempest
# Configure (omit -GNinja to use the default Make generator)
cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -DSTORM_BUILD_TESTS=OFF
# Build
cmake --build build -j$(nproc)The compiled binary is located at build/bin/storm.
Tempest serves as the computational backend for TempestPy, a Python interface for shield synthesis. See the TempestPy repository for Python bindings and high-level shield synthesis workflows: