Designed for users that need particular features and people developing under Storm, this guide will detail how to perform a manual configuration of the build process.
Manually installing dependencies
Storm makes use of CArL for the representation of rationals and rational functions. If you don’t have it installed on your system, our build script will download and configure it automatically for you. However, under certain circumstances, you might want to install CArL yourself. This may for example be advantageous if you need to repeatedly build Storm from scratch or you want to change its source code. Installing CArL is as easy as
$ git clone -b master14 https://github.com/smtrat/carl $ cd carl $ mkdir build $ cd build $ cmake -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON .. $ make lib_carl
Make sure you are using the
master14 branch of CArL as the current master branch uses a newer C++ standard that Storm does not require and therefore does not enable.
Once it is build, it will register itself to cmake so Storm can find your build automatically.
There may be problems with this auto-detection mechanism if you have multiple versions of CArL installed. We strongly recommend to have CArL just once and completely remove the build folder of Storm if one is already present. Rerunning
cmake should then pick up on the “new” version of CArL.
Storm requires Boost to be available in a version that is at least 1.61. On the supported operating systems this can be easily achieved with readily available package managers. If your system does not allow for an easy installation of this Boost version, you might need to build it yourself.
$ wget https://sourceforge.net/projects/boost/files/boost/1.63.0/boost_1_63_0.tar.gz $ tar -xzf boost_1_63_0.tar.gz $ cd boost_1_63_0 $ ./bootstrap.sh $ ./bjam
If you want to install Boost in some other location, you can provide a
--prefix=path/to/installation/prefix to bootstrap.
If you installed your self-built Boost version into standard system locations, it should automatically be found by Storm. However, if it resides in a non-standard location, you need to make Storm aware of it, by passing
-DBOOST_ROOT=/path/to/boost to the
cmake invocation in the configuration step.
There are a number of cmake options that modify how Storm is built. All of them can be set in the configuration step by providing them to
cmake. We don’t detail all options here, but only selected ones.
For developers, we offer the option
STORM_DEVELOPER=ON. This enables
- more cmake output
- more warnings
- debug and trace log levels (they are not always printed and may need to be enabled; in the Storm main binary, this can be done by providing
By default, Storm uses link-time optimization (LTO) to enable even more optimizations that are done at link time. This, however, comes at a penalty for building in terms of both time and memory, as the linking step becomes very resource-intensive. Disabling LTO via
-DSTORM_USE_LTO=OFF avoids this at the price of producing slower binaries.
By default, the binaries will be built specifically for your machine, because this enables a wider range of optimizations to be enabled. If you need your binaries to be portable (in the sense that they could run on another machine that has all required dependencies in their right version), you can set
-DSTORM_PORTABLE=ON at the cost of producing slower binaries.
Some libraries will not be enabled by default as they are not critical (or only for some tasks) and may not be easily available.
Intel Threading Building Blocks (TBB)
Intel’s Threading Building Blocks is a framework for parallelism. If available, Storm can use it to parallelize some operations like (some but not all) matrix-vector multiplications. If TBB is installed, you can enable it via
Gurobi is a commercial high-performance solver for (mixed-integer) linear programs (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). To enable Gurobi, specify the option
-DSTORM_USE_GUROBI=ON and set a hint at where to find Gurobi via
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. To enable MathSAT, you need to set
-DMSAT_ROOT=/path/to/mathsat/root where MathSAT’s root directory is required to contain the
lib folders with the appropriate files (if you download and unpack it, its the directory into which you unpacked it).