diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 1dc1301e4..c1ef831f8 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,5 +1,6 @@ #include "shortestPaths.h" #include "graph.h" +#include "constants.h" namespace storm { namespace utility { @@ -8,15 +9,16 @@ namespace storm { ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model) : model(model) { // FIXME: does this create a copy? I don't need one, so I should avoid that transitionMatrix = model->getTransitionMatrix(); + numStates = model->getNumberOfStates(); - // TODO: init various things we'll need later - // - predecessors computePredecessors(); - // - Dijkstra (giving us SP-predecessors, SP-distances) + + // gives us SP-predecessors, SP-distances performDijkstra(); - // - SP-successors + computeSPSuccessors(); - // - shortest paths + + // constructs the recursive shortest path representations initializeShortestPaths(); } @@ -26,9 +28,10 @@ namespace storm { template void ShortestPathsGenerator::computePredecessors() { - graphPredecessors.resize(model->getNumberOfStates()); + graphPredecessors.resize(numStates); - for (int i = 0; i < transitionMatrix.getRowCount(); i++) { + assert(numStates == transitionMatrix.getRowCount()); + for (state_t i = 0; i < numStates; i++) { // what's the difference? TODO //auto foo = transitionMatrix.getRowGroupEntryCount(i); //auto bar = transitionMatrix.getRowGroupSize(i); @@ -41,19 +44,50 @@ namespace storm { template void ShortestPathsGenerator::performDijkstra() { - auto result = storm::utility::graph::performDijkstra(*model, transitionMatrix, model->getInitialStates()); - shortestPathDistances = result.first; - shortestPathPredecessors = result.second; - // FIXME: fix bad predecessor result for initial states (either here, or by fixing the Dijkstra) + // the existing Dijkstra isn't working anyway AND + // doesn't fully meet our requirements, so let's roll our own + + T inftyDistance = storm::utility::zero(); + T zeroDistance = storm::utility::one(); + shortestPathDistances.resize(numStates, inftyDistance); + shortestPathPredecessors.resize(numStates, boost::optional()); + + // set serves as priority queue with unique membership + // default comparison on pair actually works fine if distance is the first entry + std::set> dijkstraQueue; + + for (state_t initialState : model->getInitialStates()) { + shortestPathDistances[initialState] = zeroDistance; + dijkstraQueue.emplace(zeroDistance, initialState); + } + + while (!dijkstraQueue.empty()) { + state_t currentNode = (*dijkstraQueue.begin()).second; + dijkstraQueue.erase(dijkstraQueue.begin()); + + for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) { + state_t otherNode = transition.getColumn(); + + // note that distances are probabilities, thus they are multiplied and larger is better + T alternateDistance = shortestPathDistances[currentNode] * transition.getValue(); + if (alternateDistance > shortestPathDistances[otherNode]) { + shortestPathDistances[otherNode] = alternateDistance; + shortestPathPredecessors[otherNode] = boost::optional(currentNode); + dijkstraQueue.emplace(alternateDistance, otherNode); + } + } + } } template void ShortestPathsGenerator::computeSPSuccessors() { - shortestPathSuccessors.resize(model->getNumberOfStates()); + shortestPathSuccessors.resize(numStates); - for (int i = 0; i < model->getNumberOfStates(); i++) { - state_t predecessor = shortestPathPredecessors[i]; - shortestPathSuccessors[predecessor].push_back(i); + for (state_t i = 0; i < numStates; i++) { + if (shortestPathPredecessors[i]) { + state_t predecessor = shortestPathPredecessors[i].get(); + shortestPathSuccessors[predecessor].push_back(i); + } } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 1d31fd89f..d2d85cb62 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -29,12 +29,13 @@ namespace storm { private: //storm::models::sparse::Model* model; std::shared_ptr> model; - storm::storage::SparseMatrix transitionMatrix; + storm::storage::SparseMatrix transitionMatrix; + state_t numStates; - std::vector graphPredecessors; - std::vector shortestPathPredecessors; - std::vector shortestPathSuccessors; - std::vector shortestPathDistances; + std::vector graphPredecessors; + std::vector> shortestPathPredecessors; + std::vector shortestPathSuccessors; + std::vector shortestPathDistances; std::vector>> shortestPaths; std::vector>> shortestPathCandidates;