From 87e8af98528ecaba2fbf5976be16db8436f86959 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Tue, 20 Dec 2016 17:00:13 +0100 Subject: [PATCH] moved ksp stuff to right location fix include --- src/{ => storm}/utility/shortestPaths.cpp | 0 src/{ => storm}/utility/shortestPaths.h | 4 +- .../test}/utility/KSPTest.cpp | 12 +- src/utility/shortestPaths.md | 114 ------------------ 4 files changed, 8 insertions(+), 122 deletions(-) rename src/{ => storm}/utility/shortestPaths.cpp (100%) rename src/{ => storm}/utility/shortestPaths.h (99%) rename {test/functional => src/test}/utility/KSPTest.cpp (94%) delete mode 100644 src/utility/shortestPaths.md diff --git a/src/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp similarity index 100% rename from src/utility/shortestPaths.cpp rename to src/storm/utility/shortestPaths.cpp diff --git a/src/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h similarity index 99% rename from src/utility/shortestPaths.h rename to src/storm/utility/shortestPaths.h index c34439401..e7cb38df6 100644 --- a/src/utility/shortestPaths.h +++ b/src/storm/utility/shortestPaths.h @@ -4,8 +4,8 @@ #include #include #include -#include "src/models/sparse/Model.h" -#include "src/storage/sparse/StateType.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/sparse/StateType.h" #include "constants.h" // NOTE: You'll (eventually) find the usual API documentation below; diff --git a/test/functional/utility/KSPTest.cpp b/src/test/utility/KSPTest.cpp similarity index 94% rename from test/functional/utility/KSPTest.cpp rename to src/test/utility/KSPTest.cpp index e3c127f4b..3d28ccae6 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/src/test/utility/KSPTest.cpp @@ -1,12 +1,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/builder/ExplicitModelBuilder.h" -#include "src/models/sparse/Dtmc.h" -#include "src/parser/PrismParser.h" -#include "src/storage/SymbolicModelDescription.h" -#include "src/utility/graph.h" -#include "src/utility/shortestPaths.cpp" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/parser/PrismParser.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/utility/graph.h" +#include "storm/utility/shortestPaths.cpp" // NOTE: The KSPs / distances of these tests were generated by the // KSP-Generator itself and checked for gross implausibility, but no diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md deleted file mode 100644 index 13dc96376..000000000 --- a/src/utility/shortestPaths.md +++ /dev/null @@ -1,114 +0,0 @@ -# k-shortest Path Generator -[This is a collection of random notes for now, to help me remember -the design decisions and the rationale behind them.] - -## Differences from REA algorithm -This class closely follows the Jimenez-Marzal REA algorithm. -However, there are some notable deviations in the way targets and shortest -paths are defined. - -### Target groups -Firstly, instead of a single target state, a group of target states is -considered. It is clear that this can achieved by removing all outgoing -transitions (other than self-loops, but this is moot due to not allowing -non-minimal paths -- see below) and instead introducing edges to a new sink -state that serves as a meta-target. - - - -I chose to implement this by modifying the precomputation results, meaning -that they are only valid for a fixed group of target states. Thus, the -target group is required in the constructor. (It would have been possible to -allow for interchangeable target groups, but I don't anticipate that use -case.) - -#### Special case: Using Matrix/Vector from SamplingModel - -The class has been updated to support the matrix/vector that `SamplingModel` -generates (as an instance of a PDTMC) as input. This is in fact closely -related to the target groups, since it works as follows: - -The input is a (sub-stochastic) transition matrix of the maybe-states (only!) -and a vector (again over the maybe-states) with the probabilities to an -implied target state. - -This naturally corresponds to having a meta-target, except the probability -of its incoming edges range over $(0,1]$ rather than being $1$. -Thus, applying the term "target group" to the set of states with non-zero -transitions to the meta-target is now misleading[^1], but nevertheless it -should work exactly the same. [Right?] - -In terms of implementation, in `getEdgeDistance` as well as in the loop of -the Dijkstra, the "virtual" edges to the meta-target were checked for and -set to probability $1$; this must now be changed to use the probability as -indicated in the `targetProbVector` if this input format is used. - -### Minimality of paths -Secondly, we define shortest paths as "minimal" shortest paths in the -following sense: The path may not visit any target state except at the -end. As a corollary, no KSP (to a target node) may be a prefix of another. -This in particular forbids shortest path progressions such as these: - - 1-SP: 1 2 3 - 2-SP: 1 2 3 3 - 3-SP: 1 2 3 3 3 - ... - -This is a common feature if the target state is a sink; but we are not -interested in such paths. - -(In fact, ideally we'd like to see paths whose node-intersection with all -shorter paths is non-empty [^2] (which is an even stronger statement than -loop-free-ness of paths), because we want to take a union of those node -sets. But that's a different matter.) - - -## Data structures, in particular: Path representation - -The implicit shortest path representation that J&M describe in the paper -is used, except that indices rather than back-pointers are stored to -refer to the tail of the path. -[Maybe pointers would be faster? STL vector access via index should be -pretty fast too, though, and less error-prone.] - -A bit more detail (recap of the paper): -All shortest paths (from `s` to `t`) can be described as some k-shortest -path to some node `u` plus an edge to `t`: - - s ~~k-shortest path~~> u --> t - -Further, the shortest paths to some node are always computed in order and -without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed -before the 4-SP. Thus, we store the SPs in a linked list for each node, -with the k-th entry[^3] being the k-th SP to that node. - -Thus for an SP as shown above we simply store the predecessor node (`u`) -and the `k`, which allows us to look up the tail of the SP. -By recursively looking up the tail (until it's empty), we reconstruct -the entire path back-to-front. - -[^1]: I suppose the correct term would now be "meta-target predecessors". - In fact, I will rename all occurences of `target` in the source to - `metaTargetPredecessors` – clumsy but accurate. -[^2]: (2016-08-20:) Is this correct? Didn't I mean that the path should - contain new nodes, i.e., non-emptiness of - ((nodes in path) set-minus (union(nodes in shorter paths)))? - Yeah, I'm pretty sure that's what I meant. -[^3]: Which due to 0-based indexing has index `k-1`, of course! Damn it.