diff --git a/doc/source/doc/exploration.rst b/doc/source/doc/exploration.rst index 383d4f2..aac93fd 100644 --- a/doc/source/doc/exploration.rst +++ b/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 `_ +.. seealso:: `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 `_ + + +Often, one may sort the states according to the graph structure. +Storm supports some of these sorting algorithms, e.g., topological sort. + + diff --git a/examples/exploration/03-exploration.py b/examples/exploration/03-exploration.py new file mode 100644 index 0000000..a2a7739 --- /dev/null +++ b/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() \ No newline at end of file