From dd71882ee8c20f150ba886f7eb6d920ea67eb5d9 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Mon, 30 Oct 2017 18:17:52 +0100 Subject: [PATCH 1/2] document basic functionality of ShortestPathsGenerator --- doc/source/index.rst | 1 + doc/source/shortest_paths.rst | 63 +++++++++++++++++++++++++++++++++++ examples/07-shortest-paths.py | 31 +++++++++++++++++ 3 files changed, 95 insertions(+) create mode 100644 doc/source/shortest_paths.rst create mode 100644 examples/07-shortest-paths.py diff --git a/doc/source/index.rst b/doc/source/index.rst index 4adead3..23474df 100644 --- a/doc/source/index.rst +++ b/doc/source/index.rst @@ -16,6 +16,7 @@ Stormpy is a set of python bindings for the probabilistic model checker `Storm < installation getting_started + shortest_paths contributors diff --git a/doc/source/shortest_paths.rst b/doc/source/shortest_paths.rst new file mode 100644 index 0000000..4e3f43d --- /dev/null +++ b/doc/source/shortest_paths.rst @@ -0,0 +1,63 @@ +*************************** +Working with Shortest Paths +*************************** + +Storm can enumerate the most probable paths of a model, leading from the initial state to a defined set of target states, which we refer to as shortest paths. +In particular, the model states visited along those paths are available as sets and can be accumulated, yielding a *sub-model*. + +Background +========== + +The underlying implementation uses the *recursive enumeration algorithm* [JM1999]_, substituting distance for probability – which is why we refer to the most probable paths as the *shortest* paths. + +This algorithm computes the shortest paths recursively and in order, i.e., to find the 7th shortest path, the 1st through 6th shortest paths are computed as precursors. The next (i.e., 8th shortest) path can then be computed efficiently. + +It is crucial to note that *any* path is eligible, including those that (repeatedly) traverse loops (i.e., *non-simple* paths). This is a common case in practice: Often a large number of similar paths that differ only in the order and number of loop traversals occur successively in the sequence of shortest paths. (For applications that are only interested in simple paths, this is rather unfortunate.) + + +Examining Shortest Paths +======================== + +.. seealso:: `07-shortest-paths.py `_ + +As in :doc:`getting_started`, we import some required modules and build a model from the example files:: + + >>> import stormpy.examples + >>> import stormpy.examples.files + >>> path = stormpy.examples.files.prism_dtmc_die + >>> prism_program = stormpy.parse_prism_program(path) + >>> model = stormpy.build_model(prism_program) + + +We also import the `ShortestPathsGenerator`:: + + >>> from stormpy.utility import ShortestPathsGenerator + +and choose a target state (by its ID) to which we want to compute the shortest paths:: + + >>> state_id = 8 + +It is also possible to specify a set of target states (as a list, e.g., ``[8, 10, 11]``) or a label in the model if applicable (e.g., ``"observe0Greater1"``). +For simplicity, we will stick to using a single state for now. + +We initialize a `ShortestPathsGenerator` instance:: + + >>> spg = ShortestPathsGenerator(model, state_id) + +Now we can query the `k`-shortest path by index. Note that 1-based indices are used, so that the 3rd shortest path indeed corresponds to index ``k=3``. +Let us inspect the first three shortest paths:: + + >>> for k in range(1, 4): + ... path = spg.get_path_as_list(k) + ... distance = spg.get_distance(k) + ... print("{}-shortest path to state #{}: {}, with distance {}".format(k, state_id, path, distance)) + 1-shortest path to state #8: [8, 4, 1, 0], with distance 0.125 + 2-shortest path to state #8: [8, 4, 1, 3, 1, 0], with distance 0.03125 + 3-shortest path to state #8: [8, 4, 1, 3, 1, 3, 1, 0], with distance 0.0078125 + +As you can see, the distance (i.e., probability of the path) is also available. +Note that the paths are displayed as a backward-traversal from the target to the initial state. + +.. Yeah, sorry about that. Would be more user-friendly to (un-)reverse it + +.. [JM1999] Víctor M. Jiménez, Andrés Marzal. `Computing the K Shortest Paths: A New Algorithm and an Experimental Comparison `_. International Workshop on Algorithm Engineering, 1999 diff --git a/examples/07-shortest-paths.py b/examples/07-shortest-paths.py new file mode 100644 index 0000000..ecacd1f --- /dev/null +++ b/examples/07-shortest-paths.py @@ -0,0 +1,31 @@ +# TODO: it is not obvious which of these imports are needed under what circumstances +# note that this script runs fine without stormpy[.core]! +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + +from stormpy.utility import ShortestPathsGenerator + + +def example_shortest_paths(): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + model = stormpy.build_model(prism_program) + + state_id = 8 + spg = ShortestPathsGenerator(model, state_id) + + # TODO: it's unintuitive to return the paths reversed, change that + # the reason for being reversed in the first place is that the algorithm traverses them in that order + print("Note: Paths are traversed in reverse (from target back to the initial state).") + + for k in range(1, 4): + path = spg.get_path_as_list(k) + distance = spg.get_distance(k) + print("{}-shortest path to state #{}: {}, with distance {}".format(k, state_id, path, distance)) + + +if __name__ == '__main__': + example_shortest_paths() From 6f64af5acfd380111ef12eb32cb6b8884398dd66 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 7 Nov 2017 11:09:12 +0100 Subject: [PATCH 2/2] some minor changes to the documentation tree --- doc/source/advanced_topics.rst | 13 +++++++++++++ doc/source/building_models.rst | 5 +++++ doc/source/index.rst | 2 +- doc/source/reward_models.rst | 7 +++++++ 4 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 doc/source/advanced_topics.rst create mode 100644 doc/source/building_models.rst create mode 100644 doc/source/reward_models.rst diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst new file mode 100644 index 0000000..124c702 --- /dev/null +++ b/doc/source/advanced_topics.rst @@ -0,0 +1,13 @@ +***************** +Advanced Examples +***************** + +This guide is a collection of examples meant to bridge the gap between the getting started guide and the API. + +.. toctree:: + :maxdepth: 2 + :caption: Contents: + + building_models + reward_models + shortest_paths \ No newline at end of file diff --git a/doc/source/building_models.rst b/doc/source/building_models.rst new file mode 100644 index 0000000..991b2d9 --- /dev/null +++ b/doc/source/building_models.rst @@ -0,0 +1,5 @@ +*************** +Building Models +*************** + + diff --git a/doc/source/index.rst b/doc/source/index.rst index 23474df..76040e8 100644 --- a/doc/source/index.rst +++ b/doc/source/index.rst @@ -16,7 +16,7 @@ Stormpy is a set of python bindings for the probabilistic model checker `Storm < installation getting_started - shortest_paths + advanced_topics contributors diff --git a/doc/source/reward_models.rst b/doc/source/reward_models.rst new file mode 100644 index 0000000..2bf2619 --- /dev/null +++ b/doc/source/reward_models.rst @@ -0,0 +1,7 @@ +************** +Reward Models +************** + +Exploring reward models +------------------------ +