The following contains some general guidelines for developers.
- Storm consists of the core library
lib/libstormresulting from the source code insrc/storm. - Several additional libraries
lib/libstorm-xyzprovide additional features (parametric models, POMPD, DFT, etc.) and are built from the corresponding code insrc/storm-xyz. - For each library, a corresponding binary
/bin/storm-xyzis built from the source insrc/storm-xyz-cli. - Functionality is accompanied by tests (
src/test) whenever possible. The complete test suite can be executed bymake testand individual tests can be executed via the corresponding binariesbin/test-xyz. - Storm is heavily templated.
In particular, it features the template argument
ValueTyperepresenting the underlying number type. The most commonly used types aredouble,storm::RationalNumberandstorm::RationalFunction.
- 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.
- We use Doxygen for documentation, see storm-doc.
Code blocks should be documented with:
/*! * ... * @param ... * @return ... */
- Header files should start with
#pragma once - Includes should follow the following order:
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.
#include "storm/header.h" // If cpp file #include <external_library1> #include <external_library2> ... #include "storm/additional/headerfile1.h" #include "storm/additional/headerfile2.h" ... - 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 ...
- We provide custom macros for output and logging.
The use of
std::coutshould be avoided and instead, macros such asSTORM_LOG_DEBUG,STORM_LOG_INFOorSTORM_PRINT_AND_LOGshould be used. - For line breaks, we use
'\n'instead ofstd::endlto avoid unnecessary flushing. See PR 178 for details.
- 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.