You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
44 lines
2.0 KiB
44 lines
2.0 KiB
#include "gtest/gtest.h"
|
|
#include "storm-config.h"
|
|
|
|
#include "src/parser/PrismParser.h"
|
|
#include "src/models/sparse/Dtmc.h"
|
|
#include "src/builder/ExplicitPrismModelBuilder.h"
|
|
#include "src/utility/graph.h"
|
|
#include "src/utility/shortestPaths.cpp"
|
|
|
|
const bool VERBOSE = true;
|
|
|
|
TEST(KSPTest, crowdsSpeed) {
|
|
if (VERBOSE) std::cout << "Parsing crowds-5-4.pm file and building model ... " << std::endl;
|
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-4.pm");
|
|
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
|
|
|
|
if (VERBOSE) std::cout << "Initializing ShortestPathsGenerator ..." << std::endl;
|
|
// timekeeping taken from http://en.cppreference.com/w/cpp/chrono#Example
|
|
std::chrono::time_point<std::chrono::system_clock> startTime = std::chrono::system_clock::now();
|
|
|
|
auto target = "observe0Greater1";
|
|
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, target);
|
|
|
|
storm::storage::BitVector accStates(model->getNumberOfStates(), false);
|
|
double accumProb = 0;
|
|
|
|
if (VERBOSE) std::cout << "Accumulating shortest paths ..." << std::endl;
|
|
for (int i = 1; accumProb < 0.15; i++) {
|
|
double pathProb = spg.getDistance(i);
|
|
accumProb += pathProb;
|
|
|
|
storm::storage::BitVector statesInPath = spg.getStates(i);
|
|
accStates |= statesInPath;
|
|
|
|
if (i % 50000 == 0) {
|
|
if (VERBOSE) std::cout << " --> It/States/AccProb/PathProb: " << i << " / " << accStates.getNumberOfSetBits() << " / " << accumProb << " / " << pathProb << std::endl;
|
|
}
|
|
}
|
|
|
|
std::chrono::duration<double> elapsedSeconds = std::chrono::system_clock::now() - startTime;
|
|
if (VERBOSE) std::cout << "Done. Num of states: " << accStates.getNumberOfSetBits() << ". Seconds: " << elapsedSeconds.count() << std::endl;
|
|
|
|
EXPECT_LE(elapsedSeconds.count(), 5); // should take less than 5 seconds on a modern PC
|
|
}
|