diff --git a/doc/source/building_models.rst b/doc/source/building_models.rst index 991b2d9..690e491 100644 --- a/doc/source/building_models.rst +++ b/doc/source/building_models.rst @@ -2,4 +2,43 @@ 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:: + + >>> import stormpy.examples + >>> import stormpy.examples.files + +Storm supports the DRN format. +From this, models can be built directly:: + + >>> path = stormpy.examples.files.drn_ctmc_dft + >>> model = stormpy.build_model_from_drn(path) + >>> print(model.model_type) + ModelType.CTMC + +And the same for parametric models:: + + >>> path = stormpy.examples.files.drn_pdtmc_die + >>> model = stormpy.build_parametric_model_from_drn(path) + >>> print(model.model_type) + ModelType.DTMC + +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. + + >>> 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. diff --git a/examples/building_models/01-building-models.py b/examples/building_models/01-building-models.py new file mode 100644 index 0000000..68ee92d --- /dev/null +++ b/examples/building_models/01-building-models.py @@ -0,0 +1,29 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_building_models(): + path = stormpy.examples.files.drn_ctmc_dft + model = stormpy.build_model_from_drn(path) + print(model.model_type) + print("Number of states: {}".format(model.nr_states)) + + # And the parametric + path = stormpy.examples.files.drn_pdtmc_die + model = stormpy.build_parametric_model_from_drn(path) + print(model.model_type) + print("Number of states: {}".format(model.nr_states)) + + 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) + print("Number of states: {}".format(model.nr_states)) + + + +if __name__ == '__main__': + example_building_models() \ No newline at end of file diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 0dffe66..bfc6f13 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -19,3 +19,9 @@ prism_pdtmc_die = _path("pdtmc", "parametric_die.pm") """Knuth Yao Die -- 2 unfair coins Example""" prism_dtmc_brp = _path("dtmc", "brp-16-2.pm") """Bounded Retransmission Protocol""" +drn_ctmc_dft = _path("ctmc", "dft.drn") +"""DRN format for a CTMC from a DFT""" +drn_pdtmc_die = _path("pdtmc", "die.drn") +"""DRN format for a pDTMC for the KY-Die""" +jani_dtmc_die = _path("dtmc", "die.jani") +"""Jani Version of Knuth Yao Die Example""" \ No newline at end of file diff --git a/lib/stormpy/examples/files/pdtmc/die.drn b/lib/stormpy/examples/files/pdtmc/die.drn new file mode 100644 index 0000000..f1d0e3e --- /dev/null +++ b/lib/stormpy/examples/files/pdtmc/die.drn @@ -0,0 +1,56 @@ +// Exported by storm +// Original model type: DTMC +@type: DTMC +@parameters +p q +@reward_models + +@nr_states +13 +@model +state 0 init + action 0 + 1 : p + 2 : (-1)*p+1 +state 1 + action 0 + 3 : q + 4 : (-1)*q+1 +state 2 + action 0 + 5 : q + 6 : (-1)*q+1 +state 3 + action 0 + 1 : p + 7 : (-1)*p+1 +state 4 + action 0 + 8 : p + 9 : (-1)*p+1 +state 5 + action 0 + 2 : p + 10 : (-1)*p+1 +state 6 + action 0 + 11 : p + 12 : (-1)*p+1 +state 7 + action 0 + 7 : 1 +state 8 + action 0 + 8 : 1 +state 9 + action 0 + 9 : 1 +state 10 + action 0 + 10 : 1 +state 11 + action 0 + 11 : 1 +state 12 + action 0 + 12 : 1