Developer information

The following contains some general guidelines for developers.

Structure

• Storm consists of the core library lib/libstorm resulting from the source code in src/storm.
• Several additional libraries lib/libstorm-xyz provide additional features (parametric models, POMPD, DFT, etc.) and are built from the corresponding code in src/storm-xyz.
• For each library, a corresponding binary /bin/storm-xyz is built from the source in src/storm-xyz-cli.
• Functionality is accompanied by tests (src/test) whenever possible. The complete test suite can be executed by make test and individual tests can be executed via the corresponding binaries bin/test-xyz.
• Storm is heavily templated. In particular, it features the template argument ValueType representing the underlying number type. The most commonly used types are double, storm::RationalNumber and storm::RationalFunction.

The key source directories are:

Directory	Output	Description
src/storm	libstorm	Core model-checking library
src/storm-cli	storm binary	Main command-line interface
src/storm-dft	libstorm-dft	Dynamic Fault Trees
src/storm-pars	libstorm-pars	Parametric models
src/storm-pomdp	libstorm-pomdp	POMDPs
src/storm-gspn	libstorm-gspn	Generalised Stochastic Petri Nets
src/storm-conv	libstorm-conv	Model conversion
src/storm-parsers	(part of libstorm)	PRISM and JANI parsers
src/storm-gamebased-ar		Game-based abstraction refinement
src/storm-permissive		Permissive schedulers
src/test		GTest test suite mirroring the library structure

Each library's public API lives in its api/ subdirectory (e.g., src/storm/api/, src/storm-pars/api/).

Building

Storm uses CMake out-of-source builds. All dependencies must be pre-installed (see the website for the exact set). The CI uses the pre-built Docker image stormchecker/storm-dependencies:latest which comes with most dependencies already installed.

mkdir build && cd build
cmake .. -DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON
make -j$(nproc)        # Build everything
make storm             # Build only the core library
make storm-pars        # Build a specific sub-library
make test              # Run all tests via CTest
make format            # Apply clang-format to all src/

Individual test binaries are placed in build/bin/. Run a specific test with:

./bin/test-storm --gtest_filter='TestSuite.TestName'

Important CMake options:

Option	Default	Meaning
STORM_DEVELOPER	OFF	Enable extra warnings and assertions
STORM_WARNING_AS_ERROR	OFF	Treat warnings as errors (used in CI)
STORM_USE_CLN_EA	OFF	Use CLN instead of GMP for exact arithmetic
STORM_USE_CLN_RF	ON	Use CLN for rational functions
STORM_BUILD_TESTS	ON	Build test binaries
STORM_DISABLE_<DEP>	OFF	Disable optional dependencies (CUDD, GLPK, Z3, …)

Coding conventions

Templates and ValueType

New functionality should typically be templated on ValueType. Add explicit instantiations at the bottom of each .cpp file:

template class MyClass<double>;
template class MyClass<storm::RationalNumber>;
template class MyClass<storm::RationalFunction>;

New numerical code must be tested under both CLN and GMP configurations (STORM_USE_CLN_EA on/off, STORM_USE_CLN_RF on/off) since their arithmetic differs in edge cases.

Infinity

storm::utility::infinity<ValueType>() returns a true infinity only for double. For the exact types it returns the literal 100000000000; it is deprecated and must not be used in new code.

A value that can be infinite is held in storm::utility::ExtendedValueType<ValueType>. This is ValueType itself for types that bring their own infinity (double, reported by NumberTraits<ValueType>::HasInfinity) and storm::utility::ExtendedNumber<ValueType> for the rest. storm::ExtendedRationalNumber and storm::ExtendedRationalFunction are the aliases for RationalNumber and RationalFunction.

Use it at the boundaries of a computation: check results, value vectors handed to a caller, bounds passed around as scalars. Do not use it in hot loops as the extra wrapper can cause unnecessary slowdowns. Often it is possible to filter out any value which would become or are infinte. To detect or set infinities use the following functions:

