path construction

thanks to new Dijkstra, the (1-)shortest paths construction code is
simpler

Former-commit-id: ec2ef461b8 [formerly 5757d66bc5]
Former-commit-id: 00f3d35a38

src/utility/shortestPaths.cpp

@@ -1,3 +1,4 @@
+#include <queue>
 #include "shortestPaths.h"
 #include "graph.h"
 #include "constants.h"
@@ -32,10 +33,6 @@ namespace storm {
 
                 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);
-
                     for (auto transition : transitionMatrix.getRowGroup(i)) {
                         graphPredecessors[transition.getColumn()].push_back(i);
                     }
@@ -92,7 +89,38 @@ namespace storm {
             }
 
             template <typename T>
-            void ShortestPathsGenerator<T>::initializeShortestPaths() {}
+            void ShortestPathsGenerator<T>::initializeShortestPaths() {
+                kShortestPaths.resize(numStates);
+                candidatePaths.resize(numStates);
+
+                // BFS in Dijkstra-SP order
+                std::queue<state_t> bfsQueue;
+                for (state_t initialState : model->getInitialStates()) {
+                    bfsQueue.push(initialState);
+                }
+
+                while (!bfsQueue.empty()) {
+                    state_t currentNode = bfsQueue.front();
+                    bfsQueue.pop();
+
+                    if (!kShortestPaths[currentNode].empty()) {
+                        continue; // already visited
+                    }
+
+                    for (state_t successorNode : shortestPathSuccessors[currentNode]) {
+                        bfsQueue.push(successorNode);
+                    }
+
+                    // note that `shortestPathPredecessor` may not be present
+                    // if current node is an initial state
+                    // in this case, the boost::optional copy of an uninitialized optional is hopefully also uninitialized
+                    kShortestPaths[currentNode].push_back(Path<T> {
+                            shortestPathPredecessors[currentNode],
+                            1,
+                            shortestPathDistances[currentNode]
+                    });
+                }
+            }
         }
     }
 }

src/utility/shortestPaths.h

@@ -12,10 +12,27 @@ namespace storm {
             typedef storm::storage::sparse::state_type state_t;
             typedef std::vector<state_t> state_list_t;
 
+            /*
+             * Implicit shortest path representation
+             *
+             * All shortest paths (from s to t) can be described as some
+             * k-shortest path to some node u plus the edge to t:
+             *
+             *     s ~~k-shortest path~~> u --> t
+             *
+             * This struct stores u (`pathPredecessor`) and k (`predecessorK`).
+             *
+             * t is implied by this struct's location: It is stored in the
+             * k-shortest paths list associated with t.
+             *
+             * Thus we can reconstruct the entire path by recursively looking
+             * up the path's tail stored as the k-th entry of the predecessor's
+             * shortest paths list.
+             */
             template <typename T>
-            struct path {
-                boost::optional<state_t> tail;
-                unsigned int tail_k;
+            struct Path {
+                boost::optional<state_t> pathPredecessor;
+                unsigned int predecessorK;
                 T distance;
             };
 
@@ -37,8 +54,8 @@ namespace storm {
                 std::vector<state_list_t>             shortestPathSuccessors;
                 std::vector<T>                        shortestPathDistances;
 
-                std::vector<std::vector<path<T>>> shortestPaths;
-                std::vector<std::set<path<T>>>    shortestPathCandidates;
+                std::vector<std::vector<Path<T>>> kShortestPaths;
+                std::vector<std::set<Path<T>>>    candidatePaths;
 
                 /*!
                  * Computes list of predecessors for all nodes.