Skip to content

Installation

Tempest is a shield synthesis tool built as a fork of Storm. tempestpy is its Python interface, following the same layered design as stormpy over Storm.

For most users, installing tempestpy is all that is needed: the installation fetches and builds the matching version of Tempest automatically. A separate Tempest build is only required if you want the standalone tempest command-line tool or want to reuse an existing build (see Advanced).

Dependencies

Tempest inherits Storm's build dependencies, and pip does not install them for you. Install them by following the official guide for your operating system:

Storm — required dependencies

You additionally need Python 3.10 or newer with pip.

The Python-level dependencies of tempestpy (Deprecated, loguru) and the build tools (scikit-build-core, pybind11) are installed by pip automatically.

Installing tempestpy

git clone https://github.com/isec-tugraz/tempestpy
cd tempestpy

pip install .

Build time

This also fetches and builds Tempest, which takes a long time. The number of parallel build jobs is taken from the environment variable CMAKE_BUILD_PARALLEL_LEVEL:

CMAKE_BUILD_PARALLEL_LEVEL=4 pip install .

We recommend installing into a virtual environment (python3 -m venv env && source env/bin/activate).

Verify the install:

from tempestpy.shielding import ShieldConfig, ShieldFactory

factory = ShieldFactory("model.prism", property='Pmin=? [F "unsafe"]')
shield = factory.build(ShieldConfig(threshold=0.05))

state = 0
shield.query_mask(state)             # bitmask of the allowed actions
shield.is_action_allowed(state, 1)   # is action 1 allowed in this state?

See the Usage section for an introduction and the API Reference for full module documentation.

Advanced

Using an existing Tempest build

Tempest is pinned in tempestpy's pyproject.toml (STORM_GIT_REPO, STORM_GIT_TAG, STORM_GIT_COMMIT). To skip building Tempest again, build it yourself and pass the build directory:

pip install . \
  --config-settings=cmake.define.STORM_DIR_HINT=/path/to/tempest/build

When an existing build is used, CMake checks it while configuring:

  • Its version must be at least the minimum required by tempestpy; otherwise the configuration fails.
  • If it is not at the pinned commit, was built from a dirty working tree, or its revision is unknown, a warning is printed and the installation continues. Such builds may or may not work.
  • If the library cannot be linked, the build is incomplete or broken and the configuration fails.
  • With --config-settings=cmake.define.STORM_STRICT=ON, the warnings become errors.

Building Tempest standalone

Tempest is built with CMake. Ninja is recommended but optional.

git clone https://github.com/isec-tugraz/tempest
cd tempest
cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -GNinja -DSTORM_BUILD_TESTS=OFF
ninja -C build -j$(nproc)

git clone https://github.com/isec-tugraz/tempest
cd tempest
cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -DSTORM_BUILD_TESTS=OFF
cmake --build build -j$(nproc)

The binary is located at build/bin/tempest; tempest --version shows the revision it was built from. The build/ directory can be passed to tempestpy as STORM_DIR_HINT as described above.

Development (editable) installs

By default, pip builds in a temporary isolated environment whose path changes on every run, so every build recompiles all of tempestpy. For repeated builds, install the build requirements once and disable build isolation:

pip install --group incremental-builds   # needs pip >= 25.1
pip install -e . --no-build-isolation

On older pip versions, use pip install scikit-build-core==0.12.2 pybind11==3.0.4 instead of the first command. The build directory is kept in build/, so later builds only recompile what changed.