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

More tests adapted, decreased verbosity of TopologicalValueIterationNondeterministicLinearEquationSolver 

Former-commit-id: 6e0b492533
tempestpy_adaptions
David_Korzeniewski 10 years ago
parent
90958bb018
commit
84f8a41302
2 changed files with 62 additions and 52 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. 19
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  2. 95
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

19
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
View File

@ -73,10 +73,10 @@ namespace storm {
// For testing only
if (sizeof(ValueType) == sizeof(double)) {
std::cout << "<<< Using CUDA-DOUBLE Kernels >>>" << std::endl;
//std::cout << "<<< Using CUDA-DOUBLE Kernels >>>" << std::endl;
LOG4CPLUS_INFO(logger, "<<< Using CUDA-DOUBLE Kernels >>>");
} else {
std::cout << "<<< Using CUDA-FLOAT Kernels >>>" << std::endl;
//std::cout << "<<< Using CUDA-FLOAT Kernels >>>" << std::endl;
LOG4CPLUS_INFO(logger, "<<< Using CUDA-FLOAT Kernels >>>");
}
@ -96,7 +96,7 @@ namespace storm {
std::vector<std::pair<bool, storm::storage::StateBlock>> sccDecomposition;
if (__USE_CUDAFORSTORM_OPT && (gpuSizeOfCompleteSystem < cudaFreeMemory)) {
// Dummy output for SCC Times
std::cout << "Computing the SCC Decomposition took 0ms" << std::endl;
//std::cout << "Computing the SCC Decomposition took 0ms" << std::endl;
#ifdef STORM_HAVE_CUDAFORSTORM
if (!resetCudaDevice()) {
@ -124,9 +124,9 @@ namespace storm {
}
std::chrono::high_resolution_clock::time_point calcEndTime = std::chrono::high_resolution_clock::now();
std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast<std::chrono::milliseconds>(calcEndTime - calcStartTime).count() << "ms." << std::endl;
//std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast<std::chrono::milliseconds>(calcEndTime - calcStartTime).count() << "ms." << std::endl;
std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << globalIterations << " iterations in a single block." << std::endl;
//std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << globalIterations << " iterations in a single block." << std::endl;
// Check if the solver converged and issue a warning otherwise.
if (converged) {
@ -157,7 +157,7 @@ namespace storm {
LOG4CPLUS_INFO(logger, "Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs.");
std::chrono::high_resolution_clock::time_point sccEndTime = std::chrono::high_resolution_clock::now();
std::cout << "Computing the SCC Decomposition took " << std::chrono::duration_cast<std::chrono::milliseconds>(sccEndTime - sccStartTime).count() << "ms." << std::endl;
//std::cout << "Computing the SCC Decomposition took " << std::chrono::duration_cast<std::chrono::milliseconds>(sccEndTime - sccStartTime).count() << "ms." << std::endl;
std::chrono::high_resolution_clock::time_point calcStartTime = std::chrono::high_resolution_clock::now();
@ -255,7 +255,8 @@ namespace storm {
throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
#endif
} else {
std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
//std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
LOG4CPLUS_INFO(logger, "Performance Warning: Using CPU based TopoSolver! (double)");
localIterations = 0;
converged = false;
while (!converged && localIterations < this->maximalNumberOfIterations) {
@ -313,7 +314,7 @@ namespace storm {
}
}
std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << localIterations << " iterations in a single block." << std::endl;
//std::cout << "Used a total of " << globalIterations << " iterations with a maximum of " << localIterations << " iterations in a single block." << std::endl;
// Check if the solver converged and issue a warning otherwise.
if (converged) {
@ -323,7 +324,7 @@ namespace storm {
}
std::chrono::high_resolution_clock::time_point calcEndTime = std::chrono::high_resolution_clock::now();
std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast<std::chrono::milliseconds>(calcEndTime - calcStartTime).count() << "ms." << std::endl;
//std::cout << "Obtaining the fixpoint solution took " << std::chrono::duration_cast<std::chrono::milliseconds>(calcEndTime - calcStartTime).count() << "ms." << std::endl;
}
}

95
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -209,77 +209,86 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
}
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
//storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as<storm::models::Mdp<double>>();
//ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
//ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
//storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
//storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
//storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
//std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
auto probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*probabilityOperatorFormula);
//ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//delete probFormula;
probabilityOperatorFormula.reset();
//apFormula = new storm::property::prctl::Ap<double>("elected");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
//result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probabilityOperatorFormula);
//ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//delete probFormula;
probabilityOperatorFormula.reset();
//apFormula = new storm::property::prctl::Ap<double>("elected");
//storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula);
//result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probabilityOperatorFormula);
//ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0625),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//delete probFormula;
probabilityOperatorFormula.reset();
//apFormula = new storm::property::prctl::Ap<double>("elected");
//boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula);
//result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probabilityOperatorFormula);
//ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0625),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//delete probFormula;
probabilityOperatorFormula.reset();
//apFormula = new storm::property::prctl::Ap<double>("elected");
//storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
auto rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
//result = mc.checkNoBoundOperator(*rewardFormula);
result = mc.check(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
//ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 4.285689611),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
//ASSERT_LT(std::abs(result[0] - 4.285701547), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 4.285701547),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
//delete rewardFormula;
//apFormula = new storm::property::prctl::Ap<double>("elected");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
probabilityOperatorFormula.reset();
//result = mc.checkNoBoundOperator(*rewardFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = mc.check(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM
//ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 4.285689611),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#else
//ASSERT_LT(std::abs(result[0] - 4.285703591), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 4.285703591),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
//delete rewardFormula;
probabilityOperatorFormula.reset();
}
Write Preview
Loading…
Cancel
Save