From 6911d50985f3770654f955340416d03b2f8555e0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 Nov 2017 15:19:06 +0100 Subject: [PATCH] extended MDP model checker test --- .../modelchecker/MdpPrctlModelCheckerTest.cpp | 210 +++++++++++++++--- 1 file changed, 184 insertions(+), 26 deletions(-) diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index dcdb3c70e..758c9bd74 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -3,8 +3,10 @@ #include "test/storm_gtest.h" -#include "storm/parser/FormulaParser.h" -#include "storm/logic/Formulas.h" +#include "storm/api/builder.h" +#include "storm/api/model_descriptions.h" +#include "storm/api/properties.h" + #include "storm/models/sparse/Mdp.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -15,35 +17,31 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm/settings/SettingsManager.h" -#include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" -#include "storm/api/properties.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" - -#include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/parser/AutoParser.h" +#include "storm/logic/Formulas.h" +#include "storm/storage/jani/Property.h" +#include "storm/exceptions/UncheckedRequirementException.h" namespace { class SparseDoubleValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); return env; } - // TODO: this should be part of the environment - static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } }; class SparseDoubleSoundValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; static const bool isExact = false; typedef double ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -54,12 +52,11 @@ namespace { env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); return env; } - // TODO: this should be part of the environment - static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } }; class SparseRationalPolicyIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -68,12 +65,11 @@ namespace { env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); return env; } - // TODO: this should be part of the environment - static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } }; class SparseRationalRationalSearchEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; static const bool isExact = true; typedef storm::RationalNumber ValueType; typedef storm::models::sparse::Mdp ModelType; @@ -82,10 +78,119 @@ namespace { env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); return env; } - // TODO: this should be part of the environment - static storm::settings::modules::CoreSettings::Engine engine() { return storm::settings::modules::CoreSettings::Engine::Sparse; } }; - + class HybridCuddDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class HybridSylvanDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class HybridCuddDoubleSoundValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + }; + class HybridSylvanRationalPolicyIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + }; + class DdCuddDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class DdSylvanDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class DdCuddDoublePolicyIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class DdSylvanRationalRationalSearchEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Dd; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::symbolic::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); + return env; + } + }; + template class MdpPrctlModelCheckerTest : public ::testing::Test { public: @@ -133,15 +238,17 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - return std::make_shared>(*model); + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + return std::make_shared>(*model); + } } template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { return std::make_shared>(*model); - } else if (TestType::engine() == storm::settings::modules::CoreSettings::Engine::Dd) { + } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { return std::make_shared>(*model); } } @@ -174,8 +281,16 @@ namespace { SparseDoubleValueIterationEnvironment, SparseDoubleSoundValueIterationEnvironment, SparseRationalPolicyIterationEnvironment, - SparseRationalRationalSearchEnvironment - > TestingTypes; + SparseRationalRationalSearchEnvironment, + HybridCuddDoubleValueIterationEnvironment, + HybridSylvanDoubleValueIterationEnvironment, + HybridCuddDoubleSoundValueIterationEnvironment, + HybridSylvanRationalPolicyIterationEnvironment, + DdCuddDoubleValueIterationEnvironment, + DdSylvanDoubleValueIterationEnvironment, + DdCuddDoublePolicyIterationEnvironment, + DdSylvanRationalRationalSearchEnvironment + > TestingTypes; TYPED_TEST_CASE(MdpPrctlModelCheckerTest, TestingTypes); @@ -261,6 +376,42 @@ namespace { EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(MdpPrctlModelCheckerTest, consensus) { + std::string formulasString = "Pmax=? [F \"finished\"]"; + formulasString += "; Pmax=? [F \"all_coins_equal_1\"]"; + formulasString += "; Rmax=? [F \"all_coins_equal_1\"]"; + formulasString += "; Rmin=? [F \"all_coins_equal_1\"]"; + formulasString += "; Rmax=? [F \"finished\"]"; + formulasString += "; Rmin=? [F \"finished\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(272ul, model->getNumberOfStates()); + EXPECT_EQ(492ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("57/64"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + result = checker->check(this->env(), tasks[3]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("75"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("48"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) { std::string formulasString = "Rmin=? [F \"target\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString); @@ -271,8 +422,15 @@ namespace { ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); auto checker = this->createModelChecker(model); std::unique_ptr result; + + // This example considers a zero-reward end component that does not reach the target + // For some methods this requires end-component elimination which is (currently) not supported in the Dd engine - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + if (TypeParam::engine == storm::settings::modules::CoreSettings::Engine::Dd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) { + EXPECT_THROW(checker->check(this->env(), tasks[0]), storm::exceptions::UncheckedRequirementException); + } else { + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } } } \ No newline at end of file