Browse Source

kSP: a few more comments

tempestpy_adaptions
tomjanson 8 years ago
committed by Tom Janson
parent
commit
83445f67c3
  1. 29
      src/utility/shortestPaths.cpp
  2. 10
      src/utility/shortestPaths.md

29
src/utility/shortestPaths.cpp

@ -1,8 +1,16 @@
#include <queue> #include <queue>
#include <set> #include <set>
#include <string>
#include "macros.h"
#include "shortestPaths.h" #include "shortestPaths.h"
#include "graph.h" #include "graph.h"
// FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required!
// Accessing zero should trigger a warning!
// (Also, did I document this? I think so, somewhere. I went with k>=1 because
// that's what the KSP paper used, but in retrospect k>=0 seems more intuitive ...)
namespace storm { namespace storm {
namespace utility { namespace utility {
namespace ksp { namespace ksp {
@ -249,9 +257,13 @@ namespace storm {
template <typename T> template <typename T>
void ShortestPathsGenerator<T>::computeNextPath(state_t node, unsigned long k) { void ShortestPathsGenerator<T>::computeNextPath(state_t node, unsigned long k) {
assert(k >= 2); // Dijkstra is used for k=1
assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist
// TODO: I could extract the candidate generation to make this function more succinct
if (k == 2) { if (k == 2) {
// Step B.1 in J&M paper
Path<T> shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-| Path<T> shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-|
for (state_t predecessor : graphPredecessors[node]) { for (state_t predecessor : graphPredecessors[node]) {
@ -271,7 +283,9 @@ namespace storm {
} }
} }
if (k > 2 || !isInitialState(node)) {
if (not (k == 2 && isInitialState(node))) {
// Steps B.2-5 in J&M paper
// the (k-1)th shortest path (i.e., one better than the one we want to compute) // the (k-1)th shortest path (i.e., one better than the one we want to compute)
Path<T> previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN Path<T> previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN
@ -297,9 +311,10 @@ namespace storm {
}; };
candidatePaths[node].insert(pathToPredecessorPlusEdge); candidatePaths[node].insert(pathToPredecessorPlusEdge);
} }
// else there was no path; TODO: does this need handling?
// else there was no path; TODO: does this need handling? -- yes, but not here (because the step B.1 may have added candidates)
} }
// Step B.6 in J&M paper
if (!candidatePaths[node].empty()) { if (!candidatePaths[node].empty()) {
Path<T> minDistanceCandidate = *(candidatePaths[node].begin()); Path<T> minDistanceCandidate = *(candidatePaths[node].begin());
for (auto path : candidatePaths[node]) { for (auto path : candidatePaths[node]) {
@ -310,6 +325,9 @@ namespace storm {
candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate)); candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate));
kShortestPaths[node].push_back(minDistanceCandidate); kShortestPaths[node].push_back(minDistanceCandidate);
} else {
// TODO: kSP does not exist. this is handled later, but it would be nice to catch it as early as possble, wouldn't it?
STORM_LOG_TRACE("KSP: no candidates, this will trigger nonexisting ksp after exiting these recursions. TODO: handle here");
} }
} }
@ -320,9 +338,10 @@ namespace storm {
for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) {
computeNextPath(metaTarget, nextK); computeNextPath(metaTarget, nextK);
if (kShortestPaths[metaTarget].size() < nextK) { if (kShortestPaths[metaTarget].size() < nextK) {
//std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl;
//printKShortestPath(metaTarget, nextK - 1);
//std::cout << "---------" << "No other path exists!" << std::endl;
unsigned long lastExistingK = nextK - 1;
STORM_LOG_DEBUG("KSP throws (as expected) due to nonexistence -- maybe this is unhandled and causes the Python interface to segfault?");
STORM_LOG_DEBUG("last existing k-SP has k=" + std::to_string(lastExistingK));
STORM_LOG_DEBUG("maybe this is unhandled and causes the Python interface to segfault?");
throw std::invalid_argument("k-SP does not exist for k=" + std::to_string(k)); throw std::invalid_argument("k-SP does not exist for k=" + std::to_string(k));
} }
} }

10
src/utility/shortestPaths.md

@ -75,7 +75,7 @@ This is a common feature if the target state is a sink; but we are not
interested in such paths. interested in such paths.
(In fact, ideally we'd like to see paths whose node-intersection with all (In fact, ideally we'd like to see paths whose node-intersection with all
shorter paths is non-empty (which is an even stronger statement than
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 loop-free-ness of paths), because we want to take a union of those node
sets. But that's a different matter.) sets. But that's a different matter.)
@ -97,7 +97,7 @@ path to some node `u` plus an edge to `t`:
Further, the shortest paths to some node are always computed in order and 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 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, before the 4-SP. Thus, we store the SPs in a linked list for each node,
with the k-th entry[^2] being the k-th SP to that 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`) 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. and the `k`, which allows us to look up the tail of the SP.
@ -107,4 +107,8 @@ the entire path back-to-front.
[^1]: I suppose the correct term would now be "meta-target predecessors". [^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 In fact, I will rename all occurences of `target` in the source to
`metaTargetPredecessors` – clumsy but accurate. `metaTargetPredecessors` – clumsy but accurate.
[^2]: Which due to 0-based indexing has index `k-1`, of course! Damn it.
[^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.
Loading…
Cancel
Save