From 6d1608a14787e82058783daee4a51d3c4058933b Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 25 Oct 2015 17:38:10 +0100 Subject: [PATCH] Dijkstra fixed, maybe TODO: check; improve Things that aren't going well: - On the example graph BRP-16-2, all nodes have distance 1. I that possible?? - The initial states list themself as their own predecessor. That's bad, because it's simply false (unless there is a self-loop). Former-commit-id: 06f9a283064c17533f6d5cb4a0959aab0cf98005 [formerly e7e2385e0d335dfd2e4c4fb2c008028da6babef6] Former-commit-id: 350501183197c5c5baaad6ab14e87b28202ee76d --- src/storm/utility/graph.cpp | 49 +++++++++++++++++++++++++---------- src/storm/utility/graph.h | 3 ++- src/utility/shortestPaths.cpp | 5 ++++ src/utility/shortestPaths.h | 15 +++++++++++ 4 files changed, 57 insertions(+), 15 deletions(-) create mode 100644 src/utility/shortestPaths.cpp create mode 100644 src/utility/shortestPaths.h 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/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp new file mode 100644 index 000000000..0c778d55b --- /dev/null +++ b/src/utility/shortestPaths.cpp @@ -0,0 +1,5 @@ +// +// Created by Tom Janson on 15-1025. +// + +#include "shortestPaths.h" diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h new file mode 100644 index 000000000..28e9e7c16 --- /dev/null +++ b/src/utility/shortestPaths.h @@ -0,0 +1,15 @@ +// +// Created by Tom Janson on 15-1025. +// + +#ifndef STORM_UTIL_SHORTESTPATHS_H_ +#define STORM_UTIL_SHORTESTPATHS_H_ + + + +class shortestPathsUtil { + +}; + + +#endif //STORM_UTIL_SHORTESTPATHS_H_