From 83445f67c319aaadd3bfb7fdc98f9b2a43164856 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 18 Nov 2016 16:55:05 +0100 Subject: [PATCH] kSP: a few more comments --- src/utility/shortestPaths.cpp | 29 ++++++++++++++++++++++++----- src/utility/shortestPaths.md | 10 +++++++--- 2 files changed, 31 insertions(+), 8 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index ad25e2616..2a7c21285 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,8 +1,16 @@ #include #include +#include + +#include "macros.h" #include "shortestPaths.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 utility { namespace ksp { @@ -249,9 +257,13 @@ namespace storm { template void ShortestPathsGenerator::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 + // TODO: I could extract the candidate generation to make this function more succinct if (k == 2) { + // Step B.1 in J&M paper + Path shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-| 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) Path previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN @@ -297,9 +311,10 @@ namespace storm { }; 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()) { Path minDistanceCandidate = *(candidatePaths[node].begin()); for (auto path : candidatePaths[node]) { @@ -310,6 +325,9 @@ namespace storm { candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), 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++) { computeNextPath(metaTarget, 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)); } } diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md index f2beb801a..13dc96376 100644 --- a/src/utility/shortestPaths.md +++ b/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. (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 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 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[^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`) 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". In fact, I will rename all occurences of `target` in the source to `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.