Interactive version: Binder badge.

Building Models

Background

Storm supports a wide range of formalisms. Stormpy can be used to build models from some of these formalisms. Moreover, during construction, various options can be set. This document yields information about the most important options.

Building different formalisms

We use some standard examples:

[1]:
>>> import stormpy.examples
>>> import stormpy.examples.files

Storm supports the explicit DRN format. From this, models can be built directly:

[2]:
>>> path = stormpy.examples.files.drn_ctmc_dft
>>> model = stormpy.build_model_from_drn(path)
>>> print(model.model_type)
ModelType.CTMC
 WARN (DirectEncodingParser.cpp:119): No. of actions has to be declared. We may continue now, but future versions might not support this.

And the same for parametric models:

[3]:
>>> path = stormpy.examples.files.drn_pdtmc_die
>>> model = stormpy.build_parametric_model_from_drn(path)
>>> print(model.model_type)
ModelType.DTMC
 WARN (DirectEncodingParser.cpp:119): No. of actions has to be declared. We may continue now, but future versions might not support this.

Another option are JANI descriptions. These are another high-level description format. Building models from JANI is done in two steps. First the Jani-description is parsed, and then the model is built from this description:

[4]:
>>> path = stormpy.examples.files.jani_dtmc_die
>>> jani_program, properties = stormpy.parse_jani_model(path)
>>> model = stormpy.build_model(jani_program)
>>> print(model.model_type)
ModelType.DTMC

Notice that parsing JANI files also returns properties. In JANI, properties can be embedded in the model file.