From df195d85f68974398b8411304430bc9b0a02a660 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Tue, 27 Oct 2015 23:20:03 +0100 Subject: [PATCH] REA fully implemented; needs testing Former-commit-id: 9795a24835822be49225e24cf0a680a8a54628bd [formerly fc732962dda71a65ab2585463ea765725aa13cb9] Former-commit-id: 0ae2abacd112f2a4ce1f197ac3f1fc9742346f78 --- src/test/utility/GraphTest.cpp | 6 +++ src/utility/shortestPaths.cpp | 94 ++++++++++++++++++++++++++++++++-- src/utility/shortestPaths.h | 52 +++++++++++++++++-- 3 files changed, 145 insertions(+), 7 deletions(-) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 7b1871d2d..0d43c02ad 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -276,6 +276,12 @@ TEST(GraphTest, kshortest) { storm::utility::shortestPaths::ShortestPathsGenerator shortestPathsGenerator(model); + storm::storage::sparse::state_type exampleState = 50; + + for (int i = 1; i < 20; i++) { + auto foo = shortestPathsGenerator.getKShortest(exampleState, i); + } + // TODO: actually write tests here EXPECT_TRUE(false); diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index afb849792..9a51e7c7c 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,7 +1,7 @@ #include +#include #include "shortestPaths.h" #include "graph.h" -#include "constants.h" namespace storm { namespace utility { @@ -21,6 +21,8 @@ namespace storm { // constructs the recursive shortest path representations initializeShortestPaths(); + + candidatePaths.resize(numStates); } template @@ -53,7 +55,7 @@ namespace storm { // set serves as priority queue with unique membership // default comparison on pair actually works fine if distance is the first entry - std::set> dijkstraQueue; + std::set, std::greater_equal>> dijkstraQueue; for (state_t initialState : model->getInitialStates()) { shortestPathDistances[initialState] = zeroDistance; @@ -124,7 +126,93 @@ namespace storm { } template - void ShortestPathsGenerator::printKShortestPath(state_t targetNode, int k, bool head) { + void ShortestPathsGenerator::computeNextPath(state_t node, unsigned long k) { + assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist + + if (k == 2) { + Path shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-| + + for (state_t predecessor : graphPredecessors[node]) { + // add shortest paths to predecessors plus edge to current node + Path pathToPredecessorPlusEdge = { + boost::optional(predecessor), + 1, + shortestPathDistances[predecessor] * getEdgeDistance(predecessor, node) + }; + candidatePaths[node].insert(pathToPredecessorPlusEdge); + + // ... but not the actual shortest path + auto it = find(candidatePaths[node].begin(), candidatePaths[node].end(), shortestPathToNode); + if (it != candidatePaths[node].end()) { + candidatePaths[node].erase(it); + } + } + } + + if (k > 2 || !isInitialState(node)) { + // 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 + + // the predecessor node on that path + state_t predecessor = previousShortestPath.predecessorNode.get(); + // the path to that predecessor was the `tailK`-shortest + unsigned long tailK = previousShortestPath.predecessorK; + + // i.e. source ~~tailK-shortest path~~> predecessor --> node + + // compute one-worse-shortest path to the predecessor (if it hasn't yet been computed) + if (kShortestPaths[predecessor].size() < tailK + 1) { + // TODO: investigate recursion depth and possible iterative alternative + computeNextPath(predecessor, tailK + 1); + } + + if (kShortestPaths[predecessor].size() >= tailK + 1) { + // take that path, add an edge to the current node; that's a candidate + Path pathToPredecessorPlusEdge = { + boost::optional(predecessor), + tailK + 1, + kShortestPaths[predecessor][tailK + 1 - 1].distance * getEdgeDistance(predecessor, node) + }; + candidatePaths[node].insert(pathToPredecessorPlusEdge); + } + // else there was no path; TODO: does this need handling? + } + + if (!candidatePaths[node].empty()) { + Path minDistanceCandidate = *(candidatePaths[node].begin()); + for (auto path : candidatePaths[node]) { + if (path.distance > minDistanceCandidate.distance) { + minDistanceCandidate = path; + } + } + + candidatePaths[node].erase(find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate)); + kShortestPaths[node].push_back(minDistanceCandidate); + } + } + + template + Path ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { + unsigned long alreadyComputedK = kShortestPaths[node].size(); + + for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { + computeNextPath(node, nextK); + if (kShortestPaths[node].size() < nextK) { + break; + } + } + + if (kShortestPaths[node].size() >= k) { + printKShortestPath(node, k); // DEBUG + } else { + std::cout << "No other path exists!" << std::endl; + } + + return kShortestPaths[node][k - 1]; + } + + template + void ShortestPathsGenerator::printKShortestPath(state_t targetNode, unsigned long k, bool head) { // note the index shift! risk of off-by-one Path p = kShortestPaths[targetNode][k - 1]; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 42bb2edee..6aba88434 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -5,6 +5,7 @@ #include #include "src/models/sparse/Model.h" #include "src/storage/sparse/StateType.h" +#include "constants.h" namespace storm { namespace utility { @@ -26,23 +27,44 @@ namespace storm { * 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. + * up the path's tail stored as the k-th entry [1] of the + * predecessor's shortest paths list. + * + * [1] oh, actually, the `k-1`th entry due to 0-based indexing! */ template struct Path { boost::optional predecessorNode; - unsigned int predecessorK; + unsigned long predecessorK; T distance; + + // FIXME: uhh.. is this okay for set? just some arbitrary order + bool operator<(const Path& rhs) const { + if (predecessorNode != rhs.predecessorNode) { + return predecessorNode < rhs.predecessorNode; + } + return predecessorK < predecessorK; + } + + bool operator==(const Path& rhs) const { + return (predecessorNode == rhs.predecessorNode) && (predecessorK == rhs.predecessorK); + } }; + // ------------------------------------------------------------------------------------------------------- + template class ShortestPathsGenerator { public: // FIXME: this shared_ptr-passing business is probably a bad idea ShortestPathsGenerator(std::shared_ptr> model); + ~ShortestPathsGenerator(); + // TODO: think about suitable output format + Path getKShortest(state_t node, unsigned long k); + + private: std::shared_ptr> model; storm::storage::SparseMatrix transitionMatrix; @@ -85,10 +107,32 @@ namespace storm { */ void initializeShortestPaths(); + /*! + * Main step of REA algorithm. TODO: Document further. + */ + void computeNextPath(state_t node, unsigned long k); + /*! * Recurses over the path and prints the nodes. Intended for debugging. */ - void printKShortestPath(state_t targetNode, int k, bool head=true); + void printKShortestPath(state_t targetNode, unsigned long k, bool head=true); + + + // --- tiny helper fcts --- + bool isInitialState(state_t node) { + auto initialStates = model->getInitialStates(); + return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); + } + + T getEdgeDistance(state_t tailNode, state_t headNode) { + for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) { + if (transition.getColumn() == headNode) { + return transition.getValue(); + } + } + return storm::utility::zero(); + } + // ----------------------- }; } }