examples and docu for building models

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.

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()

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"""

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