From b71ef02692cc44fb0865f6b3d4efd04a8e6a5d2a Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Tue, 20 Dec 2016 17:51:00 +0100 Subject: [PATCH] comments and fixes (?) to graph.cpp's Dijkstra This implementation seemed pretty wrong in multiple ways; I attempted to fix it (a long time ago) (see diff, you'll see what I'm talking about), then gave up. Luckily (?) the code is unused, just sitting there, sad and broken. --- src/storm/utility/graph.cpp | 49 ++++++++++++++++++++++++---------- src/storm/utility/graph.h | 3 ++- src/test/utility/GraphTest.cpp | 1 + 3 files changed, 38 insertions(+), 15 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 7604c45af..694697c61 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -992,7 +992,8 @@ namespace storm { } - + + // There seems to be a lot of stuff wrong here. FIXME: Check whether it works now. -Tom template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, @@ -1016,26 +1017,43 @@ namespace storm { // As long as there is one reachable state, we need to consider it. while (!probabilityStateSet.empty()) { // Get the state with the least distance from the set and remove it. - std::pair probabilityStatePair = probabilityStateSet.erase(probabilityStateSet.begin()); - + // FIXME? is this correct? this used to take the second element!! + std::pair probabilityStatePair = *(probabilityStateSet.begin()); + probabilityStateSet.erase(probabilityStateSet.begin()); + + uint_fast64_t currentNode = probabilityStatePair.second; + // Now check the new distances for all successors of the current state. - typename storm::storage::SparseMatrix::Rows row = transitions.getRow(probabilityStatePair.second); + typename storm::storage::SparseMatrix::const_rows row = transitions.getRowGroup(currentNode); for (auto const& transition : row) { + uint_fast64_t targetNode = transition.getColumn(); + // Only follow the transition if it lies within the filtered states. - if (filterStates != nullptr && filterStates->get(transition.first)) { + // -- shouldn't "no filter" (nullptr) mean that all nodes are checked? - Tom FIXME + if (filterStates == nullptr || filterStates->get(targetNode)) { + // Calculate the distance we achieve when we take the path to the successor via the current state. - T newDistance = probabilityStatePair.first; + // FIXME: this should be multiplied with the distance to the current node, right? + //T newDistance = probabilityStatePair.first; + T edgeProbability = probabilityStatePair.first; + T newDistance = probabilities[currentNode] * edgeProbability; + + // DEBUG + if (newDistance != 1) { + std::cout << "yay" << std::endl; + } + // We found a cheaper way to get to the target state of the transition. - if (newDistance > probabilities[transition.first]) { + if (newDistance > probabilities[targetNode]) { // Remove the old distance. - if (probabilities[transition.first] != noPredecessorValue) { - probabilityStateSet.erase(std::make_pair(probabilities[transition.first], transition.first)); + if (probabilities[targetNode] != noPredecessorValue) { + probabilityStateSet.erase(std::make_pair(probabilities[targetNode], targetNode)); } // Set and add the new distance. - probabilities[transition.first] = newDistance; - predecessors[transition.first] = probabilityStatePair.second; - probabilityStateSet.insert(std::make_pair(newDistance, transition.first)); + probabilities[targetNode] = newDistance; + predecessors[targetNode] = currentNode; + probabilityStateSet.insert(std::make_pair(newDistance, targetNode)); } } } @@ -1179,8 +1197,11 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + + template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, storm::storage::BitVector const* filterStates); + + // Instantiations for storm::RationalNumber. #ifdef STORM_HAVE_CARL template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 13100e3ac..770af42d4 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -544,13 +544,14 @@ namespace storm { * @param transitions The transitions wrt to which to compute the most probable paths. * @param startingStates The starting states of the Dijkstra search. * @param filterStates A set of states that must not be left on any path. + * @return A pair consisting of a vector of distances and a vector of shortest path predecessors */ template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, storm::storage::BitVector const* filterStates = nullptr); - + } // namespace graph } // namespace utility } // namespace storm diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index dff3ccc53..76e17299c 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -12,6 +12,7 @@ #include "storm/builder/DdPrismModelBuilder.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/utility/graph.h" +#include "storm/utility/shortestPaths.cpp" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/DdManager.h"