From 44b3a9108e72137cc2d662e6e5da4048029e9c5e Mon Sep 17 00:00:00 2001 From: tomjanson Date: Fri, 12 Feb 2016 22:39:08 +0100 Subject: [PATCH] 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);