From 2aec312fbda27cee173b3c4aea7c6756c5b270ae Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 7 Oct 2015 17:58:03 +0200 Subject: [PATCH 01/35] testcase-stub for kshortest added Former-commit-id: 215c5b73788c143bbd413dd55185c672fe6b8c4c [formerly 5598231acbf66f5220902832823efd57e6d15574] Former-commit-id: 6d51229aa17a09d0bbeb9ce47ddf096772d03d05 --- src/test/utility/GraphTest.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index dff3ccc53..903ea1076 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -263,3 +263,14 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); 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"); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + std::cout << model->getNumberOfStates() << std::endl; + + EXPECT_TRUE(false); +} \ No newline at end of file From 6d1608a14787e82058783daee4a51d3c4058933b Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 25 Oct 2015 17:38:10 +0100 Subject: [PATCH 02/35] Dijkstra fixed, maybe TODO: check; improve Things that aren't going well: - On the example graph BRP-16-2, all nodes have distance 1. I that possible?? - The initial states list themself as their own predecessor. That's bad, because it's simply false (unless there is a self-loop). Former-commit-id: 06f9a283064c17533f6d5cb4a0959aab0cf98005 [formerly e7e2385e0d335dfd2e4c4fb2c008028da6babef6] Former-commit-id: 350501183197c5c5baaad6ab14e87b28202ee76d --- src/storm/utility/graph.cpp | 49 +++++++++++++++++++++++++---------- src/storm/utility/graph.h | 3 ++- src/utility/shortestPaths.cpp | 5 ++++ src/utility/shortestPaths.h | 15 +++++++++++ 4 files changed, 57 insertions(+), 15 deletions(-) create mode 100644 src/utility/shortestPaths.cpp create mode 100644 src/utility/shortestPaths.h diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 7604c45af..694697c61 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -992,7 +992,8 @@ namespace storm { } - + + // There seems to be a lot of stuff wrong here. FIXME: Check whether it works now. -Tom template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, @@ -1016,26 +1017,43 @@ namespace storm { // As long as there is one reachable state, we need to consider it. while (!probabilityStateSet.empty()) { // Get the state with the least distance from the set and remove it. - std::pair probabilityStatePair = probabilityStateSet.erase(probabilityStateSet.begin()); - + // FIXME? is this correct? this used to take the second element!! + std::pair probabilityStatePair = *(probabilityStateSet.begin()); + probabilityStateSet.erase(probabilityStateSet.begin()); + + uint_fast64_t currentNode = probabilityStatePair.second; + // Now check the new distances for all successors of the current state. - typename storm::storage::SparseMatrix::Rows row = transitions.getRow(probabilityStatePair.second); + typename storm::storage::SparseMatrix::const_rows row = transitions.getRowGroup(currentNode); for (auto const& transition : row) { + uint_fast64_t targetNode = transition.getColumn(); + // Only follow the transition if it lies within the filtered states. - if (filterStates != nullptr && filterStates->get(transition.first)) { + // -- shouldn't "no filter" (nullptr) mean that all nodes are checked? - Tom FIXME + if (filterStates == nullptr || filterStates->get(targetNode)) { + // Calculate the distance we achieve when we take the path to the successor via the current state. - T newDistance = probabilityStatePair.first; + // FIXME: this should be multiplied with the distance to the current node, right? + //T newDistance = probabilityStatePair.first; + T edgeProbability = probabilityStatePair.first; + T newDistance = probabilities[currentNode] * edgeProbability; + + // DEBUG + if (newDistance != 1) { + std::cout << "yay" << std::endl; + } + // We found a cheaper way to get to the target state of the transition. - if (newDistance > probabilities[transition.first]) { + if (newDistance > probabilities[targetNode]) { // Remove the old distance. - if (probabilities[transition.first] != noPredecessorValue) { - probabilityStateSet.erase(std::make_pair(probabilities[transition.first], transition.first)); + if (probabilities[targetNode] != noPredecessorValue) { + probabilityStateSet.erase(std::make_pair(probabilities[targetNode], targetNode)); } // Set and add the new distance. - probabilities[transition.first] = newDistance; - predecessors[transition.first] = probabilityStatePair.second; - probabilityStateSet.insert(std::make_pair(newDistance, transition.first)); + probabilities[targetNode] = newDistance; + predecessors[targetNode] = currentNode; + probabilityStateSet.insert(std::make_pair(newDistance, targetNode)); } } } @@ -1179,8 +1197,11 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; - + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + + template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, storm::storage::BitVector const* filterStates); + + // Instantiations for storm::RationalNumber. #ifdef STORM_HAVE_CARL template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 13100e3ac..770af42d4 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -544,13 +544,14 @@ namespace storm { * @param transitions The transitions wrt to which to compute the most probable paths. * @param startingStates The starting states of the Dijkstra search. * @param filterStates A set of states that must not be left on any path. + * @return A pair consisting of a vector of distances and a vector of shortest path predecessors */ template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, storm::storage::BitVector const* filterStates = nullptr); - + } // namespace graph } // namespace utility } // namespace storm diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp new file mode 100644 index 000000000..0c778d55b --- /dev/null +++ b/src/utility/shortestPaths.cpp @@ -0,0 +1,5 @@ +// +// Created by Tom Janson on 15-1025. +// + +#include "shortestPaths.h" diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h new file mode 100644 index 000000000..28e9e7c16 --- /dev/null +++ b/src/utility/shortestPaths.h @@ -0,0 +1,15 @@ +// +// Created by Tom Janson on 15-1025. +// + +#ifndef STORM_UTIL_SHORTESTPATHS_H_ +#define STORM_UTIL_SHORTESTPATHS_H_ + + + +class shortestPathsUtil { + +}; + + +#endif //STORM_UTIL_SHORTESTPATHS_H_ From 010f0ca988eef1c7bf35b299b99e115b6274e584 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sun, 25 Oct 2015 17:44:33 +0100 Subject: [PATCH 03/35] shortest paths generator skeleton Former-commit-id: c37fdbbec8338686863ab532bda29e91cdc6a239 [formerly 23dba537c7c776a3d74387c916c647b5fc1474fb] Former-commit-id: 6eb54e64add1342a8bf1b6b939e4c7d46c67ad39 --- src/test/utility/GraphTest.cpp | 77 ++++++++++++++++++++++++++++++++-- src/utility/shortestPaths.cpp | 67 +++++++++++++++++++++++++++-- src/utility/shortestPaths.h | 59 +++++++++++++++++++++++--- 3 files changed, 189 insertions(+), 14 deletions(-) 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_ From fd3c59e86e05ea953048620abccc237d7e599db5 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Mon, 26 Oct 2015 23:07:53 +0100 Subject: [PATCH 04/35] 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: 33b2be8067446d3bad0ff152116f19c4db47f0c3 [formerly 0d5c507568b1ced0d7e45fba0572878bf248bb24] Former-commit-id: b35fc0bee302bf2b1894f8c1cd6174cf2c74a6d6 --- src/utility/shortestPaths.cpp | 64 +++++++++++++++++++++++++++-------- src/utility/shortestPaths.h | 11 +++--- 2 files changed, 55 insertions(+), 20 deletions(-) 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; From 519b46f171f96c436fbba9b9439b2191729b4afd Mon Sep 17 00:00:00 2001 From: tomjanson Date: Tue, 27 Oct 2015 01:32:58 +0100 Subject: [PATCH 05/35] path construction thanks to new Dijkstra, the (1-)shortest paths construction code is simpler Former-commit-id: ec2ef461b83735cc743d9060f9233de320723303 [formerly 5757d66bc53cc838eecf93bba3a596a9c6dfcad4] Former-commit-id: 00f3d35a38396d3fdd5641d60d4ea2d70c5f17ca --- src/utility/shortestPaths.cpp | 38 ++++++++++++++++++++++++++++++----- src/utility/shortestPaths.h | 27 ++++++++++++++++++++----- 2 files changed, 55 insertions(+), 10 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index c1ef831f8..f2170bc9f 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,3 +1,4 @@ +#include #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 - void ShortestPathsGenerator::initializeShortestPaths() {} + void ShortestPathsGenerator::initializeShortestPaths() { + kShortestPaths.resize(numStates); + candidatePaths.resize(numStates); + + // BFS in Dijkstra-SP order + std::queue 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 { + shortestPathPredecessors[currentNode], + 1, + shortestPathDistances[currentNode] + }); + } + } } } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index d2d85cb62..31733c9d3 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -12,10 +12,27 @@ namespace storm { typedef storm::storage::sparse::state_type state_t; typedef std::vector 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 - struct path { - boost::optional tail; - unsigned int tail_k; + struct Path { + boost::optional pathPredecessor; + unsigned int predecessorK; T distance; }; @@ -37,8 +54,8 @@ namespace storm { std::vector shortestPathSuccessors; std::vector shortestPathDistances; - std::vector>> shortestPaths; - std::vector>> shortestPathCandidates; + std::vector>> kShortestPaths; + std::vector>> candidatePaths; /*! * Computes list of predecessors for all nodes. From d6c6b9b8d51761781b7fdb07172f2cfa486322f7 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Tue, 27 Oct 2015 02:14:36 +0100 Subject: [PATCH 06/35] path printing print path ammendment: off-by-one Former-commit-id: cdeb58711b7f062ee274b2fadb0427b3a82a5087 [formerly abd5a8777f8feb17877b085be0ad8e2e756a5c68] Former-commit-id: 506ce7fc90d65dfe1ab2c429621678be0b901c24 --- src/utility/shortestPaths.cpp | 20 ++++++++++++++++++++ src/utility/shortestPaths.h | 8 ++++++-- 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index f2170bc9f..2092bf7a5 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -21,6 +21,8 @@ namespace storm { // constructs the recursive shortest path representations initializeShortestPaths(); + + printKShortestPath(400, 1); // DEBUG } template @@ -121,6 +123,24 @@ namespace storm { }); } } + + template + void ShortestPathsGenerator::printKShortestPath(state_t targetNode, int k, bool head) { + // note the index shift! risk of off-by-one + Path p = kShortestPaths[targetNode][k - 1]; + + if (head) { + std::cout << "Path (reversed), dist (prob)=" << p.distance << ": ["; + } + + std::cout << " " << targetNode; + + if (p.predecessorNode) { + printKShortestPath(p.predecessorNode.get(), p.predecessorK, false); + } else { + std::cout << " ]" << std::endl; + } + } } } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 31733c9d3..91f5c7843 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -20,7 +20,7 @@ namespace storm { * * s ~~k-shortest path~~> u --> t * - * This struct stores u (`pathPredecessor`) and k (`predecessorK`). + * This struct stores u (`predecessorNode`) and k (`predecessorK`). * * t is implied by this struct's location: It is stored in the * k-shortest paths list associated with t. @@ -31,7 +31,7 @@ namespace storm { */ template struct Path { - boost::optional pathPredecessor; + boost::optional predecessorNode; unsigned int predecessorK; T distance; }; @@ -71,6 +71,10 @@ namespace storm { void computeSPSuccessors(); void initializeShortestPaths(); + /* + * Recurses over the path and prints the nodes. Intended for debugging. + */ + void printKShortestPath(state_t targetNode, int k, bool head=true); }; } } From 38d22093a3cfbcff79dd2c32901f1693ee52edad Mon Sep 17 00:00:00 2001 From: tomjanson Date: Tue, 27 Oct 2015 18:11:59 +0100 Subject: [PATCH 07/35] documentation / cleanup Former-commit-id: e7798a5669159ff2e050d8125382e4df404ae981 [formerly 43dd865fbc66eb07365643907c2824f6db12762a] Former-commit-id: 6fb69a017c05076a7e5ded14a7f2351226e0cc27 --- src/test/utility/GraphTest.cpp | 65 +--------------------------------- src/utility/shortestPaths.cpp | 13 ++++--- src/utility/shortestPaths.h | 28 +++++++++++---- 3 files changed, 28 insertions(+), 78 deletions(-) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 248e4a69b..7b1871d2d 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -278,68 +278,5 @@ TEST(GraphTest, kshortest) { // 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(); - - 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 2092bf7a5..afb849792 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -21,8 +21,6 @@ namespace storm { // constructs the recursive shortest path representations initializeShortestPaths(); - - printKShortestPath(400, 1); // DEBUG } template @@ -31,11 +29,13 @@ namespace storm { template void ShortestPathsGenerator::computePredecessors() { - graphPredecessors.resize(numStates); + auto rowCount = transitionMatrix.getRowCount(); + assert(numStates == rowCount); - assert(numStates == transitionMatrix.getRowCount()); - for (state_t i = 0; i < numStates; i++) { - for (auto transition : transitionMatrix.getRowGroup(i)) { + graphPredecessors.resize(rowCount); + + for (state_t i = 0; i < rowCount; i++) { + for (auto const& transition : transitionMatrix.getRowGroup(i)) { graphPredecessors[transition.getColumn()].push_back(i); } } @@ -93,7 +93,6 @@ namespace storm { template void ShortestPathsGenerator::initializeShortestPaths() { kShortestPaths.resize(numStates); - candidatePaths.resize(numStates); // BFS in Dijkstra-SP order std::queue bfsQueue; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 91f5c7843..42bb2edee 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -44,7 +44,6 @@ namespace storm { ~ShortestPathsGenerator(); private: - //storm::models::sparse::Model* model; std::shared_ptr> model; storm::storage::SparseMatrix transitionMatrix; state_t numStates; @@ -59,19 +58,34 @@ namespace storm { /*! * 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 + * Reachability is not considered; a predecessor is simply any node that has an edge leading to the node in question. + * Requires `transitionMatrix`. + * Modifies `graphPredecessors`. */ void computePredecessors(); + /*! + * Computes shortest path distances and predecessors. + * Requires `model`, `numStates`, `transitionMatrix`. + * Modifies `shortestPathPredecessors` and `shortestPathDistances`. + */ void performDijkstra(); + + /*! + * Computes list of shortest path successor nodes from predecessor list. + * Requires `shortestPathPredecessors`, `numStates`. + * Modifies `shortestPathSuccessors`. + */ void computeSPSuccessors(); + + /*! + * Constructs and stores the implicit shortest path representations (see `Path`) for the (1-)shortest paths. + * Requires `shortestPathPredecessors`, `shortestPathDistances`, `model`, `numStates`. + * Modifies `kShortestPaths`. + */ void initializeShortestPaths(); - /* + /*! * Recurses over the path and prints the nodes. Intended for debugging. */ void printKShortestPath(state_t targetNode, int k, bool head=true); From df195d85f68974398b8411304430bc9b0a02a660 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Tue, 27 Oct 2015 23:20:03 +0100 Subject: [PATCH 08/35] REA fully implemented; needs testing Former-commit-id: 9795a24835822be49225e24cf0a680a8a54628bd [formerly fc732962dda71a65ab2585463ea765725aa13cb9] Former-commit-id: 0ae2abacd112f2a4ce1f197ac3f1fc9742346f78 --- src/test/utility/GraphTest.cpp | 6 +++ src/utility/shortestPaths.cpp | 94 ++++++++++++++++++++++++++++++++-- src/utility/shortestPaths.h | 52 +++++++++++++++++-- 3 files changed, 145 insertions(+), 7 deletions(-) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 7b1871d2d..0d43c02ad 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -276,6 +276,12 @@ TEST(GraphTest, kshortest) { storm::utility::shortestPaths::ShortestPathsGenerator shortestPathsGenerator(model); + storm::storage::sparse::state_type exampleState = 50; + + for (int i = 1; i < 20; i++) { + auto foo = shortestPathsGenerator.getKShortest(exampleState, i); + } + // TODO: actually write tests here EXPECT_TRUE(false); diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index afb849792..9a51e7c7c 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,7 +1,7 @@ #include +#include #include "shortestPaths.h" #include "graph.h" -#include "constants.h" namespace storm { namespace utility { @@ -21,6 +21,8 @@ namespace storm { // constructs the recursive shortest path representations initializeShortestPaths(); + + candidatePaths.resize(numStates); } template @@ -53,7 +55,7 @@ namespace storm { // set serves as priority queue with unique membership // default comparison on pair actually works fine if distance is the first entry - std::set> dijkstraQueue; + std::set, std::greater_equal>> dijkstraQueue; for (state_t initialState : model->getInitialStates()) { shortestPathDistances[initialState] = zeroDistance; @@ -124,7 +126,93 @@ namespace storm { } template - void ShortestPathsGenerator::printKShortestPath(state_t targetNode, int k, bool head) { + void ShortestPathsGenerator::computeNextPath(state_t node, unsigned long k) { + assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist + + if (k == 2) { + Path shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-| + + for (state_t predecessor : graphPredecessors[node]) { + // add shortest paths to predecessors plus edge to current node + Path pathToPredecessorPlusEdge = { + boost::optional(predecessor), + 1, + shortestPathDistances[predecessor] * getEdgeDistance(predecessor, node) + }; + candidatePaths[node].insert(pathToPredecessorPlusEdge); + + // ... but not the actual shortest path + auto it = find(candidatePaths[node].begin(), candidatePaths[node].end(), shortestPathToNode); + if (it != candidatePaths[node].end()) { + candidatePaths[node].erase(it); + } + } + } + + if (k > 2 || !isInitialState(node)) { + // the (k-1)th shortest path (i.e., one better than the one we want to compute) + Path previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN + + // the predecessor node on that path + state_t predecessor = previousShortestPath.predecessorNode.get(); + // the path to that predecessor was the `tailK`-shortest + unsigned long tailK = previousShortestPath.predecessorK; + + // i.e. source ~~tailK-shortest path~~> predecessor --> node + + // compute one-worse-shortest path to the predecessor (if it hasn't yet been computed) + if (kShortestPaths[predecessor].size() < tailK + 1) { + // TODO: investigate recursion depth and possible iterative alternative + computeNextPath(predecessor, tailK + 1); + } + + if (kShortestPaths[predecessor].size() >= tailK + 1) { + // take that path, add an edge to the current node; that's a candidate + Path pathToPredecessorPlusEdge = { + boost::optional(predecessor), + tailK + 1, + kShortestPaths[predecessor][tailK + 1 - 1].distance * getEdgeDistance(predecessor, node) + }; + candidatePaths[node].insert(pathToPredecessorPlusEdge); + } + // else there was no path; TODO: does this need handling? + } + + if (!candidatePaths[node].empty()) { + Path minDistanceCandidate = *(candidatePaths[node].begin()); + for (auto path : candidatePaths[node]) { + if (path.distance > minDistanceCandidate.distance) { + minDistanceCandidate = path; + } + } + + candidatePaths[node].erase(find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate)); + kShortestPaths[node].push_back(minDistanceCandidate); + } + } + + template + Path ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { + unsigned long alreadyComputedK = kShortestPaths[node].size(); + + for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { + computeNextPath(node, nextK); + if (kShortestPaths[node].size() < nextK) { + break; + } + } + + if (kShortestPaths[node].size() >= k) { + printKShortestPath(node, k); // DEBUG + } else { + std::cout << "No other path exists!" << std::endl; + } + + return kShortestPaths[node][k - 1]; + } + + template + void ShortestPathsGenerator::printKShortestPath(state_t targetNode, unsigned long k, bool head) { // note the index shift! risk of off-by-one Path p = kShortestPaths[targetNode][k - 1]; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 42bb2edee..6aba88434 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -5,6 +5,7 @@ #include #include "src/models/sparse/Model.h" #include "src/storage/sparse/StateType.h" +#include "constants.h" namespace storm { namespace utility { @@ -26,23 +27,44 @@ namespace storm { * 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. + * up the path's tail stored as the k-th entry [1] of the + * predecessor's shortest paths list. + * + * [1] oh, actually, the `k-1`th entry due to 0-based indexing! */ template struct Path { boost::optional predecessorNode; - unsigned int predecessorK; + unsigned long predecessorK; T distance; + + // FIXME: uhh.. is this okay for set? just some arbitrary order + bool operator<(const Path& rhs) const { + if (predecessorNode != rhs.predecessorNode) { + return predecessorNode < rhs.predecessorNode; + } + return predecessorK < predecessorK; + } + + bool operator==(const Path& rhs) const { + return (predecessorNode == rhs.predecessorNode) && (predecessorK == rhs.predecessorK); + } }; + // ------------------------------------------------------------------------------------------------------- + template class ShortestPathsGenerator { public: // FIXME: this shared_ptr-passing business is probably a bad idea ShortestPathsGenerator(std::shared_ptr> model); + ~ShortestPathsGenerator(); + // TODO: think about suitable output format + Path getKShortest(state_t node, unsigned long k); + + private: std::shared_ptr> model; storm::storage::SparseMatrix transitionMatrix; @@ -85,10 +107,32 @@ namespace storm { */ void initializeShortestPaths(); + /*! + * Main step of REA algorithm. TODO: Document further. + */ + void computeNextPath(state_t node, unsigned long k); + /*! * Recurses over the path and prints the nodes. Intended for debugging. */ - void printKShortestPath(state_t targetNode, int k, bool head=true); + void printKShortestPath(state_t targetNode, unsigned long k, bool head=true); + + + // --- tiny helper fcts --- + bool isInitialState(state_t node) { + auto initialStates = model->getInitialStates(); + return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); + } + + T getEdgeDistance(state_t tailNode, state_t headNode) { + for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) { + if (transition.getColumn() == headNode) { + return transition.getValue(); + } + } + return storm::utility::zero(); + } + // ----------------------- }; } } From 140597fb9060546f7652c53adbece0ad9afa4512 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Wed, 28 Oct 2015 15:34:30 +0100 Subject: [PATCH 09/35] interactive debug in test Former-commit-id: 161afac16e738af2f0f076f6d3518b989e9bb35c [formerly 17962bf2008e1546a56a72cfd3afed20f1019650] Former-commit-id: 53dc4819cfedcbdd169a593b8bbae3f22cc1a97b --- src/test/utility/GraphTest.cpp | 17 ++++++++++++++--- src/utility/shortestPaths.cpp | 23 +++++++++++++---------- src/utility/shortestPaths.h | 11 ++++++++++- 3 files changed, 37 insertions(+), 14 deletions(-) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 0d43c02ad..98359a364 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -268,18 +268,29 @@ TEST(GraphTest, ExplicitProb01MinMax) { TEST(GraphTest, kshortest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + //storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/../examples/dtmc/die/die.pm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); model->printModelInformationToStream(std::cout); + std::cout << "Initializing ShortestPathsGenerator ..." << std::endl; storm::utility::shortestPaths::ShortestPathsGenerator shortestPathsGenerator(model); - storm::storage::sparse::state_type exampleState = 50; + unsigned int k; + storm::storage::sparse::state_type state; - for (int i = 1; i < 20; i++) { - auto foo = shortestPathsGenerator.getKShortest(exampleState, i); + while (true) { + std::cout << std::endl; + std::cout << "Enter state (note: 0-based index) ... "; + std::cin >> state; + + std::cout << "Enter k ... "; + std::cin >> k; + + std::cout << "Computing " << k << "-shortest path to state " << state << std::endl; + shortestPathsGenerator.getKShortest(state, k); } // TODO: actually write tests here diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 9a51e7c7c..cb053b5e5 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -55,7 +55,7 @@ namespace storm { // set serves as priority queue with unique membership // default comparison on pair actually works fine if distance is the first entry - std::set, std::greater_equal>> dijkstraQueue; + std::set, std::greater>> dijkstraQueue; for (state_t initialState : model->getInitialStates()) { shortestPathDistances[initialState] = zeroDistance; @@ -192,23 +192,26 @@ namespace storm { } template - Path ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { + void ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { unsigned long alreadyComputedK = kShortestPaths[node].size(); +// std::cout << std::endl << "--> DEBUG: Dijkstra SP to " << node << ":" << std::endl; +// printKShortestPath(node, 1); +// std::cout << "---------" << std::endl; + for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { computeNextPath(node, nextK); if (kShortestPaths[node].size() < nextK) { - break; + std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; + printKShortestPath(node, nextK - 1); + std::cout << "---------" << "No other path exists!" << std::endl; + return; } } - if (kShortestPaths[node].size() >= k) { - printKShortestPath(node, k); // DEBUG - } else { - std::cout << "No other path exists!" << std::endl; - } - - return kShortestPaths[node][k - 1]; + std::cout << std::endl << "--> DEBUG: Finished. " << k << "-shortest path:" << std::endl; + printKShortestPath(node, k); + std::cout << "---------" << std::endl; } template diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 6aba88434..3b65ce22a 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -7,6 +7,15 @@ #include "src/storage/sparse/StateType.h" #include "constants.h" +/* + * TODO: + * - take care of self-loops of target states + * - implement target group + * - think about how to get paths with new nodes, rather than different + * paths over the same set of states (which happens often) + */ + + namespace storm { namespace utility { namespace shortestPaths { @@ -62,7 +71,7 @@ namespace storm { ~ShortestPathsGenerator(); // TODO: think about suitable output format - Path getKShortest(state_t node, unsigned long k); + void getKShortest(state_t node, unsigned long k); private: From d8f2eec9af46868ad1dba32665acad328fd602a3 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sat, 7 Nov 2015 17:32:02 +0100 Subject: [PATCH 10/35] actual test for single-target non-disjoint KSP Former-commit-id: abb27b9078f106e2e0f1062ffcd3fc2d092c7f67 [formerly 8492e75c075d5a4f4655296d9c30867d6462dbf0] Former-commit-id: c60c8298268613ba635a27ae27b6415a2dbb5a97 --- src/test/utility/GraphTest.cpp | 32 +++++++++++++------------------- src/utility/shortestPaths.cpp | 9 +++------ src/utility/shortestPaths.h | 4 +++- 3 files changed, 19 insertions(+), 26 deletions(-) diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 98359a364..026f850e4 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -268,32 +268,26 @@ TEST(GraphTest, ExplicitProb01MinMax) { TEST(GraphTest, kshortest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); - //storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/../examples/dtmc/die/die.pm"); std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); - model->printModelInformationToStream(std::cout); + storm::storage::sparse::state_type testState = 300; - std::cout << "Initializing ShortestPathsGenerator ..." << std::endl; storm::utility::shortestPaths::ShortestPathsGenerator shortestPathsGenerator(model); - unsigned int k; - storm::storage::sparse::state_type state; + // the 1-shortest path is computed as a preprocessing step via Dijkstra; + // since there were some bugs here in the past, let's test it separately + double dijkstraSPDistance = shortestPathsGenerator.getKShortest(testState, 1); + std::cout << "Res: " << dijkstraSPDistance << std::endl; + //EXPECT_NEAR(0.0158593, dijkstraSPDistance, 0.0000001); + EXPECT_DOUBLE_EQ(0.015859334652581887, dijkstraSPDistance); - while (true) { - std::cout << std::endl; - std::cout << "Enter state (note: 0-based index) ... "; - std::cin >> state; + // main test + double kSPDistance1 = shortestPathsGenerator.getKShortest(testState, 100); + EXPECT_DOUBLE_EQ(1.5231305000339649e-06, kSPDistance1); - std::cout << "Enter k ... "; - std::cin >> k; - - std::cout << "Computing " << k << "-shortest path to state " << state << std::endl; - shortestPathsGenerator.getKShortest(state, k); - } - - // TODO: actually write tests here - - EXPECT_TRUE(false); + // let's test again to ensure re-entry is no problem + double kSPDistance2 = shortestPathsGenerator.getKShortest(testState, 500); + EXPECT_DOUBLE_EQ(3.0462610000679282e-08, kSPDistance2); } \ No newline at end of file diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index cb053b5e5..8e5aef6b5 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -192,26 +192,23 @@ namespace storm { } template - void ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { + T ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { unsigned long alreadyComputedK = kShortestPaths[node].size(); -// std::cout << std::endl << "--> DEBUG: Dijkstra SP to " << node << ":" << std::endl; -// printKShortestPath(node, 1); -// std::cout << "---------" << std::endl; - for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { computeNextPath(node, nextK); if (kShortestPaths[node].size() < nextK) { std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; printKShortestPath(node, nextK - 1); std::cout << "---------" << "No other path exists!" << std::endl; - return; + return storm::utility::zero(); // TODO: throw exception or something } } std::cout << std::endl << "--> DEBUG: Finished. " << k << "-shortest path:" << std::endl; printKShortestPath(node, k); std::cout << "---------" << std::endl; + return kShortestPaths[node][k - 1].distance; } template diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 3b65ce22a..9935f3945 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -71,7 +71,9 @@ namespace storm { ~ShortestPathsGenerator(); // TODO: think about suitable output format - void getKShortest(state_t node, unsigned long k); + T getKShortest(state_t node, unsigned long k); + + // TODO: allow three kinds of target arguments: single state, BitVector, Label private: From 62fcf7e0a57b65125609727865051cb55c11348b Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sat, 7 Nov 2015 18:28:59 +0100 Subject: [PATCH 11/35] thoughts about loops & target groups Former-commit-id: c9b4b3697d8d70e4ae115941990cdaebc5a8cb1c [formerly 8609d79a43ccb97d6c6bc9bbddb9ac122fc27da5] Former-commit-id: dea158308bb2eec82549a84af79f6747103e9548 --- src/utility/shortestPaths.h | 4 +++ src/utility/shortestPaths.md | 50 ++++++++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+) create mode 100644 src/utility/shortestPaths.md diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 9935f3945..546afaec4 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -7,6 +7,10 @@ #include "src/storage/sparse/StateType.h" #include "constants.h" +// NOTE: You'll (eventually) find the usual API documentation below; +// for more information about the purpose, design decisions, +// etc., you may consult `shortestPath.md`. - Tom + /* * TODO: * - take care of self-loops of target states diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md new file mode 100644 index 000000000..6f1042ae4 --- /dev/null +++ b/src/utility/shortestPaths.md @@ -0,0 +1,50 @@ +# k-shortest Path Generator +[This is a collection of random notes for now, to help me remember +the design decisions and the rationale behind them.] + +## Differences from REA algorithm +This class closely follows the Jimenez-Marzal REA algorithm. +However, there are some notable deviations: + +### Target groups +Firstly, instead of a single target state, a group of target states is +considered. It is clear that this can achieved by removing all outgoing +transitions (other than self-loops, but this is moot due to not allowing +non-minimal paths -- see below) and instead introducing edges to a new sink +state that serves as a meta-target. + +In terms of implementation, there are two possible routes (that I can think +of): + + - Simply (but destructively) modifying the precomputation results (in + particular the predecessor list). This is straightforward and has no + performance penalty, but implies that each instance of the SP-Generator + is restricted to a single group of targets. + (Whereas the original algorithm can compute the KSPs to several targets, + reusing all partial results.) + - Keeping the computation "clean" so that all results remain universally + valid (and thus reusable for other targets) by means of reversibly + "overlaying" the graph modifications. + +It is not clear if there will ever be a need for changing targets. While +the overlay option is alluring, in the spirit of YAGNI, I choose the +destructive, simple route. + +### Minimality of paths +Secondly, we define shortest paths as "minimal" shortest paths in the +following sense: The path may only visit the target state once (at the +end). In other words, no KSP may be a prefix of another. +This in particular forbids shortest path progressions such as these: + + 1-SP: 1 2 3 + 2-SP: 1 2 3 3 + 3-SP: 1 2 3 3 3 + ... + +This is a common feature if the target state is a sink; but we are not +interested in such paths. + +(In fact, ideally we'd like to see paths whose node-intersection with all +shorter paths is non-empty (which is an even stronger statement than +loop-free-ness of paths), because we want to take a union of those node +sets. But that's a different matter.) From b89d3f289a47c98120ebb8f44db39d9a4ba20555 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sat, 7 Nov 2015 19:49:33 +0100 Subject: [PATCH 12/35] group targets & minimal paths Note that this is a major, API-breaking change. Also bunched into this commit: - rename namespace `shortestPaths` to `ksp` - omit unneeded namespace qualifiers - move tests from `GraphTest` to `KSPTest` and wrote more - path representation explanation in .md file Former-commit-id: f395c3df40012b5ef7775aad27668beefc21a7e8 [formerly 7fa07d1c8fc45fdf0f0aa26795836799ee7ed8bd] Former-commit-id: f50dd3ce7c5d4ed2651e6852e1bda475d423a413 --- src/test/utility/GraphTest.cpp | 27 ----- src/utility/shortestPaths.cpp | 150 ++++++++++++++++++++-------- src/utility/shortestPaths.h | 79 +++++++-------- src/utility/shortestPaths.md | 42 +++++++- test/functional/utility/KSPTest.cpp | 69 +++++++++++++ 5 files changed, 254 insertions(+), 113 deletions(-) create mode 100644 test/functional/utility/KSPTest.cpp diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 026f850e4..76e17299c 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -264,30 +264,3 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); } - - -TEST(GraphTest, kshortest) { - 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::Dtmc); - - storm::storage::sparse::state_type testState = 300; - - storm::utility::shortestPaths::ShortestPathsGenerator shortestPathsGenerator(model); - - // the 1-shortest path is computed as a preprocessing step via Dijkstra; - // since there were some bugs here in the past, let's test it separately - double dijkstraSPDistance = shortestPathsGenerator.getKShortest(testState, 1); - std::cout << "Res: " << dijkstraSPDistance << std::endl; - //EXPECT_NEAR(0.0158593, dijkstraSPDistance, 0.0000001); - EXPECT_DOUBLE_EQ(0.015859334652581887, dijkstraSPDistance); - - // main test - double kSPDistance1 = shortestPathsGenerator.getKShortest(testState, 100); - EXPECT_DOUBLE_EQ(1.5231305000339649e-06, kSPDistance1); - - // let's test again to ensure re-entry is no problem - double kSPDistance2 = shortestPathsGenerator.getKShortest(testState, 500); - EXPECT_DOUBLE_EQ(3.0462610000679282e-08, kSPDistance2); -} \ No newline at end of file diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 8e5aef6b5..1b60717d7 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -5,12 +5,16 @@ namespace storm { namespace utility { - namespace shortestPaths { + namespace ksp { template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model) : model(model) { + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, + state_list_t const& targets) : model(model), targets(targets) { // FIXME: does this create a copy? I don't need one, so I should avoid that transitionMatrix = model->getTransitionMatrix(); - numStates = model->getNumberOfStates(); + numStates = model->getNumberOfStates() + 1; // one more for meta-target + + metaTarget = numStates - 1; // first unused state number + targetSet = std::unordered_set(targets.begin(), targets.end()); computePredecessors(); @@ -25,22 +29,60 @@ namespace storm { candidatePaths.resize(numStates); } + // several alternative ways to specify the targets are provided, + // each converts the targets and delegates to the ctor above + // I admit it's kind of ugly, but actually pretty convenient (and I've wanted to try C++11 delegation) + template + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, + state_t singleTarget) : ShortestPathsGenerator(model, std::vector{singleTarget}) {} + + template + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, + storage::BitVector const& targetBV) : ShortestPathsGenerator(model, bitvectorToList(targetBV)) {} + template - ShortestPathsGenerator::~ShortestPathsGenerator() { + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, + std::string const& targetLabel) : ShortestPathsGenerator(model, bitvectorToList(model->getStates(targetLabel))) {} + + template + T ShortestPathsGenerator::computeKSP(unsigned long k) { + unsigned long alreadyComputedK = kShortestPaths[metaTarget].size(); + + for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { + computeNextPath(metaTarget, nextK); + if (kShortestPaths[metaTarget].size() < nextK) { + std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; + printKShortestPath(metaTarget, nextK - 1); + std::cout << "---------" << "No other path exists!" << std::endl; + return utility::zero(); // TODO: throw exception or something + } + } + + //std::cout << std::endl << "--> DEBUG: Finished. " << k << "-shortest path:" << std::endl; + //printKShortestPath(metaTarget, k); + //std::cout << "---------" << std::endl; + return kShortestPaths[metaTarget][k - 1].distance; } template void ShortestPathsGenerator::computePredecessors() { - auto rowCount = transitionMatrix.getRowCount(); - assert(numStates == rowCount); + assert(numStates - 1 == transitionMatrix.getRowCount()); - graphPredecessors.resize(rowCount); + // one more for meta-target + graphPredecessors.resize(numStates); - for (state_t i = 0; i < rowCount; i++) { + for (state_t i = 0; i < numStates - 1; i++) { for (auto const& transition : transitionMatrix.getRowGroup(i)) { - graphPredecessors[transition.getColumn()].push_back(i); + // to avoid non-minimal paths, the target states are + // *not* predecessors of any state but the meta-target + if (std::find(targets.begin(), targets.end(), i) == targets.end()) { + graphPredecessors[transition.getColumn()].push_back(i); + } } } + + // meta-target has exactly the target states as predecessors + graphPredecessors[metaTarget] = targets; } template @@ -48,8 +90,8 @@ namespace storm { // 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(); + T inftyDistance = utility::zero(); + T zeroDistance = utility::one(); shortestPathDistances.resize(numStates, inftyDistance); shortestPathPredecessors.resize(numStates, boost::optional()); @@ -66,16 +108,28 @@ namespace storm { 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); + if (targetSet.count(currentNode) == 0) { + // non-target node, treated normally + 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); + } } + } else { + // target node has only "virtual edge" (with prob 1) to meta-target + // no multiplication necessary + T alternateDistance = shortestPathDistances[currentNode]; + if (alternateDistance > shortestPathDistances[metaTarget]) { + shortestPathDistances[metaTarget] = alternateDistance; + shortestPathPredecessors[metaTarget] = boost::optional(currentNode); + } + // no need to enqueue meta-target } } } @@ -125,6 +179,30 @@ namespace storm { } } + template + T ShortestPathsGenerator::getEdgeDistance(state_t tailNode, state_t headNode) const { + // just to be clear, head is where the arrow points (obviously) + if (headNode != metaTarget) { + // edge is "normal", not to meta-target + + for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) { + if (transition.getColumn() == headNode) { + return transition.getValue(); + } + } + + // there is no such edge + // let's disallow that for now, because I'm not expecting it to happen + assert(false); + return utility::zero(); + } else { + // edge must be "virtual edge" from target state to meta-target + assert(targetSet.count(tailNode) == 1); + return utility::one(); + } + } + + template void ShortestPathsGenerator::computeNextPath(state_t node, unsigned long k) { assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist @@ -142,7 +220,7 @@ namespace storm { candidatePaths[node].insert(pathToPredecessorPlusEdge); // ... but not the actual shortest path - auto it = find(candidatePaths[node].begin(), candidatePaths[node].end(), shortestPathToNode); + auto it = std::find(candidatePaths[node].begin(), candidatePaths[node].end(), shortestPathToNode); if (it != candidatePaths[node].end()) { candidatePaths[node].erase(it); } @@ -186,38 +264,22 @@ namespace storm { } } - candidatePaths[node].erase(find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate)); + candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate)); kShortestPaths[node].push_back(minDistanceCandidate); } } template - T ShortestPathsGenerator::getKShortest(state_t node, unsigned long k) { - unsigned long alreadyComputedK = kShortestPaths[node].size(); - - for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { - computeNextPath(node, nextK); - if (kShortestPaths[node].size() < nextK) { - std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; - printKShortestPath(node, nextK - 1); - std::cout << "---------" << "No other path exists!" << std::endl; - return storm::utility::zero(); // TODO: throw exception or something - } - } - - std::cout << std::endl << "--> DEBUG: Finished. " << k << "-shortest path:" << std::endl; - printKShortestPath(node, k); - std::cout << "---------" << std::endl; - return kShortestPaths[node][k - 1].distance; - } - - template - void ShortestPathsGenerator::printKShortestPath(state_t targetNode, unsigned long k, bool head) { + void ShortestPathsGenerator::printKShortestPath(state_t targetNode, unsigned long k, bool head) const { // note the index shift! risk of off-by-one Path p = kShortestPaths[targetNode][k - 1]; if (head) { - std::cout << "Path (reversed), dist (prob)=" << p.distance << ": ["; + std::cout << "Path (reversed"; + if (targetNode == metaTarget) { + std::cout << ", w/ meta-target"; + } + std::cout <<"), dist (prob)=" << p.distance << ": ["; } std::cout << " " << targetNode; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 546afaec4..742cc2eec 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/models/sparse/Model.h" #include "src/storage/sparse/StateType.h" #include "constants.h" @@ -22,36 +23,17 @@ namespace storm { namespace utility { - namespace shortestPaths { - typedef storm::storage::sparse::state_type state_t; + namespace ksp { + typedef storage::sparse::state_type state_t; typedef std::vector 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 (`predecessorNode`) 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 [1] of the - * predecessor's shortest paths list. - * - * [1] oh, actually, the `k-1`th entry due to 0-based indexing! - */ template struct Path { boost::optional predecessorNode; unsigned long predecessorK; T distance; - // FIXME: uhh.. is this okay for set? just some arbitrary order + // arbitrary order for std::set bool operator<(const Path& rhs) const { if (predecessorNode != rhs.predecessorNode) { return predecessorNode < rhs.predecessorNode; @@ -69,21 +51,36 @@ namespace storm { template class ShortestPathsGenerator { public: - // FIXME: this shared_ptr-passing business is probably a bad idea - ShortestPathsGenerator(std::shared_ptr> model); + /*! + * Performs precomputations (including meta-target insertion and Dijkstra). + * Modifications are done locally, `model` remains unchanged. + * Target (group) cannot be changed. + */ + // FIXME: this shared_ptr-passing business might be a bad idea + ShortestPathsGenerator(std::shared_ptr> model, state_list_t const& targets); - ~ShortestPathsGenerator(); + // allow alternative ways of specifying the target, + // all of which will be converted to list and delegated to constructor above + ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget); + ShortestPathsGenerator(std::shared_ptr> model, storage::BitVector const& targetBV); + ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel); - // TODO: think about suitable output format - T getKShortest(state_t node, unsigned long k); + ~ShortestPathsGenerator(){} - // TODO: allow three kinds of target arguments: single state, BitVector, Label + /*! + * Computes k-SP to target and returns distance (probability). + */ + T computeKSP(unsigned long k); private: - std::shared_ptr> model; - storm::storage::SparseMatrix transitionMatrix; - state_t numStates; + std::shared_ptr> model; + storage::SparseMatrix transitionMatrix; + state_t numStates; // includes meta-target, i.e. states in model + 1 + + state_list_t targets; + std::unordered_set targetSet; + state_t metaTarget; std::vector graphPredecessors; std::vector> shortestPathPredecessors; @@ -130,22 +127,26 @@ namespace storm { /*! * Recurses over the path and prints the nodes. Intended for debugging. */ - void printKShortestPath(state_t targetNode, unsigned long k, bool head=true); + void printKShortestPath(state_t targetNode, unsigned long k, bool head=true) const; + + /*! + * Returns actual distance for real edges, 1 for edges to meta-target. + */ + T getEdgeDistance(state_t tailNode, state_t headNode) const; // --- tiny helper fcts --- - bool isInitialState(state_t node) { + bool isInitialState(state_t node) const { auto initialStates = model->getInitialStates(); return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); } - T getEdgeDistance(state_t tailNode, state_t headNode) { - for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) { - if (transition.getColumn() == headNode) { - return transition.getValue(); - } + state_list_t bitvectorToList(storage::BitVector const& bv) const { + state_list_t list; + for (state_t state : bv) { + list.push_back(state); } - return storm::utility::zero(); + return list; } // ----------------------- }; diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md index 6f1042ae4..61f6fe1e3 100644 --- a/src/utility/shortestPaths.md +++ b/src/utility/shortestPaths.md @@ -4,7 +4,8 @@ the design decisions and the rationale behind them.] ## Differences from REA algorithm This class closely follows the Jimenez-Marzal REA algorithm. -However, there are some notable deviations: +However, there are some notable deviations in the way targets and shortest +paths are defined. ### Target groups Firstly, instead of a single target state, a group of target states is @@ -13,6 +14,7 @@ transitions (other than self-loops, but this is moot due to not allowing non-minimal paths -- see below) and instead introducing edges to a new sink state that serves as a meta-target. + + +I chose to implement this by modifying the precomputation results, meaning +that they are only valid for a fixed group of target states. Thus, the +target group is required in the constructor. (It would have been possible to +allow for interchangeable target groups, but I don't anticipate that use +case.) ### Minimality of paths Secondly, we define shortest paths as "minimal" shortest paths in the -following sense: The path may only visit the target state once (at the -end). In other words, no KSP may be a prefix of another. +following sense: The path may not visit any target state except at the +end. As a corollary, no KSP (to a target node) may be a prefix of another. This in particular forbids shortest path progressions such as these: 1-SP: 1 2 3 @@ -48,3 +57,30 @@ interested in such paths. shorter paths is non-empty (which is an even stronger statement than loop-free-ness of paths), because we want to take a union of those node sets. But that's a different matter.) + + +## Data structures, in particular: Path representation + +The implicit shortest path representation that J&M describe in the paper +is used, except that indices rather than back-pointers are stored to +refer to the tail of the path. +[Maybe pointers would be faster? STL vector access via index should be +pretty fast too, though, and less error-prone.] + +A bit more detail (recap of the paper): +All shortest paths (from `s` to `t`) can be described as some k-shortest +path to some node `u` plus an edge to `t`: + + s ~~k-shortest path~~> u --> t + +Further, the shortest paths to some node are always computed in order and +without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed +before the 4-SP. Thus, we store the SPs in a linked list for each node, +with the k-th entry[^1] being the k-th SP to that node. + +Thus for an SP as shown above we simply store the predecessor node (`u`) +and the `k`, which allows us to look up the tail of the SP. +By recursively looking up the tail (until it's empty), we reconstruct +the entire path back-to-front. + +[^1]: Which due to 0-based indexing has index `k-1`, of course! Damn it. diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp new file mode 100644 index 000000000..b3118cec6 --- /dev/null +++ b/test/functional/utility/KSPTest.cpp @@ -0,0 +1,69 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/PrismParser.h" +#include "src/models/sparse/Dtmc.h" +#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/utility/graph.h" +#include "src/utility/shortestPaths.cpp" + +// NOTE: These result values of these tests were generated by the +// KSP-Generator itself and checked for gross implausibility, but no +// more than that. +// An independent verification of the values would be really nice ... + +TEST(KSPTest, dijkstra) { + 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); + + storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + + double dist = spg.computeKSP(1); + EXPECT_DOUBLE_EQ(0.015859334652581887, dist); +} + +TEST(KSPTest, singleTarget) { + 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); + + storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + + double dist = spg.computeKSP(100); + EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); +} + +TEST(KSPTest, reentry) { + 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); + + storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + + double dist = spg.computeKSP(100); + EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); + + // get another distance to ensure re-entry is no problem + double dist2 = spg.computeKSP(500); + EXPECT_DOUBLE_EQ(3.0462610000679282e-08, dist2); +} + +TEST(KSPTest, groupTarget) { + 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); + + auto spg = storm::utility::ksp::ShortestPathsGenerator(model, storm::utility::ksp::state_list_t{50, 90}); + + // this path should lead to 90 + double dist1 = spg.computeKSP(8); + EXPECT_DOUBLE_EQ(7.3796982335999988e-06, dist1); + + // this one to 50 + double dist2 = spg.computeKSP(9); + EXPECT_DOUBLE_EQ(3.92e-06, dist2); + + // this one to 90 again + double dist3 = spg.computeKSP(12); + EXPECT_DOUBLE_EQ(3.6160521344640002e-06, dist3); +} From fbee00e448a01ecb4e30d51b722a27e032df2330 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sun, 8 Nov 2015 22:39:02 +0100 Subject: [PATCH 13/35] KSP output as BitVector or list Former-commit-id: f8a74864f7593b946bf5b4cbce49cbe1e90dd3b3 [formerly 3b61d8d47673df18dfd6e452566dafe7570d4a31] Former-commit-id: 4fe402ae83d6eabd535cffdeb4316f568405c395 --- src/utility/shortestPaths.cpp | 70 +++++++++++++++++++++++------ src/utility/shortestPaths.h | 33 +++++++++++--- test/functional/utility/KSPTest.cpp | 60 +++++++++++++++++++++---- 3 files changed, 135 insertions(+), 28 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 1b60717d7..087456877 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -45,23 +45,50 @@ namespace storm { std::string const& targetLabel) : ShortestPathsGenerator(model, bitvectorToList(model->getStates(targetLabel))) {} template - T ShortestPathsGenerator::computeKSP(unsigned long k) { - unsigned long alreadyComputedK = kShortestPaths[metaTarget].size(); + T ShortestPathsGenerator::getDistance(unsigned long k) { + computeKSP(k); + return kShortestPaths[metaTarget][k - 1].distance; + } - for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { - computeNextPath(metaTarget, nextK); - if (kShortestPaths[metaTarget].size() < nextK) { - std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; - printKShortestPath(metaTarget, nextK - 1); - std::cout << "---------" << "No other path exists!" << std::endl; - return utility::zero(); // TODO: throw exception or something - } + template + storage::BitVector ShortestPathsGenerator::getStates(unsigned long k) { + computeKSP(k); + storage::BitVector stateSet(numStates - 1, false); // no meta-target + + Path currentPath = kShortestPaths[metaTarget][k - 1]; + boost::optional maybePredecessor = currentPath.predecessorNode; + // this omits the first node, which is actually convenient since that's the meta-target + + while (maybePredecessor) { + state_t predecessor = maybePredecessor.get(); + stateSet.set(predecessor, true); + + currentPath = kShortestPaths[predecessor][currentPath.predecessorK - 1]; // god damn you, index + maybePredecessor = currentPath.predecessorNode; } - //std::cout << std::endl << "--> DEBUG: Finished. " << k << "-shortest path:" << std::endl; - //printKShortestPath(metaTarget, k); - //std::cout << "---------" << std::endl; - return kShortestPaths[metaTarget][k - 1].distance; + return stateSet; + } + + template + state_list_t ShortestPathsGenerator::getPathAsList(unsigned long k) { + computeKSP(k); + + state_list_t backToFrontList; + + Path currentPath = kShortestPaths[metaTarget][k - 1]; + boost::optional maybePredecessor = currentPath.predecessorNode; + // this omits the first node, which is actually convenient since that's the meta-target + + while (maybePredecessor) { + state_t predecessor = maybePredecessor.get(); + backToFrontList.push_back(predecessor); + + currentPath = kShortestPaths[predecessor][currentPath.predecessorK - 1]; + maybePredecessor = currentPath.predecessorNode; + } + + return backToFrontList; } template @@ -269,6 +296,21 @@ namespace storm { } } + template + void ShortestPathsGenerator::computeKSP(unsigned long k) { + unsigned long alreadyComputedK = kShortestPaths[metaTarget].size(); + + for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { + computeNextPath(metaTarget, nextK); + if (kShortestPaths[metaTarget].size() < nextK) { + //std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; + //printKShortestPath(metaTarget, nextK - 1); + //std::cout << "---------" << "No other path exists!" << std::endl; + throw std::invalid_argument("k-SP does not exist for k=" + std::to_string(k)); + } + } + } + template void ShortestPathsGenerator::printKShortestPath(state_t targetNode, unsigned long k, bool head) const { // note the index shift! risk of off-by-one diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 742cc2eec..8139f1c91 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -65,12 +65,29 @@ namespace storm { ShortestPathsGenerator(std::shared_ptr> model, storage::BitVector const& targetBV); ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel); - ~ShortestPathsGenerator(){} + inline ~ShortestPathsGenerator(){} /*! - * Computes k-SP to target and returns distance (probability). + * Returns distance (i.e., probability) of the KSP. + * Computes KSP if not yet computed. + * @throws std::invalid_argument if no such k-shortest path exists */ - T computeKSP(unsigned long k); + T getDistance(unsigned long k); + + /*! + * Returns the states that occur in the KSP. + * For a path-traversal (in order and with duplicates), see `getKSP`. + * Computes KSP if not yet computed. + * @throws std::invalid_argument if no such k-shortest path exists + */ + storage::BitVector getStates(unsigned long k); + + /*! + * Returns the states of the KSP as back-to-front traversal. + * Computes KSP if not yet computed. + * @throws std::invalid_argument if no such k-shortest path exists + */ + state_list_t getPathAsList(unsigned long k); private: @@ -124,6 +141,12 @@ namespace storm { */ void computeNextPath(state_t node, unsigned long k); + /*! + * Computes k-shortest path if not yet computed. + * @throws std::invalid_argument if no such k-shortest path exists + */ + void computeKSP(unsigned long k); + /*! * Recurses over the path and prints the nodes. Intended for debugging. */ @@ -136,12 +159,12 @@ namespace storm { // --- tiny helper fcts --- - bool isInitialState(state_t node) const { + inline bool isInitialState(state_t node) const { auto initialStates = model->getInitialStates(); return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); } - state_list_t bitvectorToList(storage::BitVector const& bv) const { + inline state_list_t bitvectorToList(storage::BitVector const& bv) const { state_list_t list; for (state_t state : bv) { list.push_back(state); diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index b3118cec6..3a940359f 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -7,7 +7,7 @@ #include "src/utility/graph.h" #include "src/utility/shortestPaths.cpp" -// NOTE: These result values of these tests were generated by the +// NOTE: The KSPs / distances of these tests were generated by the // KSP-Generator itself and checked for gross implausibility, but no // more than that. // An independent verification of the values would be really nice ... @@ -19,7 +19,7 @@ TEST(KSPTest, dijkstra) { storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); - double dist = spg.computeKSP(1); + double dist = spg.getDistance(1); EXPECT_DOUBLE_EQ(0.015859334652581887, dist); } @@ -30,7 +30,7 @@ TEST(KSPTest, singleTarget) { storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); - double dist = spg.computeKSP(100); + double dist = spg.getDistance(100); EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); } @@ -41,11 +41,11 @@ TEST(KSPTest, reentry) { storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); - double dist = spg.computeKSP(100); + double dist = spg.getDistance(100); EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); // get another distance to ensure re-entry is no problem - double dist2 = spg.computeKSP(500); + double dist2 = spg.getDistance(500); EXPECT_DOUBLE_EQ(3.0462610000679282e-08, dist2); } @@ -53,17 +53,59 @@ TEST(KSPTest, groupTarget) { 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); - auto spg = storm::utility::ksp::ShortestPathsGenerator(model, storm::utility::ksp::state_list_t{50, 90}); + auto groupTarget = storm::utility::ksp::state_list_t{50, 90}; + auto spg = storm::utility::ksp::ShortestPathsGenerator(model, groupTarget); // this path should lead to 90 - double dist1 = spg.computeKSP(8); + double dist1 = spg.getDistance(8); EXPECT_DOUBLE_EQ(7.3796982335999988e-06, dist1); // this one to 50 - double dist2 = spg.computeKSP(9); + double dist2 = spg.getDistance(9); EXPECT_DOUBLE_EQ(3.92e-06, dist2); // this one to 90 again - double dist3 = spg.computeKSP(12); + double dist3 = spg.getDistance(12); EXPECT_DOUBLE_EQ(3.6160521344640002e-06, dist3); } + +TEST(KSPTest, kTooLargeException) { + 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); + + storm::storage::sparse::state_type testState = 1; + storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + + ASSERT_THROW(spg.getDistance(2), std::invalid_argument); +} + +TEST(KSPTest, kspStateSet) { + 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); + + storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + + storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); + for (auto s : storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) { + referenceBV.set(s, true); + } + + auto bv = spg.getStates(7); + + EXPECT_EQ(bv, referenceBV); +} + +TEST(KSPTest, kspPathAsList) { + 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); + + storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + + // TODO: use path that actually has a loop or something to make this more interesting + auto reference = storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; + auto list = spg.getPathAsList(7); + + EXPECT_EQ(list, reference); +} From 5d28c4cb57d7f336ea1e49b3ea003b3f9f644817 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sun, 8 Nov 2015 23:51:17 +0100 Subject: [PATCH 14/35] naive performance test on crowds5-4 (cf Comics) Former-commit-id: c1616d07fd9bfd1131b6a607349f19ce58c2dc98 [formerly e2068f5e84c369ce682008aa1d9d1070e29fa793] Former-commit-id: 158cf0a2452aebf28beddb585890691d9c97d7b4 --- test/functional/builder/crowds-5-4.pm | 69 +++++++++++++++++++++++++++ test/functional/utility/KSPTest.cpp | 7 +++ test/performance/utility/KSPTest.cpp | 44 +++++++++++++++++ 3 files changed, 120 insertions(+) create mode 100644 test/functional/builder/crowds-5-4.pm create mode 100644 test/performance/utility/KSPTest.cpp diff --git a/test/functional/builder/crowds-5-4.pm b/test/functional/builder/crowds-5-4.pm new file mode 100644 index 000000000..0eb518bf6 --- /dev/null +++ b/test/functional/builder/crowds-5-4.pm @@ -0,0 +1,69 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 4; +// size of the crowd +const int CrowdSize = 5; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> 1: (phase'=0); + +endmodule + +label "observe0Greater1" = observe0>1; +label "observe1Greater1" = observe1>1; +label "observe2Greater1" = observe2>1; +label "observe3Greater1" = observe3>1; +label "observe4Greater1" = observe4>1; +label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index 3a940359f..1e1dd3070 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -109,3 +109,10 @@ TEST(KSPTest, kspPathAsList) { EXPECT_EQ(list, reference); } + + +//---------------------------- +// v---- PLAYGROUND ----v +//---------------------------- + +// (empty) diff --git a/test/performance/utility/KSPTest.cpp b/test/performance/utility/KSPTest.cpp new file mode 100644 index 000000000..ea43f9826 --- /dev/null +++ b/test/performance/utility/KSPTest.cpp @@ -0,0 +1,44 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/PrismParser.h" +#include "src/models/sparse/Dtmc.h" +#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/utility/graph.h" +#include "src/utility/shortestPaths.cpp" + +const bool VERBOSE = true; + +TEST(KSPTest, crowdsSpeed) { + if (VERBOSE) std::cout << "Parsing crowds-5-4.pm file and building model ... " << std::endl; + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-4.pm"); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); + + if (VERBOSE) std::cout << "Initializing ShortestPathsGenerator ..." << std::endl; + // timekeeping taken from http://en.cppreference.com/w/cpp/chrono#Example + std::chrono::time_point startTime = std::chrono::system_clock::now(); + + auto target = "observe0Greater1"; + storm::utility::ksp::ShortestPathsGenerator spg(model, target); + + storm::storage::BitVector accStates(model->getNumberOfStates(), false); + double accumProb = 0; + + if (VERBOSE) std::cout << "Accumulating shortest paths ..." << std::endl; + for (int i = 1; accumProb < 0.15; i++) { + double pathProb = spg.getDistance(i); + accumProb += pathProb; + + storm::storage::BitVector statesInPath = spg.getStates(i); + accStates |= statesInPath; + + if (i % 50000 == 0) { + if (VERBOSE) std::cout << " --> It/States/AccProb/PathProb: " << i << " / " << accStates.getNumberOfSetBits() << " / " << accumProb << " / " << pathProb << std::endl; + } + } + + std::chrono::duration elapsedSeconds = std::chrono::system_clock::now() - startTime; + if (VERBOSE) std::cout << "Done. Num of states: " << accStates.getNumberOfSetBits() << ". Seconds: " << elapsedSeconds.count() << std::endl; + + EXPECT_LE(elapsedSeconds.count(), 5); // should take less than 5 seconds on a modern PC +} From 80382da0337689791dd8233972c6a5a1ce50b57b Mon Sep 17 00:00:00 2001 From: tomjanson Date: Wed, 16 Nov 2016 18:34:35 +0100 Subject: [PATCH 15/35] adapt KSP test cases to new API; still fail Former-commit-id: 984f4f9b69363caa3a98dd717fda82d812b92180 [formerly 5de4e31bc8d7a48484b1206aa43f032e91ceed64] Former-commit-id: c41eea12e8a5d2214b459639b374e8ee26a05289 --- test/functional/utility/KSPTest.cpp | 35 ++++++++++++++++------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index 1e1dd3070..aba8747c3 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -1,9 +1,10 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/PrismParser.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/models/sparse/Dtmc.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/parser/PrismParser.h" +#include "src/storage/SymbolicModelDescription.h" #include "src/utility/graph.h" #include "src/utility/shortestPaths.cpp" @@ -12,9 +13,17 @@ // more than that. // An independent verification of the values would be really nice ... +// FIXME: (almost) all of these fail; the question is: is there actually anything wrong or does the new parser yield a different order of states? + +std::shared_ptr> buildExampleModel() { + std::string prismModelPath = STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"; + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); + storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); + return storm::builder::ExplicitModelBuilder(program).build(); +} + TEST(KSPTest, dijkstra) { - 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); + auto model = buildExampleModel(); storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); @@ -24,8 +33,7 @@ TEST(KSPTest, dijkstra) { } TEST(KSPTest, singleTarget) { - 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); + auto model = buildExampleModel(); storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); @@ -35,8 +43,7 @@ TEST(KSPTest, singleTarget) { } TEST(KSPTest, reentry) { - 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); + auto model = buildExampleModel(); storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); @@ -50,8 +57,7 @@ TEST(KSPTest, reentry) { } TEST(KSPTest, groupTarget) { - 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); + auto model = buildExampleModel(); auto groupTarget = storm::utility::ksp::state_list_t{50, 90}; auto spg = storm::utility::ksp::ShortestPathsGenerator(model, groupTarget); @@ -70,8 +76,7 @@ TEST(KSPTest, groupTarget) { } TEST(KSPTest, kTooLargeException) { - 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); + auto model = buildExampleModel(); storm::storage::sparse::state_type testState = 1; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); @@ -80,8 +85,7 @@ TEST(KSPTest, kTooLargeException) { } TEST(KSPTest, kspStateSet) { - 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); + auto model = buildExampleModel(); storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); @@ -97,8 +101,7 @@ TEST(KSPTest, kspStateSet) { } TEST(KSPTest, kspPathAsList) { - 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); + auto model = buildExampleModel(); storm::storage::sparse::state_type testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); From cf1fa2bfc9eed62327fa549e7b5f5ecaee0693a9 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 20:27:55 +0100 Subject: [PATCH 16/35] the plan --- src/utility/shortestPaths.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md index 61f6fe1e3..db5dcc326 100644 --- a/src/utility/shortestPaths.md +++ b/src/utility/shortestPaths.md @@ -39,6 +39,28 @@ target group is required in the constructor. (It would have been possible to allow for interchangeable target groups, but I don't anticipate that use case.) +#### Special case: Using Matrix/Vector from SamplingModel + +The class has been updated to support the matrix/vector that `SamplingModel` +generates (as an instance of a PDTMC) as input. This is in fact closely +related to the target groups, since it works as follows: + +The input is a (sub-stochastic) transition matrix of the maybe-states (only!) +and a vector (again over the maybe-states) with the probabilities to an +implied target state. + +This naturally corresponds to having a meta-target, except the probability +of its incoming edges range over $(0,1]$ rather than being $1$. +Thus, applying the term "target group" to the set of states with non-zero +transitions to the meta-target is now misleading (I suppose the correct term +would now be "meta-target predecessors"), but nevertheless it should work +exactly the same. [Right?] + +In terms of implementation, in `getEdgeDistance` as well as in the loop of +the Dijkstra, the "virtual" edges to the meta-target were checked for and +set to probability $1$; this must now be changed to use the probability as +indicated in the `targetProbVector` if this input format is used. + ### Minimality of paths Secondly, we define shortest paths as "minimal" shortest paths in the following sense: The path may not visit any target state except at the From e883c605198f7f7fe0d977549af379a7f5ee63a9 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 20:31:48 +0100 Subject: [PATCH 17/35] rm model as member; extracting all needed stuff in ctor # Conflicts: # src/utility/shortestPaths.cpp --- src/utility/shortestPaths.cpp | 15 +++++++-------- src/utility/shortestPaths.h | 14 +++++++++----- 2 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index ac868070d..409030c32 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -8,12 +8,11 @@ namespace storm { namespace ksp { template ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - state_list_t const& targets) : model(model), targets(targets) { - // FIXME: does this create a copy? I don't need one, so I should avoid that - transitionMatrix = model->getTransitionMatrix(); - numStates = model->getNumberOfStates() + 1; // one more for meta-target - - metaTarget = numStates - 1; // first unused state number + state_list_t const& targets) : transitionMatrix(model->getTransitionMatrix()), + numStates(model->getNumberOfStates() + 1), // one more for meta-target + metaTarget(model->getNumberOfStates()), // first unused state number + initialStates(model->getInitialStates()), + targets(targets) { targetSet = std::unordered_set(targets.begin(), targets.end()); computePredecessors(); @@ -126,7 +125,7 @@ namespace storm { // default comparison on pair actually works fine if distance is the first entry std::set, std::greater>> dijkstraQueue; - for (state_t initialState : model->getInitialStates()) { + for (state_t initialState : initialStates) { shortestPathDistances[initialState] = zeroDistance; dijkstraQueue.emplace(zeroDistance, initialState); } @@ -179,7 +178,7 @@ namespace storm { // BFS in Dijkstra-SP order std::queue bfsQueue; - for (state_t initialState : model->getInitialStates()) { + for (state_t initialState : initialStates) { bfsQueue.push(initialState); } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 8139f1c91..64fa16ca6 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -63,7 +63,13 @@ namespace storm { // all of which will be converted to list and delegated to constructor above ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget); ShortestPathsGenerator(std::shared_ptr> model, storage::BitVector const& targetBV); - ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel); + ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel = "target"); + + // a further alternative: use transition matrix of maybe-states + // combined with target vector (e.g., the instantiated matrix/ + // vector from SamplingModel); + // in this case separately specifying a target makes no sense + //ShortestPathsGenerator(storm::storage::SparseMatrix maybeTransitionMatrix, std::vector targetProbVector); inline ~ShortestPathsGenerator(){} @@ -91,13 +97,12 @@ namespace storm { private: - std::shared_ptr> model; storage::SparseMatrix transitionMatrix; state_t numStates; // includes meta-target, i.e. states in model + 1 - - state_list_t targets; std::unordered_set targetSet; state_t metaTarget; + storage::BitVector initialStates; + state_list_t targets; std::vector graphPredecessors; std::vector> shortestPathPredecessors; @@ -160,7 +165,6 @@ namespace storm { // --- tiny helper fcts --- inline bool isInitialState(state_t node) const { - auto initialStates = model->getInitialStates(); return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); } From 68ac0b24ecb97581a61b88dd05a4a4e36be9aeb9 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 21 Jan 2016 19:05:16 +0100 Subject: [PATCH 18/35] instantiate template for shortest path generation Former-commit-id: e5f505b8d45198c20b96e7e3735dcf56deac42a6 [formerly 7146af99e316b09b792df0cd54996ce01353e0c8] Former-commit-id: 24e3f3d92a56d3869d972d20742d6e95ac2b97e8 --- src/utility/shortestPaths.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 087456877..ac868070d 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -332,6 +332,9 @@ namespace storm { std::cout << " ]" << std::endl; } } + + + template class ShortestPathsGenerator; } } } From 235671d67db81fefb6fda58f37e6cb8652ed5aaa Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 20:41:55 +0100 Subject: [PATCH 19/35] use map rather than set for target[Prob] --- src/utility/shortestPaths.cpp | 8 +++++--- src/utility/shortestPaths.h | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 409030c32..3b6772464 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -13,7 +13,9 @@ namespace storm { metaTarget(model->getNumberOfStates()), // first unused state number initialStates(model->getInitialStates()), targets(targets) { - targetSet = std::unordered_set(targets.begin(), targets.end()); + for (state_t target : targets) { + targetProbMap.emplace(target, one()); + } computePredecessors(); @@ -134,7 +136,7 @@ namespace storm { state_t currentNode = (*dijkstraQueue.begin()).second; dijkstraQueue.erase(dijkstraQueue.begin()); - if (targetSet.count(currentNode) == 0) { + if (targetProbMap.count(currentNode) == 0) { // non-target node, treated normally for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) { state_t otherNode = transition.getColumn(); @@ -223,7 +225,7 @@ namespace storm { return utility::zero(); } else { // edge must be "virtual edge" from target state to meta-target - assert(targetSet.count(tailNode) == 1); + assert(targetProbMap.count(tailNode) == 1); return utility::one(); } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 64fa16ca6..2c8927609 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -99,10 +99,10 @@ namespace storm { private: storage::SparseMatrix transitionMatrix; state_t numStates; // includes meta-target, i.e. states in model + 1 - std::unordered_set targetSet; state_t metaTarget; storage::BitVector initialStates; state_list_t targets; + std::unordered_map targetProbMap; std::vector graphPredecessors; std::vector> shortestPathPredecessors; From 55599b51e7ffefed077884d4f3e48527aadd6e7d Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 22:32:42 +0100 Subject: [PATCH 20/35] aliased BitVector, used state_t more (cosmetic) --- src/utility/shortestPaths.cpp | 4 ++-- src/utility/shortestPaths.h | 3 ++- test/functional/utility/KSPTest.cpp | 18 +++++++++--------- 3 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 3b6772464..02356d974 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -52,9 +52,9 @@ namespace storm { } template - storage::BitVector ShortestPathsGenerator::getStates(unsigned long k) { + BitVector ShortestPathsGenerator::getStates(unsigned long k) { computeKSP(k); - storage::BitVector stateSet(numStates - 1, false); // no meta-target + BitVector stateSet(numStates - 1, false); // no meta-target Path currentPath = kShortestPaths[metaTarget][k - 1]; boost::optional maybePredecessor = currentPath.predecessorNode; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 2c8927609..d1219d390 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -26,6 +26,7 @@ namespace storm { namespace ksp { typedef storage::sparse::state_type state_t; typedef std::vector state_list_t; + using BitVector = storage::BitVector; template struct Path { @@ -100,8 +101,8 @@ namespace storm { storage::SparseMatrix transitionMatrix; state_t numStates; // includes meta-target, i.e. states in model + 1 state_t metaTarget; - storage::BitVector initialStates; state_list_t targets; + BitVector initialStates; std::unordered_map targetProbMap; std::vector graphPredecessors; diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index aba8747c3..746118319 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -25,7 +25,7 @@ std::shared_ptr> buildExampleModel() { TEST(KSPTest, dijkstra) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::state_t testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); double dist = spg.getDistance(1); @@ -35,7 +35,7 @@ TEST(KSPTest, dijkstra) { TEST(KSPTest, singleTarget) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::state_t testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); double dist = spg.getDistance(100); @@ -45,7 +45,7 @@ TEST(KSPTest, singleTarget) { TEST(KSPTest, reentry) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::state_t testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); double dist = spg.getDistance(100); @@ -59,7 +59,7 @@ TEST(KSPTest, reentry) { TEST(KSPTest, groupTarget) { auto model = buildExampleModel(); - auto groupTarget = storm::utility::ksp::state_list_t{50, 90}; + auto groupTarget = std::vector{50, 90}; auto spg = storm::utility::ksp::ShortestPathsGenerator(model, groupTarget); // this path should lead to 90 @@ -78,7 +78,7 @@ TEST(KSPTest, groupTarget) { TEST(KSPTest, kTooLargeException) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 1; + storm::utility::ksp::state_t testState = 1; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); ASSERT_THROW(spg.getDistance(2), std::invalid_argument); @@ -87,11 +87,11 @@ TEST(KSPTest, kTooLargeException) { TEST(KSPTest, kspStateSet) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::state_t testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); - for (auto s : storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) { + for (auto s : std::vector{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) { referenceBV.set(s, true); } @@ -103,11 +103,11 @@ TEST(KSPTest, kspStateSet) { TEST(KSPTest, kspPathAsList) { auto model = buildExampleModel(); - storm::storage::sparse::state_type testState = 300; + storm::utility::ksp::state_t testState = 300; storm::utility::ksp::ShortestPathsGenerator spg(model, testState); // TODO: use path that actually has a loop or something to make this more interesting - auto reference = storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; + auto reference = std::vector{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; auto list = spg.getPathAsList(7); EXPECT_EQ(list, reference); From 44b3a9108e72137cc2d662e6e5da4048029e9c5e Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 22:39:08 +0100 Subject: [PATCH 21/35] switching from vector to BV as authoritative input # Conflicts: # src/utility/shortestPaths.h --- src/utility/shortestPaths.cpp | 21 +++++++++++++-------- src/utility/shortestPaths.h | 28 +++++++++++++--------------- test/functional/utility/KSPTest.cpp | 2 +- 3 files changed, 27 insertions(+), 24 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 02356d974..15039a4c3 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -30,20 +30,25 @@ namespace storm { candidatePaths.resize(numStates); } + // extracts the relevant info from the model and delegates to ctor above + template + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, BitVector const& targetBV) + : ShortestPathsGenerator(model->getTransitionMatrix(), allProbOneMap(targetBV), model->getInitialStates()) {} + // several alternative ways to specify the targets are provided, // each converts the targets and delegates to the ctor above // I admit it's kind of ugly, but actually pretty convenient (and I've wanted to try C++11 delegation) template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - state_t singleTarget) : ShortestPathsGenerator(model, std::vector{singleTarget}) {} + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget) + : ShortestPathsGenerator(model, std::vector{singleTarget}) {} template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - storage::BitVector const& targetBV) : ShortestPathsGenerator(model, bitvectorToList(targetBV)) {} + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, std::vector const& targetList) + : ShortestPathsGenerator(model, BitVector(model->getNumberOfStates(), targetList)) {} template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - std::string const& targetLabel) : ShortestPathsGenerator(model, bitvectorToList(model->getStates(targetLabel))) {} + ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel) + : ShortestPathsGenerator(model, model->getStates(targetLabel)) {} template T ShortestPathsGenerator::getDistance(unsigned long k) { @@ -72,10 +77,10 @@ namespace storm { } template - state_list_t ShortestPathsGenerator::getPathAsList(unsigned long k) { + std::vector ShortestPathsGenerator::getPathAsList(unsigned long k) { computeKSP(k); - state_list_t backToFrontList; + std::vector backToFrontList; Path currentPath = kShortestPaths[metaTarget][k - 1]; boost::optional maybePredecessor = currentPath.predecessorNode; diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index d1219d390..402fb31f6 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -12,21 +12,20 @@ // for more information about the purpose, design decisions, // etc., you may consult `shortestPath.md`. - Tom -/* - * TODO: - * - take care of self-loops of target states - * - implement target group - * - think about how to get paths with new nodes, rather than different - * paths over the same set of states (which happens often) - */ +// TODO: test whether using BitVector instead of vector is +// faster for storing predecessors etc. +// Now using BitVectors instead of vector in the API because +// BitVectors are used throughout Storm to represent a (unordered) list +// of states. +// (Even though both initialStates and targets are probably very sparse.) namespace storm { namespace utility { namespace ksp { typedef storage::sparse::state_type state_t; - typedef std::vector state_list_t; using BitVector = storage::BitVector; + typedef std::vector ordered_state_list_t; template struct Path { @@ -57,13 +56,12 @@ namespace storm { * Modifications are done locally, `model` remains unchanged. * Target (group) cannot be changed. */ - // FIXME: this shared_ptr-passing business might be a bad idea - ShortestPathsGenerator(std::shared_ptr> model, state_list_t const& targets); + ShortestPathsGenerator(std::shared_ptr> model, BitVector const& targetBV); // allow alternative ways of specifying the target, - // all of which will be converted to list and delegated to constructor above + // all of which will be converted to BitVector and delegated to constructor above ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget); - ShortestPathsGenerator(std::shared_ptr> model, storage::BitVector const& targetBV); + ShortestPathsGenerator(std::shared_ptr> model, std::vector const& targetList); ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel = "target"); // a further alternative: use transition matrix of maybe-states @@ -94,7 +92,7 @@ namespace storm { * Computes KSP if not yet computed. * @throws std::invalid_argument if no such k-shortest path exists */ - state_list_t getPathAsList(unsigned long k); + ordered_state_list_t getPathAsList(unsigned long k); private: @@ -105,9 +103,9 @@ namespace storm { BitVector initialStates; std::unordered_map targetProbMap; - std::vector graphPredecessors; + std::vector graphPredecessors; // FIXME is a switch to BitVector a good idea here? std::vector> shortestPathPredecessors; - std::vector shortestPathSuccessors; + std::vector shortestPathSuccessors; std::vector shortestPathDistances; std::vector>> kShortestPaths; diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index 746118319..d1c9a2f8f 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -107,7 +107,7 @@ TEST(KSPTest, kspPathAsList) { storm::utility::ksp::ShortestPathsGenerator spg(model, testState); // TODO: use path that actually has a loop or something to make this more interesting - auto reference = std::vector{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; + auto reference = storm::utility::ksp::ordered_state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; auto list = spg.getPathAsList(7); EXPECT_EQ(list, reference); From 51c44bb7866e29a5541366d3dd440c7c23a63a7f Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 22:42:58 +0100 Subject: [PATCH 22/35] matrix/vector ctor, targetProbMap, TODO: non-1 entries --- src/utility/shortestPaths.cpp | 29 +++++++++++++++-------------- src/utility/shortestPaths.h | 19 +++++++++++++------ 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 15039a4c3..ffd3730f1 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -7,15 +7,12 @@ namespace storm { namespace utility { namespace ksp { template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, - state_list_t const& targets) : transitionMatrix(model->getTransitionMatrix()), - numStates(model->getNumberOfStates() + 1), // one more for meta-target - metaTarget(model->getNumberOfStates()), // first unused state number - initialStates(model->getInitialStates()), - targets(targets) { - for (state_t target : targets) { - targetProbMap.emplace(target, one()); - } + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix transitionMatrix, std::unordered_map targetProbMap, BitVector initialStates) : + transitionMatrix(transitionMatrix), + numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target + metaTarget(transitionMatrix.getColumnCount()), // first unused state index + initialStates(initialStates), + targetProbMap(targetProbMap) { computePredecessors(); @@ -30,6 +27,8 @@ namespace storm { candidatePaths.resize(numStates); } + // TODO: probTargetVector [!] to probTargetMap ctor + // extracts the relevant info from the model and delegates to ctor above template ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, BitVector const& targetBV) @@ -108,14 +107,16 @@ namespace storm { for (auto const& transition : transitionMatrix.getRowGroup(i)) { // to avoid non-minimal paths, the target states are // *not* predecessors of any state but the meta-target - if (std::find(targets.begin(), targets.end(), i) == targets.end()) { + if (!isTargetState(i)) { graphPredecessors[transition.getColumn()].push_back(i); } } } // meta-target has exactly the target states as predecessors - graphPredecessors[metaTarget] = targets; + for (auto targetProbPair : targetProbMap) { // FIXME + graphPredecessors[metaTarget].push_back(targetProbPair.first); + } } template @@ -141,7 +142,7 @@ namespace storm { state_t currentNode = (*dijkstraQueue.begin()).second; dijkstraQueue.erase(dijkstraQueue.begin()); - if (targetProbMap.count(currentNode) == 0) { + if (!isTargetState(currentNode)) { // non-target node, treated normally for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) { state_t otherNode = transition.getColumn(); @@ -157,7 +158,7 @@ namespace storm { } else { // target node has only "virtual edge" (with prob 1) to meta-target // no multiplication necessary - T alternateDistance = shortestPathDistances[currentNode]; + T alternateDistance = shortestPathDistances[currentNode]; // FIXME if (alternateDistance > shortestPathDistances[metaTarget]) { shortestPathDistances[metaTarget] = alternateDistance; shortestPathPredecessors[metaTarget] = boost::optional(currentNode); @@ -231,7 +232,7 @@ namespace storm { } else { // edge must be "virtual edge" from target state to meta-target assert(targetProbMap.count(tailNode) == 1); - return utility::one(); + return one(); } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 402fb31f6..400485997 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -69,6 +69,7 @@ namespace storm { // vector from SamplingModel); // in this case separately specifying a target makes no sense //ShortestPathsGenerator(storm::storage::SparseMatrix maybeTransitionMatrix, std::vector targetProbVector); + ShortestPathsGenerator(storm::storage::SparseMatrix maybeTransitionMatrix, std::unordered_map targetProbMap, BitVector initialStates); inline ~ShortestPathsGenerator(){} @@ -99,7 +100,6 @@ namespace storm { storage::SparseMatrix transitionMatrix; state_t numStates; // includes meta-target, i.e. states in model + 1 state_t metaTarget; - state_list_t targets; BitVector initialStates; std::unordered_map targetProbMap; @@ -167,12 +167,19 @@ namespace storm { return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); } - inline state_list_t bitvectorToList(storage::BitVector const& bv) const { - state_list_t list; - for (state_t state : bv) { - list.push_back(state); + inline bool isTargetState(state_t node) const { + return targetProbMap.count(node) == 1; + } + + /** + * Returns a map where each state of the input BitVector is mapped to 1 (`one`). + */ + inline std::unordered_map allProbOneMap(BitVector bitVector) const& { + std::unordered_map stateProbMap; + for (state_t node : bitVector) { + stateProbMap.emplace(node, one()); } - return list; + return stateProbMap; } // ----------------------- }; From 5f6637448130e1274111894c2d3b2bf5ef4dd3e1 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 23:00:21 +0100 Subject: [PATCH 23/35] vector to map conversion --- src/utility/shortestPaths.cpp | 4 +++- src/utility/shortestPaths.h | 29 +++++++++++++++++++++++------ 2 files changed, 26 insertions(+), 7 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index ffd3730f1..f70799d15 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -27,7 +27,9 @@ namespace storm { candidatePaths.resize(numStates); } - // TODO: probTargetVector [!] to probTargetMap ctor + template + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix transitionMatrix, std::vector targetProbVector, BitVector initialStates) + : ShortestPathsGenerator(transitionMatrix, vectorToMap(targetProbVector), initialStates) {} // extracts the relevant info from the model and delegates to ctor above template diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 400485997..b78a0758a 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -65,11 +65,11 @@ namespace storm { ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel = "target"); // a further alternative: use transition matrix of maybe-states - // combined with target vector (e.g., the instantiated matrix/ - // vector from SamplingModel); + // combined with target vector (e.g., the instantiated matrix/vector from SamplingModel); // in this case separately specifying a target makes no sense - //ShortestPathsGenerator(storm::storage::SparseMatrix maybeTransitionMatrix, std::vector targetProbVector); - ShortestPathsGenerator(storm::storage::SparseMatrix maybeTransitionMatrix, std::unordered_map targetProbMap, BitVector initialStates); + ShortestPathsGenerator(storage::SparseMatrix transitionMatrix, std::vector targetProbVector, BitVector initialStates); + ShortestPathsGenerator(storage::SparseMatrix maybeTransitionMatrix, std::unordered_map targetProbMap, BitVector initialStates); + inline ~ShortestPathsGenerator(){} @@ -174,13 +174,30 @@ namespace storm { /** * Returns a map where each state of the input BitVector is mapped to 1 (`one`). */ - inline std::unordered_map allProbOneMap(BitVector bitVector) const& { + inline std::unordered_map allProbOneMap(BitVector bitVector) const { std::unordered_map stateProbMap; for (state_t node : bitVector) { - stateProbMap.emplace(node, one()); + stateProbMap.emplace(node, one()); // FIXME check rvalue warning (here and below) } return stateProbMap; } + + inline std::unordered_map vectorToMap(std::vector probVector) const { + assert(probVector.size() == numStates); + + std::unordered_map stateProbMap; + + // non-zero entries (i.e. true transitions) are added to the map + for (state_t i = 0; i < probVector.size(); i++) { + T probEntry = probVector[i]; + if (probEntry != 0) { + assert(0 < probEntry <= 1); + stateProbMap.emplace(i, probEntry); + } + } + + return stateProbMap; + } // ----------------------- }; } From b58d48f92dee69634dd1e7c8f378bc4d7beeb1eb Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 23:54:27 +0100 Subject: [PATCH 24/35] use probs from targetProbMap TODO: test --- src/utility/shortestPaths.cpp | 24 +++++++++++++----------- src/utility/shortestPaths.h | 4 ++-- src/utility/shortestPaths.md | 12 +++++++----- 3 files changed, 22 insertions(+), 18 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index f70799d15..c9ce0b608 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -107,16 +107,18 @@ namespace storm { for (state_t i = 0; i < numStates - 1; i++) { for (auto const& transition : transitionMatrix.getRowGroup(i)) { - // to avoid non-minimal paths, the target states are + // to avoid non-minimal paths, the meta-target-predecessors are // *not* predecessors of any state but the meta-target - if (!isTargetState(i)) { + if (!isMetaTargetPredecessor(i)) { graphPredecessors[transition.getColumn()].push_back(i); } } } - // meta-target has exactly the target states as predecessors - for (auto targetProbPair : targetProbMap) { // FIXME + // meta-target has exactly the meta-target-predecessors as predecessors + // (duh. note that the meta-target-predecessors used to be called target, + // but that's not necessarily true in the matrix/value invocation case) + for (auto targetProbPair : targetProbMap) { graphPredecessors[metaTarget].push_back(targetProbPair.first); } } @@ -144,7 +146,7 @@ namespace storm { state_t currentNode = (*dijkstraQueue.begin()).second; dijkstraQueue.erase(dijkstraQueue.begin()); - if (!isTargetState(currentNode)) { + if (!isMetaTargetPredecessor(currentNode)) { // non-target node, treated normally for (auto const& transition : transitionMatrix.getRowGroup(currentNode)) { state_t otherNode = transition.getColumn(); @@ -158,9 +160,9 @@ namespace storm { } } } else { - // target node has only "virtual edge" (with prob 1) to meta-target - // no multiplication necessary - T alternateDistance = shortestPathDistances[currentNode]; // FIXME + // node only has one "virtual edge" (with prob as per targetProbMap) to meta-target + // FIXME: double check + T alternateDistance = shortestPathDistances[currentNode] * targetProbMap[currentNode]; if (alternateDistance > shortestPathDistances[metaTarget]) { shortestPathDistances[metaTarget] = alternateDistance; shortestPathPredecessors[metaTarget] = boost::optional(currentNode); @@ -232,9 +234,9 @@ namespace storm { assert(false); return utility::zero(); } else { - // edge must be "virtual edge" from target state to meta-target - assert(targetProbMap.count(tailNode) == 1); - return one(); + // edge must be "virtual edge" to meta-target + assert(isMetaTargetPredecessor(tailNode)); + return targetProbMap.at(tailNode); // FIXME double check } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index b78a0758a..1cda2eb99 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -103,7 +103,7 @@ namespace storm { BitVector initialStates; std::unordered_map targetProbMap; - std::vector graphPredecessors; // FIXME is a switch to BitVector a good idea here? + std::vector graphPredecessors; std::vector> shortestPathPredecessors; std::vector shortestPathSuccessors; std::vector shortestPathDistances; @@ -167,7 +167,7 @@ namespace storm { return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); } - inline bool isTargetState(state_t node) const { + inline bool isMetaTargetPredecessor(state_t node) const { return targetProbMap.count(node) == 1; } diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md index db5dcc326..f2beb801a 100644 --- a/src/utility/shortestPaths.md +++ b/src/utility/shortestPaths.md @@ -52,9 +52,8 @@ implied target state. This naturally corresponds to having a meta-target, except the probability of its incoming edges range over $(0,1]$ rather than being $1$. Thus, applying the term "target group" to the set of states with non-zero -transitions to the meta-target is now misleading (I suppose the correct term -would now be "meta-target predecessors"), but nevertheless it should work -exactly the same. [Right?] +transitions to the meta-target is now misleading[^1], but nevertheless it +should work exactly the same. [Right?] In terms of implementation, in `getEdgeDistance` as well as in the loop of the Dijkstra, the "virtual" edges to the meta-target were checked for and @@ -98,11 +97,14 @@ path to some node `u` plus an edge to `t`: Further, the shortest paths to some node are always computed in order and without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed before the 4-SP. Thus, we store the SPs in a linked list for each node, -with the k-th entry[^1] being the k-th SP to that node. +with the k-th entry[^2] being the k-th SP to that node. Thus for an SP as shown above we simply store the predecessor node (`u`) and the `k`, which allows us to look up the tail of the SP. By recursively looking up the tail (until it's empty), we reconstruct the entire path back-to-front. -[^1]: Which due to 0-based indexing has index `k-1`, of course! Damn it. +[^1]: I suppose the correct term would now be "meta-target predecessors". + In fact, I will rename all occurences of `target` in the source to + `metaTargetPredecessors` – clumsy but accurate. +[^2]: Which due to 0-based indexing has index `k-1`, of course! Damn it. From 67ce5cf18d9db7498fcb69804547e4f0d0aa73cb Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 18 Nov 2016 16:46:48 +0100 Subject: [PATCH 25/35] const& in signatures --- src/utility/shortestPaths.cpp | 4 ++-- src/utility/shortestPaths.h | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index c9ce0b608..8d1dd079f 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -7,7 +7,7 @@ namespace storm { namespace utility { namespace ksp { template - ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix transitionMatrix, std::unordered_map targetProbMap, BitVector initialStates) : + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, std::unordered_map const& targetProbMap, BitVector const& initialStates) : transitionMatrix(transitionMatrix), numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target metaTarget(transitionMatrix.getColumnCount()), // first unused state index @@ -28,7 +28,7 @@ namespace storm { } template - ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix transitionMatrix, std::vector targetProbVector, BitVector initialStates) + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates) : ShortestPathsGenerator(transitionMatrix, vectorToMap(targetProbVector), initialStates) {} // extracts the relevant info from the model and delegates to ctor above diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 1cda2eb99..67e857e5d 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -67,8 +67,8 @@ namespace storm { // a further alternative: use transition matrix of maybe-states // combined with target vector (e.g., the instantiated matrix/vector from SamplingModel); // in this case separately specifying a target makes no sense - ShortestPathsGenerator(storage::SparseMatrix transitionMatrix, std::vector targetProbVector, BitVector initialStates); - ShortestPathsGenerator(storage::SparseMatrix maybeTransitionMatrix, std::unordered_map targetProbMap, BitVector initialStates); + ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates); + ShortestPathsGenerator(storage::SparseMatrix const& maybeTransitionMatrix, std::unordered_map const& targetProbMap, BitVector const& initialStates); inline ~ShortestPathsGenerator(){} @@ -97,7 +97,7 @@ namespace storm { private: - storage::SparseMatrix transitionMatrix; + storage::SparseMatrix const& transitionMatrix; // FIXME: store reference instead (?) state_t numStates; // includes meta-target, i.e. states in model + 1 state_t metaTarget; BitVector initialStates; From 4bc92664167fdbc8fa6c3d480889fbe4f04289bf Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 20:29:27 +0100 Subject: [PATCH 26/35] redundant namespace refs rm --- src/utility/shortestPaths.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 8d1dd079f..dda452d5a 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -128,8 +128,8 @@ namespace storm { // the existing Dijkstra isn't working anyway AND // doesn't fully meet our requirements, so let's roll our own - T inftyDistance = utility::zero(); - T zeroDistance = utility::one(); + T inftyDistance = zero(); + T zeroDistance = one(); shortestPathDistances.resize(numStates, inftyDistance); shortestPathPredecessors.resize(numStates, boost::optional()); @@ -232,7 +232,7 @@ namespace storm { // there is no such edge // let's disallow that for now, because I'm not expecting it to happen assert(false); - return utility::zero(); + return zero(); } else { // edge must be "virtual edge" to meta-target assert(isMetaTargetPredecessor(tailNode)); From fe6804e16426e80b9a718f091a24210e7d5ba835 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 18 Nov 2016 16:52:07 +0100 Subject: [PATCH 27/35] KSP: matrix format conversion & lots of type stuff # Conflicts: # src/python/storm-tom.cpp # src/utility/shortestPaths.cpp # src/utility/shortestPaths.h # test/functional/utility/KSPTest.cpp # test/functional/utility/PdtmcInstantiationTest.cpp --- src/utility/shortestPaths.cpp | 32 +++++++------ src/utility/shortestPaths.h | 69 ++++++++++++++++++++++------- test/functional/utility/KSPTest.cpp | 16 +++---- 3 files changed, 79 insertions(+), 38 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index dda452d5a..ad25e2616 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -7,12 +7,16 @@ namespace storm { namespace utility { namespace ksp { template - ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, std::unordered_map const& targetProbMap, BitVector const& initialStates) : + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, + std::unordered_map const& targetProbMap, + BitVector const& initialStates, + MatrixFormat matrixFormat) : transitionMatrix(transitionMatrix), numStates(transitionMatrix.getColumnCount() + 1), // one more for meta-target metaTarget(transitionMatrix.getColumnCount()), // first unused state index initialStates(initialStates), - targetProbMap(targetProbMap) { + targetProbMap(targetProbMap), + matrixFormat(matrixFormat) { computePredecessors(); @@ -28,28 +32,29 @@ namespace storm { } template - ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates) - : ShortestPathsGenerator(transitionMatrix, vectorToMap(targetProbVector), initialStates) {} + ShortestPathsGenerator::ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, + std::vector const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat) + : ShortestPathsGenerator(transitionMatrix, vectorToMap(targetProbVector), initialStates, matrixFormat) {} // extracts the relevant info from the model and delegates to ctor above template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, BitVector const& targetBV) - : ShortestPathsGenerator(model->getTransitionMatrix(), allProbOneMap(targetBV), model->getInitialStates()) {} + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, BitVector const& targetBV) + : ShortestPathsGenerator(model.getTransitionMatrix(), allProbOneMap(targetBV), model.getInitialStates(), MatrixFormat::straight) {} // several alternative ways to specify the targets are provided, // each converts the targets and delegates to the ctor above // I admit it's kind of ugly, but actually pretty convenient (and I've wanted to try C++11 delegation) template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget) + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, state_t singleTarget) : ShortestPathsGenerator(model, std::vector{singleTarget}) {} template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, std::vector const& targetList) - : ShortestPathsGenerator(model, BitVector(model->getNumberOfStates(), targetList)) {} + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, std::vector const& targetList) + : ShortestPathsGenerator(model, BitVector(model.getNumberOfStates(), targetList)) {} template - ShortestPathsGenerator::ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel) - : ShortestPathsGenerator(model, model->getStates(targetLabel)) {} + ShortestPathsGenerator::ShortestPathsGenerator(Model const& model, std::string const& targetLabel) + : ShortestPathsGenerator(model, model.getStates(targetLabel)) {} template T ShortestPathsGenerator::getDistance(unsigned long k) { @@ -152,7 +157,8 @@ namespace storm { state_t otherNode = transition.getColumn(); // note that distances are probabilities, thus they are multiplied and larger is better - T alternateDistance = shortestPathDistances[currentNode] * transition.getValue(); + T alternateDistance = shortestPathDistances[currentNode] * convertDistance(currentNode, otherNode, transition.getValue()); + assert(zero() <= alternateDistance <= one()); // FIXME: there is a negative transition! SM gives us a placeholder! if (alternateDistance > shortestPathDistances[otherNode]) { shortestPathDistances[otherNode] = alternateDistance; shortestPathPredecessors[otherNode] = boost::optional(currentNode); @@ -225,7 +231,7 @@ namespace storm { for (auto const& transition : transitionMatrix.getRowGroup(tailNode)) { if (transition.getColumn() == headNode) { - return transition.getValue(); + return convertDistance(tailNode, headNode, transition.getValue()); } } diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 67e857e5d..fb1e0303c 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -23,9 +23,11 @@ namespace storm { namespace utility { namespace ksp { - typedef storage::sparse::state_type state_t; + using state_t = storage::sparse::state_type; + using OrderedStateList = std::vector; using BitVector = storage::BitVector; - typedef std::vector ordered_state_list_t; + + // -- helper structs/classes ----------------------------------------------------------------------------- template struct Path { @@ -46,29 +48,38 @@ namespace storm { } }; + // when using the raw matrix/vector invocation, this enum parameter + // forces the caller to declare whether the matrix has the evil I-P + // format, which requires back-conversion of the entries + enum class MatrixFormat { straight, iMinusP }; + // ------------------------------------------------------------------------------------------------------- template class ShortestPathsGenerator { public: + using Matrix = storage::SparseMatrix; + using StateProbMap = std::unordered_map; + using Model = models::sparse::Model; + /*! * Performs precomputations (including meta-target insertion and Dijkstra). * Modifications are done locally, `model` remains unchanged. * Target (group) cannot be changed. */ - ShortestPathsGenerator(std::shared_ptr> model, BitVector const& targetBV); + ShortestPathsGenerator(Model const& model, BitVector const& targetBV); // allow alternative ways of specifying the target, // all of which will be converted to BitVector and delegated to constructor above - ShortestPathsGenerator(std::shared_ptr> model, state_t singleTarget); - ShortestPathsGenerator(std::shared_ptr> model, std::vector const& targetList); - ShortestPathsGenerator(std::shared_ptr> model, std::string const& targetLabel = "target"); + ShortestPathsGenerator(Model const& model, state_t singleTarget); + ShortestPathsGenerator(Model const& model, std::vector const& targetList); + ShortestPathsGenerator(Model const& model, std::string const& targetLabel = "target"); // a further alternative: use transition matrix of maybe-states // combined with target vector (e.g., the instantiated matrix/vector from SamplingModel); // in this case separately specifying a target makes no sense - ShortestPathsGenerator(storage::SparseMatrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates); - ShortestPathsGenerator(storage::SparseMatrix const& maybeTransitionMatrix, std::unordered_map const& targetProbMap, BitVector const& initialStates); + ShortestPathsGenerator(Matrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat); + ShortestPathsGenerator(Matrix const& maybeTransitionMatrix, StateProbMap const& targetProbMap, BitVector const& initialStates, MatrixFormat matrixFormat); inline ~ShortestPathsGenerator(){} @@ -93,19 +104,21 @@ namespace storm { * Computes KSP if not yet computed. * @throws std::invalid_argument if no such k-shortest path exists */ - ordered_state_list_t getPathAsList(unsigned long k); + OrderedStateList getPathAsList(unsigned long k); private: - storage::SparseMatrix const& transitionMatrix; // FIXME: store reference instead (?) + Matrix const& transitionMatrix; // FIXME: store reference instead (?) state_t numStates; // includes meta-target, i.e. states in model + 1 state_t metaTarget; BitVector initialStates; - std::unordered_map targetProbMap; + StateProbMap targetProbMap; + + MatrixFormat matrixFormat; - std::vector graphPredecessors; + std::vector graphPredecessors; std::vector> shortestPathPredecessors; - std::vector shortestPathSuccessors; + std::vector shortestPathSuccessors; std::vector shortestPathDistances; std::vector>> kShortestPaths; @@ -163,6 +176,7 @@ namespace storm { // --- tiny helper fcts --- + inline bool isInitialState(state_t node) const { return find(initialStates.begin(), initialStates.end(), node) != initialStates.end(); } @@ -171,25 +185,45 @@ namespace storm { return targetProbMap.count(node) == 1; } - /** + // I dislike this. But it is necessary if we want to handle those ugly I-P matrices + inline T convertDistance(state_t tailNode, state_t headNode, T distance) const { + if (matrixFormat == MatrixFormat::straight) { + return distance; + } else { + if (tailNode == headNode) { + // diagonal: 1-p = dist + return one() - distance; + } else { + // non-diag: -p = dist + return zero() - distance; + } + } + } + + /*! * Returns a map where each state of the input BitVector is mapped to 1 (`one`). */ - inline std::unordered_map allProbOneMap(BitVector bitVector) const { - std::unordered_map stateProbMap; + inline StateProbMap allProbOneMap(BitVector bitVector) const { + StateProbMap stateProbMap; for (state_t node : bitVector) { stateProbMap.emplace(node, one()); // FIXME check rvalue warning (here and below) } return stateProbMap; } + /*! + * Given a vector of probabilities so that the `i`th entry corresponds to the + * probability of state `i`, returns an equivalent map of only the non-zero entries. + */ inline std::unordered_map vectorToMap(std::vector probVector) const { assert(probVector.size() == numStates); std::unordered_map stateProbMap; - // non-zero entries (i.e. true transitions) are added to the map for (state_t i = 0; i < probVector.size(); i++) { T probEntry = probVector[i]; + + // only non-zero entries (i.e. true transitions) are added to the map if (probEntry != 0) { assert(0 < probEntry <= 1); stateProbMap.emplace(i, probEntry); @@ -198,6 +232,7 @@ namespace storm { return stateProbMap; } + // ----------------------- }; } diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index d1c9a2f8f..2389f3f1c 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -26,7 +26,7 @@ TEST(KSPTest, dijkstra) { auto model = buildExampleModel(); storm::utility::ksp::state_t testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(1); EXPECT_DOUBLE_EQ(0.015859334652581887, dist); @@ -36,7 +36,7 @@ TEST(KSPTest, singleTarget) { auto model = buildExampleModel(); storm::utility::ksp::state_t testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(100); EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); @@ -46,7 +46,7 @@ TEST(KSPTest, reentry) { auto model = buildExampleModel(); storm::utility::ksp::state_t testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(100); EXPECT_DOUBLE_EQ(1.5231305000339649e-06, dist); @@ -60,7 +60,7 @@ TEST(KSPTest, groupTarget) { auto model = buildExampleModel(); auto groupTarget = std::vector{50, 90}; - auto spg = storm::utility::ksp::ShortestPathsGenerator(model, groupTarget); + auto spg = storm::utility::ksp::ShortestPathsGenerator(*model, groupTarget); // this path should lead to 90 double dist1 = spg.getDistance(8); @@ -79,7 +79,7 @@ TEST(KSPTest, kTooLargeException) { auto model = buildExampleModel(); storm::utility::ksp::state_t testState = 1; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); ASSERT_THROW(spg.getDistance(2), std::invalid_argument); } @@ -88,7 +88,7 @@ TEST(KSPTest, kspStateSet) { auto model = buildExampleModel(); storm::utility::ksp::state_t testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); for (auto s : std::vector{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) { @@ -104,10 +104,10 @@ TEST(KSPTest, kspPathAsList) { auto model = buildExampleModel(); storm::utility::ksp::state_t testState = 300; - storm::utility::ksp::ShortestPathsGenerator spg(model, testState); + storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); // TODO: use path that actually has a loop or something to make this more interesting - auto reference = storm::utility::ksp::ordered_state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; + auto reference = storm::utility::ksp::OrderedStateList{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; auto list = spg.getPathAsList(7); EXPECT_EQ(list, reference); From 83445f67c319aaadd3bfb7fdc98f9b2a43164856 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 18 Nov 2016 16:55:05 +0100 Subject: [PATCH 28/35] kSP: a few more comments --- src/utility/shortestPaths.cpp | 29 ++++++++++++++++++++++++----- src/utility/shortestPaths.md | 10 +++++++--- 2 files changed, 31 insertions(+), 8 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index ad25e2616..2a7c21285 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,8 +1,16 @@ #include #include +#include + +#include "macros.h" #include "shortestPaths.h" #include "graph.h" +// FIXME: I've accidentally used k=0 *twice* now without realizing that k>=1 is required! +// Accessing zero should trigger a warning! +// (Also, did I document this? I think so, somewhere. I went with k>=1 because +// that's what the KSP paper used, but in retrospect k>=0 seems more intuitive ...) + namespace storm { namespace utility { namespace ksp { @@ -249,9 +257,13 @@ namespace storm { template void ShortestPathsGenerator::computeNextPath(state_t node, unsigned long k) { + assert(k >= 2); // Dijkstra is used for k=1 assert(kShortestPaths[node].size() == k - 1); // if not, the previous SP must not exist + // TODO: I could extract the candidate generation to make this function more succinct if (k == 2) { + // Step B.1 in J&M paper + Path shortestPathToNode = kShortestPaths[node][1 - 1]; // never forget index shift :-| for (state_t predecessor : graphPredecessors[node]) { @@ -271,7 +283,9 @@ namespace storm { } } - if (k > 2 || !isInitialState(node)) { + if (not (k == 2 && isInitialState(node))) { + // Steps B.2-5 in J&M paper + // the (k-1)th shortest path (i.e., one better than the one we want to compute) Path previousShortestPath = kShortestPaths[node][k - 1 - 1]; // oh god, I forgot index shift AGAIN @@ -297,9 +311,10 @@ namespace storm { }; candidatePaths[node].insert(pathToPredecessorPlusEdge); } - // else there was no path; TODO: does this need handling? + // else there was no path; TODO: does this need handling? -- yes, but not here (because the step B.1 may have added candidates) } + // Step B.6 in J&M paper if (!candidatePaths[node].empty()) { Path minDistanceCandidate = *(candidatePaths[node].begin()); for (auto path : candidatePaths[node]) { @@ -310,6 +325,9 @@ namespace storm { candidatePaths[node].erase(std::find(candidatePaths[node].begin(), candidatePaths[node].end(), minDistanceCandidate)); kShortestPaths[node].push_back(minDistanceCandidate); + } else { + // TODO: kSP does not exist. this is handled later, but it would be nice to catch it as early as possble, wouldn't it? + STORM_LOG_TRACE("KSP: no candidates, this will trigger nonexisting ksp after exiting these recursions. TODO: handle here"); } } @@ -320,9 +338,10 @@ namespace storm { for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) { computeNextPath(metaTarget, nextK); if (kShortestPaths[metaTarget].size() < nextK) { - //std::cout << std::endl << "--> DEBUG: Last path: k=" << (nextK - 1) << ":" << std::endl; - //printKShortestPath(metaTarget, nextK - 1); - //std::cout << "---------" << "No other path exists!" << std::endl; + unsigned long lastExistingK = nextK - 1; + STORM_LOG_DEBUG("KSP throws (as expected) due to nonexistence -- maybe this is unhandled and causes the Python interface to segfault?"); + STORM_LOG_DEBUG("last existing k-SP has k=" + std::to_string(lastExistingK)); + STORM_LOG_DEBUG("maybe this is unhandled and causes the Python interface to segfault?"); throw std::invalid_argument("k-SP does not exist for k=" + std::to_string(k)); } } diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md index f2beb801a..13dc96376 100644 --- a/src/utility/shortestPaths.md +++ b/src/utility/shortestPaths.md @@ -75,7 +75,7 @@ This is a common feature if the target state is a sink; but we are not interested in such paths. (In fact, ideally we'd like to see paths whose node-intersection with all -shorter paths is non-empty (which is an even stronger statement than +shorter paths is non-empty [^2] (which is an even stronger statement than loop-free-ness of paths), because we want to take a union of those node sets. But that's a different matter.) @@ -97,7 +97,7 @@ path to some node `u` plus an edge to `t`: Further, the shortest paths to some node are always computed in order and without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed before the 4-SP. Thus, we store the SPs in a linked list for each node, -with the k-th entry[^2] being the k-th SP to that node. +with the k-th entry[^3] being the k-th SP to that node. Thus for an SP as shown above we simply store the predecessor node (`u`) and the `k`, which allows us to look up the tail of the SP. @@ -107,4 +107,8 @@ the entire path back-to-front. [^1]: I suppose the correct term would now be "meta-target predecessors". In fact, I will rename all occurences of `target` in the source to `metaTargetPredecessors` – clumsy but accurate. -[^2]: Which due to 0-based indexing has index `k-1`, of course! Damn it. +[^2]: (2016-08-20:) Is this correct? Didn't I mean that the path should + contain new nodes, i.e., non-emptiness of + ((nodes in path) set-minus (union(nodes in shorter paths)))? + Yeah, I'm pretty sure that's what I meant. +[^3]: Which due to 0-based indexing has index `k-1`, of course! Damn it. From 0c6574c740284aff812a7a9d538126202299190a Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 18 Nov 2016 16:58:18 +0100 Subject: [PATCH 29/35] rm questionable assertion --- src/utility/shortestPaths.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index fb1e0303c..2ffdcc13a 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -216,7 +216,7 @@ namespace storm { * probability of state `i`, returns an equivalent map of only the non-zero entries. */ inline std::unordered_map vectorToMap(std::vector probVector) const { - assert(probVector.size() == numStates); + //assert(probVector.size() == numStates); // numStates may not yet be initialized! // still true? std::unordered_map stateProbMap; From 71a54a842c71410ab13bb89848404f4445ccc298 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Wed, 23 Nov 2016 16:44:49 +0100 Subject: [PATCH 30/35] comment / clarification --- src/utility/shortestPaths.cpp | 2 +- src/utility/shortestPaths.h | 4 ++-- test/functional/utility/KSPTest.cpp | 7 ------- 3 files changed, 3 insertions(+), 10 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 2a7c21285..7912f15ee 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -113,7 +113,7 @@ namespace storm { template void ShortestPathsGenerator::computePredecessors() { - assert(numStates - 1 == transitionMatrix.getRowCount()); + assert(transitionMatrix.hasTrivialRowGrouping()); // one more for meta-target graphPredecessors.resize(numStates); diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h index 2ffdcc13a..c34439401 100644 --- a/src/utility/shortestPaths.h +++ b/src/utility/shortestPaths.h @@ -93,7 +93,7 @@ namespace storm { /*! * Returns the states that occur in the KSP. - * For a path-traversal (in order and with duplicates), see `getKSP`. + * For a path-traversal (in order and with duplicates), see `getPathAsList`. * Computes KSP if not yet computed. * @throws std::invalid_argument if no such k-shortest path exists */ @@ -108,7 +108,7 @@ namespace storm { private: - Matrix const& transitionMatrix; // FIXME: store reference instead (?) + Matrix const& transitionMatrix; state_t numStates; // includes meta-target, i.e. states in model + 1 state_t metaTarget; BitVector initialStates; diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index 2389f3f1c..ef1e8a7b5 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -112,10 +112,3 @@ TEST(KSPTest, kspPathAsList) { EXPECT_EQ(list, reference); } - - -//---------------------------- -// v---- PLAYGROUND ----v -//---------------------------- - -// (empty) From 3915a491cfafdb96eeff46f59253fa978e1b8684 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Wed, 23 Nov 2016 16:46:53 +0100 Subject: [PATCH 31/35] factor out test state --- test/functional/utility/KSPTest.cpp | 32 ++++++++++------------------- 1 file changed, 11 insertions(+), 21 deletions(-) diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index ef1e8a7b5..dfdcd8a23 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -22,10 +22,11 @@ std::shared_ptr> buildExampleModel() { return storm::builder::ExplicitModelBuilder(program).build(); } -TEST(KSPTest, dijkstra) { - auto model = buildExampleModel(); +const storm::utility::ksp::state_t testState = 300; +const storm::utility::ksp::state_t stateWithOnlyOnePath = 1; - storm::utility::ksp::state_t testState = 300; +TEST(KSPTest, dijkstra) { + auto model = buildExampleModel(); storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(1); @@ -33,9 +34,7 @@ TEST(KSPTest, dijkstra) { } TEST(KSPTest, singleTarget) { - auto model = buildExampleModel(); - - storm::utility::ksp::state_t testState = 300; + auto model = buildExampleModel(); storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(100); @@ -43,9 +42,7 @@ TEST(KSPTest, singleTarget) { } TEST(KSPTest, reentry) { - auto model = buildExampleModel(); - - storm::utility::ksp::state_t testState = 300; + auto model = buildExampleModel(); storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); double dist = spg.getDistance(100); @@ -57,8 +54,7 @@ TEST(KSPTest, reentry) { } TEST(KSPTest, groupTarget) { - auto model = buildExampleModel(); - + auto model = buildExampleModel(); auto groupTarget = std::vector{50, 90}; auto spg = storm::utility::ksp::ShortestPathsGenerator(*model, groupTarget); @@ -76,18 +72,14 @@ TEST(KSPTest, groupTarget) { } TEST(KSPTest, kTooLargeException) { - auto model = buildExampleModel(); - - storm::utility::ksp::state_t testState = 1; - storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); + auto model = buildExampleModel(); + storm::utility::ksp::ShortestPathsGenerator spg(*model, stateWithOnlyOnePath); ASSERT_THROW(spg.getDistance(2), std::invalid_argument); } TEST(KSPTest, kspStateSet) { - auto model = buildExampleModel(); - - storm::utility::ksp::state_t testState = 300; + auto model = buildExampleModel(); storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); @@ -101,9 +93,7 @@ TEST(KSPTest, kspStateSet) { } TEST(KSPTest, kspPathAsList) { - auto model = buildExampleModel(); - - storm::utility::ksp::state_t testState = 300; + auto model = buildExampleModel(); storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); // TODO: use path that actually has a loop or something to make this more interesting From 79f3e13906a2911e9f59b899aab0481dcc949eba Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Wed, 23 Nov 2016 17:05:58 +0100 Subject: [PATCH 32/35] change KSP test reference values to whatever they currently are (and hoping for the best) --- test/functional/utility/KSPTest.cpp | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index dfdcd8a23..115eab396 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -22,7 +22,10 @@ std::shared_ptr> buildExampleModel() { return storm::builder::ExplicitModelBuilder(program).build(); } -const storm::utility::ksp::state_t testState = 300; +// NOTE: these are hardcoded (obviously), but the model's state indices might change +// (e.g., when the parser or model builder are changed) +// [state 296 seems to be the new index of the old state 300 (checked a few ksps' probs)] +const storm::utility::ksp::state_t testState = 296; const storm::utility::ksp::state_t stateWithOnlyOnePath = 1; TEST(KSPTest, dijkstra) { @@ -58,17 +61,18 @@ TEST(KSPTest, groupTarget) { auto groupTarget = std::vector{50, 90}; auto spg = storm::utility::ksp::ShortestPathsGenerator(*model, groupTarget); + // FIXME comments are outdated (but does it even matter?) // this path should lead to 90 double dist1 = spg.getDistance(8); - EXPECT_DOUBLE_EQ(7.3796982335999988e-06, dist1); + EXPECT_DOUBLE_EQ(0.00018449245583999996, dist1); // this one to 50 double dist2 = spg.getDistance(9); - EXPECT_DOUBLE_EQ(3.92e-06, dist2); + EXPECT_DOUBLE_EQ(0.00018449245583999996, dist2); // this one to 90 again double dist3 = spg.getDistance(12); - EXPECT_DOUBLE_EQ(3.6160521344640002e-06, dist3); + EXPECT_DOUBLE_EQ(7.5303043199999984e-06, dist3); } TEST(KSPTest, kTooLargeException) { @@ -83,13 +87,13 @@ TEST(KSPTest, kspStateSet) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); - for (auto s : std::vector{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) { + for (auto s : std::vector{0, 1, 3, 5, 7, 10, 14, 19, 25, 29, 33, 36, 40, 44, 50, 56, 62, 70, 77, 85, 92, 98, 104, 112, 119, 127, 134, 140, 146, 154, 161, 169, 176, 182, 188, 196, 203, 211, 218, 224, 230, 238, 245, 253, 260, 266, 272, 281, 288, 296}) { referenceBV.set(s, true); } auto bv = spg.getStates(7); - EXPECT_EQ(bv, referenceBV); + EXPECT_EQ(referenceBV, bv); } TEST(KSPTest, kspPathAsList) { @@ -97,8 +101,8 @@ TEST(KSPTest, kspPathAsList) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); // TODO: use path that actually has a loop or something to make this more interesting - auto reference = storm::utility::ksp::OrderedStateList{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}; + auto reference = storm::utility::ksp::OrderedStateList{296, 288, 281, 272, 266, 260, 253, 245, 238, 230, 224, 218, 211, 203, 196, 188, 182, 176, 169, 161, 154, 146, 140, 134, 127, 119, 112, 104, 98, 92, 85, 77, 70, 62, 56, 50, 44, 36, 29, 40, 33, 25, 19, 14, 10, 7, 5, 3, 1, 0}; auto list = spg.getPathAsList(7); - EXPECT_EQ(list, reference); + EXPECT_EQ(reference, list); } From 6ec05a942d3816f3b28d4bd0cb2a255abd31b216 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Wed, 23 Nov 2016 17:36:24 +0100 Subject: [PATCH 33/35] rm accidentally reintroduced files (don't worry they are small) --- test/functional/builder/crowds-5-4.pm | 69 --------------------------- test/performance/utility/KSPTest.cpp | 44 ----------------- 2 files changed, 113 deletions(-) delete mode 100644 test/functional/builder/crowds-5-4.pm delete mode 100644 test/performance/utility/KSPTest.cpp diff --git a/test/functional/builder/crowds-5-4.pm b/test/functional/builder/crowds-5-4.pm deleted file mode 100644 index 0eb518bf6..000000000 --- a/test/functional/builder/crowds-5-4.pm +++ /dev/null @@ -1,69 +0,0 @@ -dtmc - -// probability of forwarding -const double PF = 0.8; -const double notPF = .2; // must be 1-PF -// probability that a crowd member is bad -const double badC = .167; - // probability that a crowd member is good -const double goodC = 0.833; -// Total number of protocol runs to analyze -const int TotalRuns = 4; -// size of the crowd -const int CrowdSize = 5; - -module crowds - // protocol phase - phase: [0..4] init 0; - - // crowd member good (or bad) - good: bool init false; - - // number of protocol runs - runCount: [0..TotalRuns] init 0; - - // observe_i is the number of times the attacker observed crowd member i - observe0: [0..TotalRuns] init 0; - - observe1: [0..TotalRuns] init 0; - - observe2: [0..TotalRuns] init 0; - - observe3: [0..TotalRuns] init 0; - - observe4: [0..TotalRuns] init 0; - - // the last seen crowd member - lastSeen: [0..CrowdSize - 1] init 0; - - // get the protocol started - [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); - - // decide whether crowd member is good or bad according to given probabilities - [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); - - // if the current member is a good member, update the last seen index (chosen uniformly) - [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); - - // if the current member is a bad member, record the most recently seen index - [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); - [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); - [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); - [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); - [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); - - // good crowd members forward with probability PF and deliver otherwise - [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); - - // deliver the message and start over - [] phase=4 -> 1: (phase'=0); - -endmodule - -label "observe0Greater1" = observe0>1; -label "observe1Greater1" = observe1>1; -label "observe2Greater1" = observe2>1; -label "observe3Greater1" = observe3>1; -label "observe4Greater1" = observe4>1; -label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; -label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; diff --git a/test/performance/utility/KSPTest.cpp b/test/performance/utility/KSPTest.cpp deleted file mode 100644 index ea43f9826..000000000 --- a/test/performance/utility/KSPTest.cpp +++ /dev/null @@ -1,44 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/parser/PrismParser.h" -#include "src/models/sparse/Dtmc.h" -#include "src/builder/ExplicitPrismModelBuilder.h" -#include "src/utility/graph.h" -#include "src/utility/shortestPaths.cpp" - -const bool VERBOSE = true; - -TEST(KSPTest, crowdsSpeed) { - if (VERBOSE) std::cout << "Parsing crowds-5-4.pm file and building model ... " << std::endl; - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-4.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); - - if (VERBOSE) std::cout << "Initializing ShortestPathsGenerator ..." << std::endl; - // timekeeping taken from http://en.cppreference.com/w/cpp/chrono#Example - std::chrono::time_point startTime = std::chrono::system_clock::now(); - - auto target = "observe0Greater1"; - storm::utility::ksp::ShortestPathsGenerator spg(model, target); - - storm::storage::BitVector accStates(model->getNumberOfStates(), false); - double accumProb = 0; - - if (VERBOSE) std::cout << "Accumulating shortest paths ..." << std::endl; - for (int i = 1; accumProb < 0.15; i++) { - double pathProb = spg.getDistance(i); - accumProb += pathProb; - - storm::storage::BitVector statesInPath = spg.getStates(i); - accStates |= statesInPath; - - if (i % 50000 == 0) { - if (VERBOSE) std::cout << " --> It/States/AccProb/PathProb: " << i << " / " << accStates.getNumberOfSetBits() << " / " << accumProb << " / " << pathProb << std::endl; - } - } - - std::chrono::duration elapsedSeconds = std::chrono::system_clock::now() - startTime; - if (VERBOSE) std::cout << "Done. Num of states: " << accStates.getNumberOfSetBits() << ". Seconds: " << elapsedSeconds.count() << std::endl; - - EXPECT_LE(elapsedSeconds.count(), 5); // should take less than 5 seconds on a modern PC -} From 7d06eee4ea1716ebfe2bc523f531b522535dc285 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Wed, 23 Nov 2016 17:44:16 +0100 Subject: [PATCH 34/35] adjusted KSP test model path --- test/functional/utility/KSPTest.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index 115eab396..e3c127f4b 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -16,7 +16,7 @@ // FIXME: (almost) all of these fail; the question is: is there actually anything wrong or does the new parser yield a different order of states? std::shared_ptr> buildExampleModel() { - std::string prismModelPath = STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"; + std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"; storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); return storm::builder::ExplicitModelBuilder(program).build(); From 87e8af98528ecaba2fbf5976be16db8436f86959 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Tue, 20 Dec 2016 17:00:13 +0100 Subject: [PATCH 35/35] moved ksp stuff to right location fix include --- src/{ => storm}/utility/shortestPaths.cpp | 0 src/{ => storm}/utility/shortestPaths.h | 4 +- .../test}/utility/KSPTest.cpp | 12 +- src/utility/shortestPaths.md | 114 ------------------ 4 files changed, 8 insertions(+), 122 deletions(-) rename src/{ => storm}/utility/shortestPaths.cpp (100%) rename src/{ => storm}/utility/shortestPaths.h (99%) rename {test/functional => src/test}/utility/KSPTest.cpp (94%) delete mode 100644 src/utility/shortestPaths.md diff --git a/src/utility/shortestPaths.cpp b/src/storm/utility/shortestPaths.cpp similarity index 100% rename from src/utility/shortestPaths.cpp rename to src/storm/utility/shortestPaths.cpp diff --git a/src/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h similarity index 99% rename from src/utility/shortestPaths.h rename to src/storm/utility/shortestPaths.h index c34439401..e7cb38df6 100644 --- a/src/utility/shortestPaths.h +++ b/src/storm/utility/shortestPaths.h @@ -4,8 +4,8 @@ #include #include #include -#include "src/models/sparse/Model.h" -#include "src/storage/sparse/StateType.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/sparse/StateType.h" #include "constants.h" // NOTE: You'll (eventually) find the usual API documentation below; diff --git a/test/functional/utility/KSPTest.cpp b/src/test/utility/KSPTest.cpp similarity index 94% rename from test/functional/utility/KSPTest.cpp rename to src/test/utility/KSPTest.cpp index e3c127f4b..3d28ccae6 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/src/test/utility/KSPTest.cpp @@ -1,12 +1,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/builder/ExplicitModelBuilder.h" -#include "src/models/sparse/Dtmc.h" -#include "src/parser/PrismParser.h" -#include "src/storage/SymbolicModelDescription.h" -#include "src/utility/graph.h" -#include "src/utility/shortestPaths.cpp" +#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/parser/PrismParser.h" +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/utility/graph.h" +#include "storm/utility/shortestPaths.cpp" // NOTE: The KSPs / distances of these tests were generated by the // KSP-Generator itself and checked for gross implausibility, but no diff --git a/src/utility/shortestPaths.md b/src/utility/shortestPaths.md deleted file mode 100644 index 13dc96376..000000000 --- a/src/utility/shortestPaths.md +++ /dev/null @@ -1,114 +0,0 @@ -# k-shortest Path Generator -[This is a collection of random notes for now, to help me remember -the design decisions and the rationale behind them.] - -## Differences from REA algorithm -This class closely follows the Jimenez-Marzal REA algorithm. -However, there are some notable deviations in the way targets and shortest -paths are defined. - -### Target groups -Firstly, instead of a single target state, a group of target states is -considered. It is clear that this can achieved by removing all outgoing -transitions (other than self-loops, but this is moot due to not allowing -non-minimal paths -- see below) and instead introducing edges to a new sink -state that serves as a meta-target. - - - -I chose to implement this by modifying the precomputation results, meaning -that they are only valid for a fixed group of target states. Thus, the -target group is required in the constructor. (It would have been possible to -allow for interchangeable target groups, but I don't anticipate that use -case.) - -#### Special case: Using Matrix/Vector from SamplingModel - -The class has been updated to support the matrix/vector that `SamplingModel` -generates (as an instance of a PDTMC) as input. This is in fact closely -related to the target groups, since it works as follows: - -The input is a (sub-stochastic) transition matrix of the maybe-states (only!) -and a vector (again over the maybe-states) with the probabilities to an -implied target state. - -This naturally corresponds to having a meta-target, except the probability -of its incoming edges range over $(0,1]$ rather than being $1$. -Thus, applying the term "target group" to the set of states with non-zero -transitions to the meta-target is now misleading[^1], but nevertheless it -should work exactly the same. [Right?] - -In terms of implementation, in `getEdgeDistance` as well as in the loop of -the Dijkstra, the "virtual" edges to the meta-target were checked for and -set to probability $1$; this must now be changed to use the probability as -indicated in the `targetProbVector` if this input format is used. - -### Minimality of paths -Secondly, we define shortest paths as "minimal" shortest paths in the -following sense: The path may not visit any target state except at the -end. As a corollary, no KSP (to a target node) may be a prefix of another. -This in particular forbids shortest path progressions such as these: - - 1-SP: 1 2 3 - 2-SP: 1 2 3 3 - 3-SP: 1 2 3 3 3 - ... - -This is a common feature if the target state is a sink; but we are not -interested in such paths. - -(In fact, ideally we'd like to see paths whose node-intersection with all -shorter paths is non-empty [^2] (which is an even stronger statement than -loop-free-ness of paths), because we want to take a union of those node -sets. But that's a different matter.) - - -## Data structures, in particular: Path representation - -The implicit shortest path representation that J&M describe in the paper -is used, except that indices rather than back-pointers are stored to -refer to the tail of the path. -[Maybe pointers would be faster? STL vector access via index should be -pretty fast too, though, and less error-prone.] - -A bit more detail (recap of the paper): -All shortest paths (from `s` to `t`) can be described as some k-shortest -path to some node `u` plus an edge to `t`: - - s ~~k-shortest path~~> u --> t - -Further, the shortest paths to some node are always computed in order and -without gaps, e.g., the 1, 2, 3-shortest paths to `t` will be computed -before the 4-SP. Thus, we store the SPs in a linked list for each node, -with the k-th entry[^3] being the k-th SP to that node. - -Thus for an SP as shown above we simply store the predecessor node (`u`) -and the `k`, which allows us to look up the tail of the SP. -By recursively looking up the tail (until it's empty), we reconstruct -the entire path back-to-front. - -[^1]: I suppose the correct term would now be "meta-target predecessors". - In fact, I will rename all occurences of `target` in the source to - `metaTargetPredecessors` – clumsy but accurate. -[^2]: (2016-08-20:) Is this correct? Didn't I mean that the path should - contain new nodes, i.e., non-emptiness of - ((nodes in path) set-minus (union(nodes in shorter paths)))? - Yeah, I'm pretty sure that's what I meant. -[^3]: Which due to 0-based indexing has index `k-1`, of course! Damn it.