Developer information

The following contains some general guidelines for developers.

Development setup

For development, install stormpy together with all optional features and all tools for testing, formatting and building the documentation:

pip install -v .[dev]

The extra dev installs:

The noxfile.py provides sessions for common tasks (nox -l lists all of them):

  • nox -s format formats all Python code, C++ code and the code in the documentation.

  • nox -s tests runs all tests. Additional arguments are forwarded to pytest, for example nox -s tests -- tests/core.

  • nox -s check checks the formatting of the documentation, executes the documentation and runs all tests.

  • nox -s doc builds the documentation.

All sessions run in the current Python environment, so stormpy and the dev dependencies must be installed there.

Structure

  • C++ bindings are defined in src.

  • Python methods are defined in lib/stormpy.

  • Tests are given in tests.

  • The Sphinx documentation can be found in doc/source.

Info packages

stormpy.info provides functions with information about Storm and the build; stormpy.developer.info contains the raw StormVersion.

Logic packages

stormpy.logic selects the public objects: properties, formulas, comparison types and optimization directions. stormpy.developer.logic contains the raw native module.

Storage packages

The public objects are selected explicitly in stormpy.models (models, components, rewards, state/action views, labels, valuations, schedulers and memory structures), stormpy.datastructures (bit vectors, matrices, distributions and JSON containers), stormpy.expressions (expressions and variables) and stormpy.io (format-specific descriptions, parsing, exporting and their options). stormpy.developer.storage contains the raw native module and template families such as advanced DD and transformation helpers.

Analysis, plotting and developer utilities

stormpy.plotting provides Pareto-curve plotting helpers and requires the plot extra. Shortest paths, graph decompositions and numerical analyses belong to stormpy.analysis. Model-checking results, bounds and aggregation belong to stormpy.results. Model transformations and their options, policies and mapping results belong to stormpy.transformations. Logging and timeouts are available through stormpy.developer. stormpy.developer.utility contains the raw native module, including the Kwek-Mehlhorn algorithm.

Public API and developer bindings

Each library xy of Storm (e.g. core or DFTs) is split into two layers:

  • stormpy.xy.developer contains the raw pybind11 bindings defined in src/xy. They mirror the C++ API of Storm (naming, arguments and default values).

  • stormpy.xy is the public API built on top of stormpy.xy.developer. Each public object supports a documented user task and has a supported interface, including the objects returned from public methods. The public names are declared in __all__ of the module. Only names listed in __all__ are part of the public API and appear in the API documentation. Python conveniences are implemented in this public layer. Public template families use publish_as and share their native classes with the developer families.

Extending the public API

When adding a name to the public API, import it in __init__.py, add it to __all__ and document it with a docstring. Functions must document each parameter with :param <name>:.

Number types

The Python types matching Storm’s C++ value types (e.g. Rational for storm::RationalNumber) are defined in stormpy.numbers. They are generated by CMake (cmake/numbers_config.py.in) depending on the configuration of Storm. The bindings of the carl library (pycarl, src/pycarl/) form the developer layer stormpy.numbers.developer.

Templated classes and functions

C++ templates are bound once per instantiation and grouped in Python into a subscriptable family, e.g. stormpy.results.ExplicitQuantitativeCheckResult[float].

  • Classes are bound with bindTemplateClass (src/template_binding.h) and exposed as _TemplateClass (lib/stormpy/_template.py).

  • Functions whose template parameters cannot be deduced from their arguments (e.g. because the value type only occurs in the return type) are bound with bindTemplateFunction and exposed as _TemplateFunction, e.g. stormpy.developer.build_sparse_model[stormpy.Rational](program, formulas). Do not encode the template parameters in the function name.

  • Public Python functions with a template parameter, e.g. stormpy.build_model[stormpy.Rational](program), are defined with the decorator _template_function (lib/stormpy/_template.py). The decorated function takes the template parameters as leading arguments, and one instantiation is created per supported parameter.

The families of the bindings are defined in the __init__.py of the developer module. A deduction guide (e.g. _deduce_default(float)) determines the instantiation used when the family is called without subscript.

Tests of the public APIs

The generic checks of all public APIs are given in tests/test_public_apis.py. For each registered module, they check that

  • all names in __all__ exist and are unique,

  • __all__ contains no private names (starting with _) and no modules (such as developer),

  • every public function has a docstring documenting all of its parameters,

  • every public class (and every instantiation of a templated class) has a docstring.

The modules are registered in _PUBLIC_MODULES at the top of the file. When converting a further library into the public/developer structure, add one entry consisting of

  • the module name, e.g. "stormpy.pars",

  • whether the module is available in the current build, e.g. has_pars from tests/configurations.py,

  • a predicate for names which are documented in other modules and are therefore skipped by the docstring checks.

Tests which are specific to one module, e.g. names which were removed from the public API or the availability of developer bindings, belong to the tests of that module, e.g. tests/core/test_api.py.

Coding conventions

Formatting

  • Code should be formatted according to the given rules set by black (for Python). Proper formatting can be ensured by executing black .. The CI automatically checks for proper formatting as well.

Enum naming

  • Enum values exposed to Python via py::native_enum must use UPPER_CASE_WITH_UNDERSCORES in the string name in .value("NAME", ...).

Dependencies

  • The bindings are created with pybind11. The pybind11 version is set in pyproject.toml through requires, and in CMakeLists.txt through find_package(pybind11 ...).

  • The minimal Python version is set in pyproject.toml through requires-python, and in CMakeLists.txt through find_package(Python ...).

  • The Storm version is set in pyproject.toml through STORM_GIT_TAG, and in CMakeLists.txt through STORM_MIN_VERSION. If stormpy development requires changes from Storm master which are not yet released, STORM_MIN_VERSION can be set to a development version x.y.z.N. STORM_GIT_TAG stays at the latest Storm release. Building stormpy from source by fetching Storm requires --config-settings=cmake.define.STORM_GIT_TAG=master. The CI uses Storm master by default, or the stable branch for specific configurations.

  • The optional Python dependencies are defined in pyproject.toml in [project.optional-dependencies].