From 4dc69dd6f5835af0e65179be855635e4f06f34bf Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Fri, 20 Feb 2015 17:36:24 +0100 Subject: [PATCH] Fixed performance tests, and again things concerning templates I never heard of before. Former-commit-id: 1d110c6aad536b9c6c7635b3969f20ba4e0db640 --- ...onNondeterministicLinearEquationSolver.cpp | 4 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 221 ++++++++++-------- 2 files changed, 120 insertions(+), 105 deletions(-) diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index 30331d1ae..8d62cc9ac 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -63,7 +63,7 @@ namespace storm { #define __FORCE_FLOAT_CALCULATION false #endif if (__FORCE_FLOAT_CALCULATION && (sizeof(ValueType) == sizeof(double))) { - TopologicalValueIterationNondeterministicLinearEquationSolver tvindles{ precision, maximalNumberOfIterations, relative }; + TopologicalValueIterationNondeterministicLinearEquationSolver tvindles{ this->precision, this->maximalNumberOfIterations, this->relative }; storm::storage::SparseMatrix new_A = A.template toValueType(); std::vector new_x = storm::utility::vector::toValueType(x); @@ -298,7 +298,7 @@ namespace storm { ++localIterations; ++globalIterations; } - LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations."); + LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << this->maximalNumberOfIterations << " Iterations."); } diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 441c4a3bb..a66b47028 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -1,77 +1,83 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/settings/Settings.h" #include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.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" TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); std::shared_ptr> 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>(); ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); - storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + auto apFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(apFormula); + auto probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - std::vector result = mc.checkNoBoundOperator(*probFormula); + std::unique_ptr 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()[0] - 1.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - apFormula = new storm::property::prctl::Ap("elected"); - eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + apFormula = std::make_shared("elected"); + eventuallyFormula = std::make_shared(apFormula); + probFormula = std::make_shared(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()[0] - 1.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - apFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + apFormula = std::make_shared("elected"); + auto boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); + probFormula = std::make_shared(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()[0] - 0.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - apFormula = new storm::property::prctl::Ap("elected"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + apFormula = std::make_shared("elected"); + boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 25); + probFormula = std::make_shared(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()[0] - 0.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - apFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + apFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(apFormula); + auto rewardFormula = std::make_shared(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()[0] - 6.172433512), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + rewardFormula.reset(); - apFormula = new storm::property::prctl::Ap("elected"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + apFormula = std::make_shared("elected"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(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()[0] - 6.1724344), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + rewardFormula.reset(); } TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); // Increase the maximal number of iterations, because the solver does not converge otherwise. // This is done in the main cpp unit @@ -80,84 +86,93 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); - - storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); + + auto apFormula = std::make_shared("finished"); + auto eventuallyFormula = std::make_shared(apFormula); + auto probFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); - std::vector 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()[31168] - 1.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - apFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::Ap* apFormula2 = new storm::property::prctl::Ap("all_coins_equal_0"); - storm::property::prctl::And* andFormula = new storm::property::prctl::And(apFormula, apFormula2); - eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + apFormula = std::make_shared("finished"); + auto apFormula2 = std::make_shared("all_coins_equal_0"); + auto andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2); + eventuallyFormula = std::make_shared(andFormula); + probFormula = std::make_shared(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; - - apFormula = new storm::property::prctl::Ap("finished"); - apFormula2 = new storm::property::prctl::Ap("all_coins_equal_1"); - andFormula = new storm::property::prctl::And(apFormula, apFormula2); - eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.4374282832), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - - apFormula = new storm::property::prctl::Ap("finished"); - apFormula2 = new storm::property::prctl::Ap("agree"); - storm::property::prctl::Not* notFormula = new storm::property::prctl::Not(apFormula2); - andFormula = new storm::property::prctl::And(apFormula, notFormula); - eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + apFormula = std::make_shared("finished"); + apFormula2 = std::make_shared("all_coins_equal_1"); + andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, apFormula2); + eventuallyFormula = std::make_shared(andFormula); + probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.check(*probFormula); - ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.5293286369), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - apFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + apFormula = std::make_shared("finished"); + apFormula2 = std::make_shared("agree"); + auto notFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, apFormula2); + andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, apFormula, notFormula); + eventuallyFormula = std::make_shared(andFormula); + probFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = mc.check(*probFormula); - result = mc.checkNoBoundOperator(*probFormula); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.10414097), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); + + apFormula = std::make_shared("finished"); + auto boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 50ull); + probFormula = std::make_shared(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("finished"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - result = mc.checkNoBoundOperator(*probFormula); + apFormula = std::make_shared("finished"); + boundedEventuallyFormula = std::make_shared(std::make_shared(true), apFormula, 50ull); + probFormula = std::make_shared(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("finished"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - - result = mc.checkNoBoundOperator(*rewardFormula); - - ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - - apFormula = new storm::property::prctl::Ap("finished"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 0.0), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); + + apFormula = std::make_shared("finished"); + auto reachabilityRewardFormula = std::make_shared(apFormula); + auto rewardFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = mc.check(*rewardFormula); - result = mc.checkNoBoundOperator(*rewardFormula); + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 1725.593313), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); - ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + apFormula = std::make_shared("finished"); + reachabilityRewardFormula = std::make_shared(apFormula); + rewardFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = mc.check(*rewardFormula); + + ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[31168] - 2183.142422), + storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); + probFormula.reset(); } \ No newline at end of file