From fbee00e448a01ecb4e30d51b722a27e032df2330 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sun, 8 Nov 2015 22:39:02 +0100 Subject: [PATCH] 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); +}