From 716c6be910fc89532f89106fd2c5ed4cc75b7e8d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 9 Aug 2017 15:55:40 +0200 Subject: [PATCH] extended getting started with the model type --- doc/source/getting_started.rst | 8 +++++++- examples/06-getting-started.py | 2 ++ 2 files changed, 9 insertions(+), 1 deletion(-) 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: