Browse Source

interactive debug in test

Former-commit-id: 161afac16e [formerly 17962bf200]
Former-commit-id: 53dc4819cf
tempestpy_adaptions
tomjanson 9 years ago
committed by Tom Janson
parent
commit
140597fb90
  1. 17
      src/test/utility/GraphTest.cpp
  2. 23
      src/utility/shortestPaths.cpp
  3. 11
      src/utility/shortestPaths.h

17
src/test/utility/GraphTest.cpp

@ -268,18 +268,29 @@ TEST(GraphTest, ExplicitProb01MinMax) {
TEST(GraphTest, kshortest) { 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 "/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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
model->printModelInformationToStream(std::cout); model->printModelInformationToStream(std::cout);
std::cout << "Initializing ShortestPathsGenerator ..." << std::endl;
storm::utility::shortestPaths::ShortestPathsGenerator<double> shortestPathsGenerator(model); storm::utility::shortestPaths::ShortestPathsGenerator<double> 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 // TODO: actually write tests here

23
src/utility/shortestPaths.cpp

@ -55,7 +55,7 @@ namespace storm {
// set serves as priority queue with unique membership // set serves as priority queue with unique membership
// default comparison on pair actually works fine if distance is the first entry // default comparison on pair actually works fine if distance is the first entry
std::set<std::pair<T, state_t>, std::greater_equal<std::pair<T, state_t>>> dijkstraQueue;
std::set<std::pair<T, state_t>, std::greater<std::pair<T, state_t>>> dijkstraQueue;
for (state_t initialState : model->getInitialStates()) { for (state_t initialState : model->getInitialStates()) {
shortestPathDistances[initialState] = zeroDistance; shortestPathDistances[initialState] = zeroDistance;
@ -192,23 +192,26 @@ namespace storm {
} }
template <typename T> template <typename T>
Path<T> ShortestPathsGenerator<T>::getKShortest(state_t node, unsigned long k) {
void ShortestPathsGenerator<T>::getKShortest(state_t node, unsigned long k) {
unsigned long alreadyComputedK = kShortestPaths[node].size(); 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++) { for (unsigned long nextK = alreadyComputedK + 1; nextK <= k; nextK++) {
computeNextPath(node, nextK); computeNextPath(node, nextK);
if (kShortestPaths[node].size() < 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 <typename T> template <typename T>

11
src/utility/shortestPaths.h

@ -7,6 +7,15 @@
#include "src/storage/sparse/StateType.h" #include "src/storage/sparse/StateType.h"
#include "constants.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 storm {
namespace utility { namespace utility {
namespace shortestPaths { namespace shortestPaths {
@ -62,7 +71,7 @@ namespace storm {
~ShortestPathsGenerator(); ~ShortestPathsGenerator();
// TODO: think about suitable output format // TODO: think about suitable output format
Path<T> getKShortest(state_t node, unsigned long k);
void getKShortest(state_t node, unsigned long k);
private: private:

Loading…
Cancel
Save