From 2f8c8c6be9e9c0607ab595c71980aa75748d492d Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 2 Dec 2019 17:31:51 +0100
Subject: [PATCH] topological sort added to examples

---
 doc/source/doc/exploration.rst         | 11 ++++++++++-
 examples/exploration/03-exploration.py | 27 ++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 examples/exploration/03-exploration.py

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 <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.
+
+
 
 
 
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