diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index c1ef831f8..f2170bc9f 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,3 +1,4 @@ +#include #include "shortestPaths.h" #include "graph.h" #include "constants.h" @@ -32,10 +33,6 @@ namespace storm { assert(numStates == transitionMatrix.getRowCount()); for (state_t i = 0; i < numStates; i++) { - // what's the difference? TODO - //auto foo = transitionMatrix.getRowGroupEntryCount(i); - //auto bar = transitionMatrix.getRowGroupSize(i); - for (auto transition : transitionMatrix.getRowGroup(i)) { graphPredecessors[transition.getColumn()].push_back(i); } @@ -92,7 +89,38 @@ namespace storm { } template - void ShortestPathsGenerator::initializeShortestPaths() {} + void ShortestPathsGenerator::initializeShortestPaths() { + kShortestPaths.resize(numStates); + candidatePaths.resize(numStates); + + // BFS in Dijkstra-SP order + std::queue bfsQueue; + for (state_t initialState : model->getInitialStates()) { + bfsQueue.push(initialState); + } + + while (!bfsQueue.empty()) { + state_t currentNode = bfsQueue.front(); + bfsQueue.pop(); + + if (!kShortestPaths[currentNode].empty()) { + continue; // already visited + } + + for (state_t successorNode : shortestPathSuccessors[currentNode]) { + bfsQueue.push(successorNode); + } + + // note that `shortestPathPredecessor` may not be present + // if current node is an initial state + // in this case, the boost::optional copy of an uninitialized optional is hopefully also uninitialized + kShortestPaths[currentNode].push_back(Path { + shortestPathPredecessors[currentNode], + 1, + shortestPathDistances[currentNode] + }); + } + } } } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index d2d85cb62..31733c9d3 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -12,10 +12,27 @@ namespace storm { typedef storm::storage::sparse::state_type state_t; typedef std::vector state_list_t; + /* + * Implicit shortest path representation + * + * All shortest paths (from s to t) can be described as some + * k-shortest path to some node u plus the edge to t: + * + * s ~~k-shortest path~~> u --> t + * + * This struct stores u (`pathPredecessor`) and k (`predecessorK`). + * + * t is implied by this struct's location: It is stored in the + * k-shortest paths list associated with t. + * + * Thus we can reconstruct the entire path by recursively looking + * up the path's tail stored as the k-th entry of the predecessor's + * shortest paths list. + */ template - struct path { - boost::optional tail; - unsigned int tail_k; + struct Path { + boost::optional pathPredecessor; + unsigned int predecessorK; T distance; }; @@ -37,8 +54,8 @@ namespace storm { std::vector shortestPathSuccessors; std::vector shortestPathDistances; - std::vector>> shortestPaths; - std::vector>> shortestPathCandidates; + std::vector>> kShortestPaths; + std::vector>> candidatePaths; /*! * Computes list of predecessors for all nodes.