diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 903ea1076..248e4a69b 100644 --- a/src/test/utility/GraphTest.cpp +++ b/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> model = storm::builder::ExplicitPrismModelBuilder().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 shortestPathsGenerator(model); + + // TODO: actually write tests here + + /* + std::queue nodeQueue; + for (uint_fast64_t initialNode : model->getInitialStates()) { + for (uint_fast64_t succ : shortestPathSuccessors[initialNode]) { + nodeQueue.push(succ); + } + storm::storage::sparse::path 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 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 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 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); -} \ No newline at end of file +} diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 0c778d55b..1dc1301e4 100644 --- a/src/utility/shortestPaths.cpp +++ b/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 + 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(); + + // 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 + ShortestPathsGenerator::~ShortestPathsGenerator() { + } + + template + void ShortestPathsGenerator::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 + 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) + } + + template + void ShortestPathsGenerator::computeSPSuccessors() { + shortestPathSuccessors.resize(model->getNumberOfStates()); + + for (int i = 0; i < model->getNumberOfStates(); i++) { + state_t predecessor = shortestPathPredecessors[i]; + shortestPathSuccessors[predecessor].push_back(i); + } + } + + template + void ShortestPathsGenerator::initializeShortestPaths() {} + } + } +} diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 28e9e7c16..1d31fd89f 100644 --- a/src/utility/shortestPaths.h +++ b/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 +#include +#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_list_t; + + template + struct path { + boost::optional tail; + unsigned int tail_k; + T distance; + }; + + template + class ShortestPathsGenerator { + public: + // FIXME: this shared_ptr-passing business is probably a bad idea + ShortestPathsGenerator(std::shared_ptr> model); + ~ShortestPathsGenerator(); + + private: + //storm::models::sparse::Model* model; + std::shared_ptr> model; + storm::storage::SparseMatrix transitionMatrix; + + std::vector graphPredecessors; + std::vector shortestPathPredecessors; + std::vector shortestPathSuccessors; + std::vector shortestPathDistances; + + std::vector>> shortestPaths; + std::vector>> 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_