diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index c38afd7..01598ff 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -169,7 +169,13 @@ One powerful part of the storm model checker is to quickly create the Markov cha >>> prism_program = stormpy.parse_prism_program(path) >>> model = stormpy.build_model(prism_program) -In this example, we will exploit this, and explore the underlying matrix of the model. +In this example, we will exploit this, and explore the underlying Markov chain of the model. +The most basic question might be what the type of the constructed model is:: + + >>> print(model.model_type) + ModelType.DTMC + +We can also directly explore the underlying matrix. Notice that this code can be applied to both deterministic and non-deterministic models:: >>> for state in model.states: diff --git a/examples/06-getting-started.py b/examples/06-getting-started.py index 66481bb..d656d7a 100644 --- a/examples/06-getting-started.py +++ b/examples/06-getting-started.py @@ -12,6 +12,8 @@ def example_getting_started_06(): properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) model = stormpy.build_model(prism_program, properties) + print(model.model_type) + for state in model.states: for action in state.actions: for transition in action.transitions: