shortest paths generator skeleton

Former-commit-id: c37fdbbec8 [formerly 23dba537c7]
Former-commit-id: 6eb54e64ad

src/test/utility/GraphTest.cpp

@@ -12,6 +12,7 @@
 #include "storm/builder/DdPrismModelBuilder.h"
 #include "storm/builder/ExplicitModelBuilder.h"
 #include "storm/utility/graph.h"
+#include "storm/utility/shortestPaths.cpp"
 #include "storm/storage/dd/Add.h"
 #include "storm/storage/dd/Bdd.h"
 #include "storm/storage/dd/DdManager.h"
@@ -264,13 +265,81 @@ TEST(GraphTest, ExplicitProb01MinMax) {
     EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits());
 }
 
+
 TEST(GraphTest, kshortest) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
 
-    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
+
+    model->printModelInformationToStream(std::cout);
+
+    storm::utility::shortestPaths::ShortestPathsGenerator<double> shortestPathsGenerator(model);
+
+    // TODO: actually write tests here
+
+    /*
+    std::queue<uint_fast64_t> nodeQueue;
+    for (uint_fast64_t initialNode : model->getInitialStates()) {
+        for (uint_fast64_t succ : shortestPathSuccessors[initialNode]) {
+            nodeQueue.push(succ);
+        }
+        storm::storage::sparse::path<double> path;
+        path.tail_k = 1;
+        path.distance = dijkstraDistance[initialNode];
+        assert(path.distance == 1);
+        kShortestPaths[initialNode].push_back(path);
+    }
+
+    // Dijkstra BFS
+    while (!nodeQueue.empty()) {
+        uint_fast64_t currentNode = nodeQueue.front();
+        nodeQueue.pop();
 
-    std::cout << model->getNumberOfStates() << std::endl;
+        for (auto succ : shortestPathSuccessors[currentNode]) {
+            nodeQueue.push(succ);
+        }
+
+        storm::storage::sparse::path<double> path;
+        path.tail = shortestPathPredecessor[currentNode];
+        path.tail_k = 1;
+        path.distance = dijkstraDistance[currentNode];
+        kShortestPaths[currentNode].push_back(path);
+    }
+    */
+
+    // FIXME: ~~treat starting node(s) separately~~ actually, this whole thing should be done differently:
+    // first I need to run over the Dijkstra result and make a tree (as vector of vectors) of successors,
+    // then walk that tree DF/BF
+    /*
+    for (auto node : model->getInitialStates()) {
+        storm::storage::sparse::path<double> p = {};
+        p.distance = dijkstraDistance[node];
+        assert(p.distance == 1);
+        kShortestPaths[node].emplace_back(p);
+    }
+    */
+
+    // shortest paths are stored recursively, so the predecessor must always be dealt with first
+    // by considering the nodes in order of distance, we should have roughly the correct order,
+    // but not quite: in the case s ~~~> u -1-> v, v might be listed before u, in which case it must be deferred
+    /*
+    while (!nodeQueue.empty()) {
+        std::pair<double, uint_fast64_t> distanceStatePair = nodeQueue.front();
+        nodeQueue.pop();
+
+        uint_fast64_t currentNode = distanceStatePair.second;
+
+        uint_fast64_t predecessor = shortestPathPredecessors[currentNode];
+        if (kShortestPaths[predecessor].empty) {
+            // we need to take care of the predecessor first; defer this one
+            nodeQueue.emplace(currentNode);
+            continue;
+        } else {
+            //shortestPaths[currentNode].emplace(predecessor, 1, )
+        }
+    }
+    */
 
     EXPECT_TRUE(false);
-}
+}

src/utility/shortestPaths.cpp

@@ -1,5 +1,64 @@
-//
-// Created by Tom Janson on 15-1025.
-//
-
 #include "shortestPaths.h"
+#include "graph.h"
+
+namespace storm {
+    namespace utility {
+        namespace shortestPaths {
+            template <typename T>
+            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();
+
+                // TODO: init various things we'll need later
+                // - predecessors
+                computePredecessors();
+                // - Dijkstra (giving us SP-predecessors, SP-distances)
+                performDijkstra();
+                // - SP-successors
+                computeSPSuccessors();
+                // - shortest paths
+                initializeShortestPaths();
+            }
+
+            template <typename T>
+            ShortestPathsGenerator<T>::~ShortestPathsGenerator() {
+            }
+
+            template <typename T>
+            void ShortestPathsGenerator<T>::computePredecessors() {
+                graphPredecessors.resize(model->getNumberOfStates());
+
+                for (int i = 0; i < transitionMatrix.getRowCount(); 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);
+                    }
+                }
+            }
+
+            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)
+            }
+
+            template <typename T>
+            void ShortestPathsGenerator<T>::computeSPSuccessors() {
+                shortestPathSuccessors.resize(model->getNumberOfStates());
+
+                for (int i = 0; i < model->getNumberOfStates(); i++) {
+                    state_t predecessor = shortestPathPredecessors[i];
+                    shortestPathSuccessors[predecessor].push_back(i);
+                }
+            }
+
+            template <typename T>
+            void ShortestPathsGenerator<T>::initializeShortestPaths() {}
+        }
+    }
+}

src/utility/shortestPaths.h

@@ -1,15 +1,62 @@
-//
-// Created by Tom Janson on 15-1025.
-//
-
 #ifndef STORM_UTIL_SHORTESTPATHS_H_
 #define STORM_UTIL_SHORTESTPATHS_H_
 
+#include <vector>
+#include <boost/optional/optional.hpp>
+#include "src/models/sparse/Model.h"
+#include "src/storage/sparse/StateType.h"
+
+namespace storm {
+    namespace utility {
+        namespace shortestPaths {
+            typedef storm::storage::sparse::state_type state_t;
+            typedef std::vector<state_t> state_list_t;
+
+            template <typename T>
+            struct path {
+                boost::optional<state_t> tail;
+                unsigned int tail_k;
+                T distance;
+            };
+
+            template <typename T>
+            class ShortestPathsGenerator {
+            public:
+                // FIXME: this shared_ptr-passing business is probably a bad idea
+                ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> model);
+                ~ShortestPathsGenerator();
+
+            private:
+                //storm::models::sparse::Model<T>* model;
+                std::shared_ptr<storm::models::sparse::Model<T>> model;
+                storm::storage::SparseMatrix<T>  transitionMatrix;
+
+                std::vector<state_list_t> graphPredecessors;
+                std::vector<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;
 
+                /*!
+                 * Computes list of predecessors for all nodes.
+                 * Reachability is not considered; a predecessor is simply any node that has an edge leading to the
+                 * node in question.
+                 *
+                 * @param model The model whose transitions will be examined
+                 * @return A vector of predecessors for each node
+                 */
+                void computePredecessors();
 
-class shortestPathsUtil {
+                void performDijkstra();
+                void computeSPSuccessors();
+                void initializeShortestPaths();
 
-};
+            };
+        }
+    }
+}
 
 
 #endif //STORM_UTIL_SHORTESTPATHS_H_