Browse Source

use probs from targetProbMap TODO: test

tempestpy_adaptions
tomjanson 9 years ago
committed by Tom Janson
parent
commit
b58d48f92d
  1. 24
      src/utility/shortestPaths.cpp
  2. 4
      src/utility/shortestPaths.h
  3. 12
      src/utility/shortestPaths.md

24
src/utility/shortestPaths.cpp

@ -107,16 +107,18 @@ namespace storm {
for (state_t i = 0; i < numStates - 1; i++) { for (state_t i = 0; i < numStates - 1; i++) {
for (auto const& transition : transitionMatrix.getRowGroup(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 // *not* predecessors of any state but the meta-target
if (!isTargetState(i)) {
if (!isMetaTargetPredecessor(i)) {
graphPredecessors[transition.getColumn()].push_back(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); graphPredecessors[metaTarget].push_back(targetProbPair.first);
} }
} }
@ -144,7 +146,7 @@ namespace storm {
state_t currentNode = (*dijkstraQueue.begin()).second; state_t currentNode = (*dijkstraQueue.begin()).second;
dijkstraQueue.erase(dijkstraQueue.begin()); dijkstraQueue.erase(dijkstraQueue.begin());
if (!isTargetState(currentNode)) {
if (!isMetaTargetPredecessor(currentNode)) {
// non-target node, treated normally // non-target node, treated normally
for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) { for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) {
state_t otherNode = transition.getColumn(); state_t otherNode = transition.getColumn();
@ -158,9 +160,9 @@ namespace storm {
} }
} }
} else { } 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]) { if (alternateDistance > shortestPathDistances[metaTarget]) {
shortestPathDistances[metaTarget] = alternateDistance; shortestPathDistances[metaTarget] = alternateDistance;
shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode); shortestPathPredecessors[metaTarget] = boost::optional<state_t>(currentNode);
@ -232,9 +234,9 @@ namespace storm {
assert(false); assert(false);
return utility::zero<T>(); return utility::zero<T>();
} else { } 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
} }
} }

4
src/utility/shortestPaths.h

@ -103,7 +103,7 @@ namespace storm {
BitVector initialStates; BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap; 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<boost::optional<state_t>> shortestPathPredecessors;
std::vector<ordered_state_list_t> shortestPathSuccessors; std::vector<ordered_state_list_t> shortestPathSuccessors;
std::vector<T> shortestPathDistances; std::vector<T> shortestPathDistances;
@ -167,7 +167,7 @@ namespace storm {
return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); 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; return targetProbMap.count(node) == 1;
} }

12
src/utility/shortestPaths.md

@ -52,9 +52,8 @@ implied target state.
This naturally corresponds to having a meta-target, except the probability This naturally corresponds to having a meta-target, except the probability
of its incoming edges range over $(0,1]$ rather than being $1$. 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 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 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 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 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[^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`) 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.
By recursively looking up the tail (until it's empty), we reconstruct By recursively looking up the tail (until it's empty), we reconstruct
the entire path back-to-front. 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.
Loading…
Cancel
Save