From f390aeadf3f5bb16891dfd8ca0c4c43f864d5a0d Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Tue, 20 Dec 2016 17:59:12 +0100 Subject: [PATCH] rm broken Dijkstra from graph.cpp --- src/storm/utility/graph.cpp | 80 ------------------------------------- src/storm/utility/graph.h | 26 ------------ 2 files changed, 106 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 694697c61..f14578edb 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -990,86 +990,8 @@ namespace storm { return topologicalSort; } - - - // 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, - storm::storage::BitVector const& startingStates, - storm::storage::BitVector const* filterStates) { - - STORM_LOG_INFO("Performing Dijkstra search."); - - const uint_fast64_t noPredecessorValue = storm::utility::zero(); - std::vector probabilities(model.getNumberOfStates(), storm::utility::zero()); - std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); - - // Set the probability to 1 for all starting states. - std::set, DistanceCompare> probabilityStateSet; - - for (auto state : startingStates) { - probabilityStateSet.emplace(storm::utility::one(), state); - probabilities[state] = storm::utility::one(); - } - - // 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. - // 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::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. - // -- 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. - // 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[targetNode]) { - // Remove the old distance. - if (probabilities[targetNode] != noPredecessorValue) { - probabilityStateSet.erase(std::make_pair(probabilities[targetNode], targetNode)); - } - - // Set and add the new distance. - probabilities[targetNode] = newDistance; - predecessors[targetNode] = currentNode; - probabilityStateSet.insert(std::make_pair(newDistance, targetNode)); - } - } - } - } - - // Move the values into the result and return it. - std::pair, std::vector> result; - result.first = std::move(probabilities); - result.second = std::move(predecessors); - STORM_LOG_INFO("Done performing Dijkstra search."); - return result; - } - - - - 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); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); @@ -1199,8 +1121,6 @@ namespace storm { 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 diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 770af42d4..c30318767 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -525,32 +525,6 @@ namespace storm { */ template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - - /*! - * A class needed to compare the distances for two states in the Dijkstra search. - */ - template - struct DistanceCompare { - bool operator()(std::pair const& lhs, std::pair const& rhs) const { - return lhs.first > rhs.first || (lhs.first == rhs.first && lhs.second > rhs.second); - } - }; - - /*! - * Performs a Dijkstra search from the given starting states to determine the most probable paths to all other states - * by only passing through the given state set. - * - * @param model The model whose state space is to be searched. - * @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