Dijkstra implementation

Originally, I tried to adapt the existing (but in various ways broken)
Dijkstra implementation in `storm::utility::graph::performDijkstra`,
but that proved to be more cumbersome (mostly because of the behaviour on
initial states) than simply rolling my own -- so that's what I
eventually did.

Former-commit-id: 33b2be8067 [formerly 0d5c507568]
Former-commit-id: b35fc0bee3

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<T>::ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> 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 <typename T>
             void ShortestPathsGenerator<T>::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 <typename T>
             void ShortestPathsGenerator<T>::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>();
+                T zeroDistance = storm::utility::one<T>();
+                shortestPathDistances.resize(numStates, inftyDistance);
+                shortestPathPredecessors.resize(numStates, boost::optional<state_t>());
+
+                // set serves as priority queue with unique membership
+                // default comparison on pair actually works fine if distance is the first entry
+                std::set<std::pair<T, state_t>> 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<state_t>(currentNode);
+                            dijkstraQueue.emplace(alternateDistance, otherNode);
+                        }
+                    }
+                }
             }
 
             template <typename T>
             void ShortestPathsGenerator<T>::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);
+                    }
                 }
             }
 

src/utility/shortestPaths.h

@@ -29,12 +29,13 @@ namespace storm {
             private:
                 //storm::models::sparse::Model<T>* model;
                 std::shared_ptr<storm::models::sparse::Model<T>> model;
-                storm::storage::SparseMatrix<T>  transitionMatrix;
+                storm::storage::SparseMatrix<T> transitionMatrix;
+                state_t numStates;
 
-                std::vector<state_list_t> graphPredecessors;
-                std::vector<state_t>      shortestPathPredecessors;
-                std::vector<state_list_t> shortestPathSuccessors;
-                std::vector<T>            shortestPathDistances;
+                std::vector<state_list_t>             graphPredecessors;
+                std::vector<boost::optional<state_t>> shortestPathPredecessors;
+                std::vector<state_list_t>             shortestPathSuccessors;
+                std::vector<T>                        shortestPathDistances;
 
                 std::vector<std::vector<path<T>>> shortestPaths;
                 std::vector<std::set<path<T>>>    shortestPathCandidates;