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

Fixed performance tests, and again things concerning templates I never heard of before. 

Former-commit-id: 1d110c6aad
main
David_Korzeniewski 11 years ago
parent
7515ca5293
commit
4dc69dd6f5
2 changed files with 120 additions and 105 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  2. 207
      test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

4
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
View File

@ -63,7 +63,7 @@ namespace storm {
#define __FORCE_FLOAT_CALCULATION false #define __FORCE_FLOAT_CALCULATION false
#endif #endif
if (__FORCE_FLOAT_CALCULATION && (sizeof(ValueType) == sizeof(double))) { if (__FORCE_FLOAT_CALCULATION && (sizeof(ValueType) == sizeof(double))) {
TopologicalValueIterationNondeterministicLinearEquationSolver<float> tvindles{ precision, maximalNumberOfIterations, relative };
TopologicalValueIterationNondeterministicLinearEquationSolver<float> tvindles{ this->precision, this->maximalNumberOfIterations, this->relative };
storm::storage::SparseMatrix<float> new_A = A.template toValueType<float>(); storm::storage::SparseMatrix<float> new_A = A.template toValueType<float>();
std::vector<float> new_x = storm::utility::vector::toValueType<float>(x); std::vector<float> new_x = storm::utility::vector::toValueType<float>(x);
@ -298,7 +298,7 @@ namespace storm {
++localIterations; ++localIterations;
++globalIterations; ++globalIterations;
} }
LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations.");
LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << this->maximalNumberOfIterations << " Iterations.");
} }

207
test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -1,77 +1,83 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "src/settings/Settings.h"
#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h"
#include "src/solver/NativeNondeterministicLinearEquationSolver.h" #include "src/solver/NativeNondeterministicLinearEquationSolver.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { 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/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::modelchecker::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);
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
auto probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*probFormula);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.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);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.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, true);
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);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedEventuallyFormula);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.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, false);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 25);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedEventuallyFormula);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.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);
ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 6.172433512),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
rewardFormula.reset();
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);
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.checkNoBoundOperator(*rewardFormula);
result = mc.check(*rewardFormula);
ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 6.1724344),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
rewardFormula.reset();
} }
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
// Increase the maximal number of iterations, because the solver does not converge otherwise. // Increase the maximal number of iterations, because the solver does not converge otherwise.
// This is done in the main cpp unit // This is done in the main cpp unit
@ -80,84 +86,93 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
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);
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
auto probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
auto result = mc.check(*probFormula);
ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 1.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Ap<double>* apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_0");
storm::property::prctl::And<double>* andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto apFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_0");
auto andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.check(*probFormula);
ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.4374282832),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_1");
andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
apFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("all_coins_equal_1");
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
result = mc.check(*probFormula);
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("agree");
storm::property::prctl::Not<double>* notFormula = new storm::property::prctl::Not<double>(apFormula2);
andFormula = new storm::property::prctl::And<double>(apFormula, notFormula);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.5293286369),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = mc.checkNoBoundOperator(*probFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
apFormula2 = std::make_shared<storm::logic::AtomicLabelFormula>("agree");
auto notFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, apFormula2);
andFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, notFormula);
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(andFormula);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
result = mc.check(*probFormula);
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.10414097),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = mc.checkNoBoundOperator(*probFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 50ull);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
result = mc.check(*probFormula);
apFormula = new storm::property::prctl::Ap<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = mc.checkNoBoundOperator(*probFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
boundedEventuallyFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), apFormula, 50ull);
probFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
result = mc.check(*probFormula);
apFormula = new storm::property::prctl::Ap<double>("finished");
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);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 0.0),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = mc.checkNoBoundOperator(*rewardFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
auto rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
result = mc.check(*rewardFormula);
apFormula = new storm::property::prctl::Ap<double>("finished");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 1725.593313),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
result = mc.checkNoBoundOperator(*rewardFormula);
apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("finished");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(apFormula);
rewardFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
result = mc.check(*rewardFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[31168] - 2183.142422),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
probFormula.reset();
} }
Write Preview
Loading…
Cancel
Save