From b58d48f92dee69634dd1e7c8f378bc4d7beeb1eb Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Fri, 12 Feb 2016 23:54:27 +0100
Subject: [PATCH] use probs from targetProbMap TODO: test
---
src/utility/shortestPaths.cpp | 24 +++++++++++++-----------
src/utility/shortestPaths.h | 4 ++--
src/utility/shortestPaths.md | 12 +++++++-----
3 files changed, 22 insertions(+), 18 deletions(-)
diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp
index f70799d15..c9ce0b608 100644
--- a/src/utility/shortestPaths.cpp
+++ b/src/utility/shortestPaths.cpp
@@ -107,16 +107,18 @@ namespace storm {
for (state_t i = 0; i < numStates - 1; i++) {
for (auto const& transition : transitionMatrix.getRowGroup(i)) {
- // to avoid non-minimal paths, the target states are
+ // to avoid non-minimal paths, the meta-target-predecessors are
// *not* predecessors of any state but the meta-target
- if (!isTargetState(i)) {
+ if (!isMetaTargetPredecessor(i)) {
graphPredecessors[transition.getColumn()].push_back(i);
}
}
}
- // meta-target has exactly the target states as predecessors
- for (auto targetProbPair : targetProbMap) { // FIXME
+ // meta-target has exactly the meta-target-predecessors as predecessors
+ // (duh. note that the meta-target-predecessors used to be called target,
+ // but that's not necessarily true in the matrix/value invocation case)
+ for (auto targetProbPair : targetProbMap) {
graphPredecessors[metaTarget].push_back(targetProbPair.first);
}
}
@@ -144,7 +146,7 @@ namespace storm {
state_t currentNode = (*dijkstraQueue.begin()).second;
dijkstraQueue.erase(dijkstraQueue.begin());
- if (!isTargetState(currentNode)) {
+ if (!isMetaTargetPredecessor(currentNode)) {
// non-target node, treated normally
for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
state_t otherNode = transition.getColumn();
@@ -158,9 +160,9 @@ namespace storm {
}
}
} else {
- // target node has only "virtual edge" (with prob 1) to meta-target
- // no multiplication necessary
- T alternateDistance = shortestPathDistances[currentNode]; // FIXME
+ // node only has one "virtual edge" (with prob as per targetProbMap) to meta-target
+ // FIXME: double check
+ T alternateDistance = shortestPathDistances[currentNode] * targetProbMap[currentNode];
if (alternateDistance > shortestPathDistances[metaTarget]) {
shortestPathDistances[metaTarget] = alternateDistance;
shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode);
@@ -232,9 +234,9 @@ namespace storm {
assert(false);
return utility::zero<T>();
} else {
- // edge must be "virtual edge" from target state to meta-target
- assert(targetProbMap.count(tailNode) == 1);
- return one<T>();
+ // edge must be "virtual edge" to meta-target
+ assert(isMetaTargetPredecessor(tailNode));
+ return targetProbMap.at(tailNode); // FIXME double check
}
}
diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h
index b78a0758a..1cda2eb99 100644
--- a/src/utility/shortestPaths.h
+++ b/src/utility/shortestPaths.h
@@ -103,7 +103,7 @@ namespace storm {
BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap;
- std::vector<ordered_state_list_t> graphPredecessors; // FIXME is a switch to BitVector a good idea here?
+ std::vector<ordered_state_list_t> graphPredecessors;
std::vector<boost::optional<state_t>> shortestPathPredecessors;
std::vector<ordered_state_list_t> shortestPathSuccessors;
std::vector<T> shortestPathDistances;
@@ -167,7 +167,7 @@ namespace storm {
return find(initialStates.begin(), initialStates.end(), node) != initialStates.end();
}
- inline bool isTargetState(state_t node) const {
+ inline bool isMetaTargetPredecessor(state_t node) const {
return targetProbMap.count(node) == 1;
}
diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md
index db5dcc326..f2beb801a 100644
--- a/src/utility/shortestPaths.md
+++ b/src/utility/shortestPaths.md
@@ -52,9 +52,8 @@ 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 (I suppose the correct term
-would now be "meta-target predecessors"), but nevertheless it should work
-exactly the same. [Right?]
+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
@@ -98,11 +97,14 @@ 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[^1] being the k-th SP to that node.
+with the k-th entry[^2] 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]: Which due to 0-based indexing has index `k-1`, of course! Damn it.
+[^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.