sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

KSP output as BitVector or list 

Former-commit-id: f8a74864f7 [formerly 3b61d8d476]
Former-commit-id: 4fe402ae83
tempestpy_adaptions
tomjanson 9 years ago
committed by Tom Janson
parent
b89d3f289a
commit
fbee00e448
3 changed files with 135 additions and 28 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 68
      src/utility/shortestPaths.cpp
  2. 33
      src/utility/shortestPaths.h
  3. 60
      test/functional/utility/KSPTest.cpp

68
src/utility/shortestPaths.cpp
View File

@ -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;
}
return stateSet;
}
//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 <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

33
src/utility/shortestPaths.h
View File

@ -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);

60
test/functional/utility/KSPTest.cpp
View File

@ -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);
}
Write Preview
Loading…
Cancel
Save