Matthias Volk 7 years ago
parent
commit
bbbdbd6c69
  1. 8
      doc/source/getting_started.rst
  2. 2
      examples/06-getting-started.py

8
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:

2
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:

Loading…
Cancel
Save