Browse Source

topological sort added to examples

refactoring
Sebastian Junges 5 years ago
parent
commit
2f8c8c6be9
  1. 11
      doc/source/doc/exploration.rst
  2. 27
      examples/exploration/03-exploration.py

11
doc/source/doc/exploration.rst

@ -53,7 +53,7 @@ Storm currently supports deterministic rewards on states or actions. More inform
Reading POMDPs
======================
.. seealso:: `02-exploration.py <https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/01-exploration.py>`_
.. seealso:: `02-exploration.py <https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/02-exploration.py>`_
Internally, POMDPs extend MDPs. Thus, iterating over the MDP is done as before.
@ -96,6 +96,15 @@ Additionally, POMDPs have a set of observations, which are internally just numbe
State 15 has observation id 5
Sorting states
==============
.. seealso:: `03-exploration.py <https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/03-exploration.py>`_
Often, one may sort the states according to the graph structure.
Storm supports some of these sorting algorithms, e.g., topological sort.

27
examples/exploration/03-exploration.py

@ -0,0 +1,27 @@
import stormpy
import stormpy.core
import stormpy.examples
import stormpy.examples.files
def example_exploration_03():
"""
Topological sort
:return:
"""
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
model = stormpy.build_model(prism_program, properties)
sorted = stormpy.topological_sort(model)
print(sorted)
sorted = stormpy.topological_sort(model, forward=False)
print(sorted)
if __name__ == '__main__':
example_exploration_03()
Loading…
Cancel
Save