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<T>(model, bitvectorToList(model->getStates(targetLabel))) {}
template <typename T>
- T ShortestPathsGenerator<T>::computeKSP(unsigned long k) {
- unsigned long alreadyComputedK = kShortestPaths[metaTarget].size();
+ T ShortestPathsGenerator<T>::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<T>(); // TODO: throw exception or something
- }
+ template <typename T>
+ storage::BitVector ShortestPathsGenerator<T>::getStates(unsigned long k) {
+ computeKSP(k);
+ storage::BitVector stateSet(numStates - 1, false); // no meta-target
+
+ Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
+ boost::optional<state_t> 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 <typename T>
+ state_list_t ShortestPathsGenerator<T>::getPathAsList(unsigned long k) {
+ computeKSP(k);
+
+ state_list_t backToFrontList;
+
+ Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
+ boost::optional<state_t> 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 <typename T>
@@ -269,6 +296,21 @@ namespace storm {
}
}
+ template <typename T>
+ void ShortestPathsGenerator<T>::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 <typename T>
void ShortestPathsGenerator<T>::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<models::sparse::Model<T>> model, storage::BitVector const& targetBV);
ShortestPathsGenerator(std::shared_ptr<models::sparse::Model<T>> 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<double> 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<double> 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<double> 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
- auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(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<double>(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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+
+ storm::storage::sparse::state_type testState = 1;
+ storm::utility::ksp::ShortestPathsGenerator<double> 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+
+ storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::ShortestPathsGenerator<double> 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+
+ storm::storage::sparse::state_type testState = 300;
+ storm::utility::ksp::ShortestPathsGenerator<double> 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);
+}