Storm

Installing Dependencies

Table of contents

Storm depends on several other libraries. Partly, they are packed with Storm. This page describes dependencies which are assumed to be present on the target system. We both give a general list, as well as operating system specific hints how to install them.

Compiler

For the compilation step, a C++20-compliant compiler is required. Storm is known to work with GCC, Clang, and AppleClang.

General Dependencies

In the following, we provide an overview over the required and recommended dependencies of Storm. Required dependencies are absolutely essential for Storm to be compiled and must be installed. Recommended dependencies are optional, but not installing them may severely limit the offered functionality.

Required:

Recommended:

OS specific preparations

We collected some platform specific hints to ease the installation of Storm on the supported operating systems. Since Storm has some optional dependencies that enhance it’s functionality, and some dependencies that are strictly required, we show how to install both the required and recommended dependencies. The installation instructions of the recommended dependencies already include the required dependencies.

We strongly suggest to install the recommended dependencies to obtain the full functionality of Storm.

macOS

Make sure that you use a recent macOS version. You need to download and install Xcode or its command line tools (CLT) to have the suitable tools needed for compilation. For more details, we refer to this tutorial.

Furthermore, we recommend the usage of Homebrew to install the missing packages.

For troubleshooting building on ARM-based Apple Silicon CPUs and for building using x86 emulations, please refer to this page.

Debian and Ubuntu

We currently support Debian from version 12 and Ubuntu from version 24.04.

List of dependencies

Storm supports a range of additional libraries for specific tasks in the back-end such as solvers. We provide a list of supported libraries below. By default, Storm searches for these libraries automatically and uses them if found. If a system library was not found, you can provide the location of specific library X via the additional CMake argument -DX_ROOT=/path/to/x during the configuration process. A library can be explicitly disabled by providing the CMake argument -DSTORM_DISABLE_X.

Carl

CArL is a computer arithmetic and logic library. It is heavily intertwined with Storm and provides the support for symbolic computations and a wrapper for exact arithmetic. Carl is automatically downloaded and installed during the Storm build process. You can configure the repository and git tag where carl is obtained by the CMake arguments -DSTORM_CARL_GIT_REPO and -DSTORM_CARL_GIT_TAG. To use an existing local copy of the carl repository, you can provide the location via -DFETCHCONTENT_SOURCE_DIR_CARL=/path/to/carl/repo during CMake configuration. Note that Storm only uses the sources from this directory, but still builds the carl library. The use of Carl cannot be disabled.

GLPK

GLPK is a solver for linear programming (LP), mixed integer programming (MIP) and related problems. The location of GLPK can be given via -DGLPK_ROOT=/path/to/glpk.

GMM

gmm++ is a library for sparse linear algebra operations. Storm automatically ships with gmm++.

Gurobi

Gurobi is a commercial high-performance solver for (mixed-integer) linear programming (and similar problems). A free license can be obtained for academic purposes. Storm provides an implementation of its (MI)LP solver interface that uses Gurobi (provided Storm has been compiled with support for it). The location of Gurobi can be given via -DGUROBI_ROOT=/path/to/gurobi.

MathSat

MathSAT is a high-performance SMT solver that can be used as an alternative to Z3. In contrast to Z3, it provides native support for AllSat (enumeration of all satisfying models of a formula) and may generate Craig interpolants. This makes MathSAT particularly useful in the abstraction-refinement engine. The location of MathSAT can be given via -DMATHSAT_ROOT=/path/to/mathsat/root where MathSAT’s root directory is required to contain the include and lib folders with the appropriate files (if you download and unpack it, its the directory into which you unpacked it).

Soplex

SoPlex is a solver for linear programs. The location of Soplex can be given via -DSOPLEX_ROOT=/path/to/soplex.

Spot

Spot is a library for LTL. Storm depends on Spot for model checking LTL queries. To use a system version of Spot, set the path in -DSPOT_ROOT=/path/to/spot. Alternatively, you can force Storm to automatically download and build Spot by giving the CMake option -DSTORM_SPOT_FORCE_SHIPPED=ON.

Xerces

Xerces is a library for XML parsing. It is used in Storm to parse GSPN models in the storm-gspn library. The location of Xerces can be given via -DXERCES_ROOT=/path/to/xerces.

Z3

Z3 is a SMT solving. Storm makes heavy use of Z3 for parsing and evaluating expressing. Without Z3, Storm has very limited functionality. The location of Z3 can be given via -DZ3_ROOT=/path/to/z3.

Additional libraries

Storms uses the following additional libraries for some of its functionality.

Acknowledgements

A large number of dependencies contribute to the capabilities of Storm. We would like to thank the developers of all previously mentioned tools.