From 38d22093a3cfbcff79dd2c32901f1693ee52edad Mon Sep 17 00:00:00 2001 From: tomjanson Date: Tue, 27 Oct 2015 18:11:59 +0100 Subject: [PATCH] documentation / cleanup Former-commit-id: e7798a5669159ff2e050d8125382e4df404ae981 [formerly 43dd865fbc66eb07365643907c2824f6db12762a] Former-commit-id: 6fb69a017c05076a7e5ded14a7f2351226e0cc27 --- src/test/utility/GraphTest.cpp | 65 +--------------------------------- src/utility/shortestPaths.cpp | 13 ++++--- src/utility/shortestPaths.h | 28 +++++++++++---- 3 files changed, 28 insertions(+), 78 deletions(-) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 248e4a69b..7b1871d2d 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -278,68 +278,5 @@ TEST(GraphTest, kshortest) { // TODO: actually write tests here - /* - std::queue nodeQueue; - for (uint_fast64_t initialNode : model->getInitialStates()) { - for (uint_fast64_t succ : shortestPathSuccessors[initialNode]) { - nodeQueue.push(succ); - } - storm::storage::sparse::path path; - path.tail_k = 1; - path.distance = dijkstraDistance[initialNode]; - assert(path.distance == 1); - kShortestPaths[initialNode].push_back(path); - } - - // Dijkstra BFS - while (!nodeQueue.empty()) { - uint_fast64_t currentNode = nodeQueue.front(); - nodeQueue.pop(); - - for (auto succ : shortestPathSuccessors[currentNode]) { - nodeQueue.push(succ); - } - - storm::storage::sparse::path path; - path.tail = shortestPathPredecessor[currentNode]; - path.tail_k = 1; - path.distance = dijkstraDistance[currentNode]; - kShortestPaths[currentNode].push_back(path); - } - */ - - // FIXME: ~~treat starting node(s) separately~~ actually, this whole thing should be done differently: - // first I need to run over the Dijkstra result and make a tree (as vector of vectors) of successors, - // then walk that tree DF/BF - /* - for (auto node : model->getInitialStates()) { - storm::storage::sparse::path p = {}; - p.distance = dijkstraDistance[node]; - assert(p.distance == 1); - kShortestPaths[node].emplace_back(p); - } - */ - - // shortest paths are stored recursively, so the predecessor must always be dealt with first - // by considering the nodes in order of distance, we should have roughly the correct order, - // but not quite: in the case s ~~~> u -1-> v, v might be listed before u, in which case it must be deferred - /* - while (!nodeQueue.empty()) { - std::pair distanceStatePair = nodeQueue.front(); - nodeQueue.pop(); - - uint_fast64_t currentNode = distanceStatePair.second; - - uint_fast64_t predecessor = shortestPathPredecessors[currentNode]; - if (kShortestPaths[predecessor].empty) { - // we need to take care of the predecessor first; defer this one - nodeQueue.emplace(currentNode); - continue; - } else { - //shortestPaths[currentNode].emplace(predecessor, 1, ) - } - } - */ - EXPECT_TRUE(false); -} +} \ No newline at end of file diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 2092bf7a5..afb849792 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -21,8 +21,6 @@ namespace storm { // constructs the recursive shortest path representations initializeShortestPaths(); - - printKShortestPath(400, 1); // DEBUG } template @@ -31,11 +29,13 @@ namespace storm { template void ShortestPathsGenerator::computePredecessors() { - graphPredecessors.resize(numStates); + auto rowCount = transitionMatrix.getRowCount(); + assert(numStates == rowCount); - assert(numStates == transitionMatrix.getRowCount()); - for (state_t i = 0; i < numStates; i++) { - for (auto transition : transitionMatrix.getRowGroup(i)) { + graphPredecessors.resize(rowCount); + + for (state_t i = 0; i < rowCount; i++) { + for (auto const& transition : transitionMatrix.getRowGroup(i)) { graphPredecessors[transition.getColumn()].push_back(i); } } @@ -93,7 +93,6 @@ namespace storm { template void ShortestPathsGenerator::initializeShortestPaths() { kShortestPaths.resize(numStates); - candidatePaths.resize(numStates); // BFS in Dijkstra-SP order std::queue bfsQueue; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 91f5c7843..42bb2edee 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -44,7 +44,6 @@ namespace storm { ~ShortestPathsGenerator(); private: - //storm::models::sparse::Model* model; std::shared_ptr> model; storm::storage::SparseMatrix transitionMatrix; state_t numStates; @@ -59,19 +58,34 @@ namespace storm { /*! * Computes list of predecessors for all nodes. - * Reachability is not considered; a predecessor is simply any node that has an edge leading to the - * node in question. - * - * @param model The model whose transitions will be examined - * @return A vector of predecessors for each node + * Reachability is not considered; a predecessor is simply any node that has an edge leading to the node in question. + * Requires `transitionMatrix`. + * Modifies `graphPredecessors`. */ void computePredecessors(); + /*! + * Computes shortest path distances and predecessors. + * Requires `model`, `numStates`, `transitionMatrix`. + * Modifies `shortestPathPredecessors` and `shortestPathDistances`. + */ void performDijkstra(); + + /*! + * Computes list of shortest path successor nodes from predecessor list. + * Requires `shortestPathPredecessors`, `numStates`. + * Modifies `shortestPathSuccessors`. + */ void computeSPSuccessors(); + + /*! + * Constructs and stores the implicit shortest path representations (see `Path`) for the (1-)shortest paths. + * Requires `shortestPathPredecessors`, `shortestPathDistances`, `model`, `numStates`. + * Modifies `kShortestPaths`. + */ void initializeShortestPaths(); - /* + /*! * Recurses over the path and prints the nodes. Intended for debugging. */ void printKShortestPath(state_t targetNode, int k, bool head=true);