using Extended = storm::utility::ExtendedValueType<ValueType>;
Extended value = storm::utility::positiveInfinity<ValueType>();  // and negativeInfinity<ValueType>()
storm::utility::isFinite(value);            // false
storm::utility::isInfinity(value);          // true; +infinity only, as for double
storm::utility::isNegativeInfinity(value);  // false
storm::utility::getFinite(value);           // throws unless the value is finite

The arithmetic follows the extended reals. infinity - infinity, 0 * infinity and infinity / infinity throw an InvalidOperationException instead of yielding a NaN, which the exact types have no representation for. A finite ValueType converts implicitly, so mixed expressions need no explicit wrapping.

Converting between the plain and the extended type:

storm::utility::widen(std::move(values));                             // vector<ValueType> -> vector<Extended>
storm::utility::narrowFinite<ValueType>(std::move(values));           // throws on an infinite entry
storm::utility::narrowFinite<ValueType>(std::move(values), fallback); // substitutes it instead
storm::utility::narrow<ValueType>(value);                             // one value, throws if it is infinite

storm::utility::convertNumber takes and returns extended values, so an infinity survives a change of value type.

fromSentinel and toSentinel bridge the parts of Storm that still produce the 100000000000 literal, mainly the DD leaves. They cannot tell that literal apart from a genuine value of the same magnitude, and they are removed together with the sentinel, so do not build on them.

Exception handling

Use STORM_LOG_THROW rather than throwing exceptions directly:

STORM_LOG_THROW(condition, storm::exceptions::InvalidArgumentException, "Descriptive message.");

This throws an InvalidArgumentException if condition is violated. Exception types live in src/storm/exceptions/.

Optional dependencies

Code that requires optional dependencies (CUDD, GLPK, Z3, …) must be guarded with the corresponding preprocessor flag from storm-config.h.in:

#ifdef STORM_HAVE_Z3
  // z3-specific code
#endif

Formatting

• Code should be formatted according to the given rules set by clang-format. Proper formatting can be ensured by executing make format. For more information see PR#175.

Documentation

• We use Doxygen for documentation, see storm-doc. Code blocks should be documented with:

  /*!
   * ... 
   * @param ... 
   * @return ... 
   */
  

• Default values for environments are defined in the constructor of the environment (in the corresponding cpp file).

Includes

• Header files should start with

  #pragma once
  

• Includes should follow the following order:

  #include "storm/header.h"  // If cpp file
  
  #include <external_library1>
  #include <external_library2>
  ...
  
  #include "storm/additional/headerfile1.h"
  #include "storm/additional/headerfile2.h"
  ...
  

  There should only be empty lines between the header file and the external libraries and between the external libraries and the additional header files. Clang-format will then automatically sort the includes in alphabetical order.
• Tests follow the same order as before but typically start by including two helper files:

  #include "storm-config.h"
  #include "test/storm_gtest.h"
  
  #include ...
  

Output

• We provide custom macros for output and logging. The use of std::cout should be avoided and instead, macros such as STORM_LOG_DEBUG, STORM_LOG_INFO or STORM_PRINT_AND_LOG should be used.
• For line breaks, we use '\n' instead of std::endl to avoid unnecessary flushing. See PR 178 for details.

CI / Continuous Integration

Workflows are in .github/workflows/:

Workflow	Trigger	Purpose
buildtest.yml	PR, daily, manual	Full build+test matrix (Debug/Release, GMP/CLN combos, with/without optional deps)
formatcheck.yml	push, PR, manual	Checks src/ with clang-format 20
formatapply.yml	manual	Auto-applies formatting and commits
doxygen.yml	push to master	Publishes API docs
release.yml	tag push	Publishes GitHub releases

buildtest.yml covers multiple configurations including GMP/CLN combinations and a sanitizer build. A CI failure is most commonly caused by a formatting error (fix with make format) or a missing template instantiation for one of the ValueType variants.

Contributing

• Check that all tests run successfully: make test.
• Check that the code is properly formatted: make format. There is also a CI job which can provide automated code formatting.
• New code should be submitted by opening a pull request. Our continuous integration automatically checks that the code in the PR is properly formatted and all tests run successfully.