From eeeb3df4f8323ce6f4c6422189613ab241126d48 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 5 Jun 2020 16:52:28 +0200 Subject: [PATCH] Added some tests for BeliefExplorationPomdpModelChecker and made the testing more sensible towards very imprecise results --- ...BeliefExplorationPomdpModelCheckerTest.cpp | 96 +++++++++++++++---- 1 file changed, 79 insertions(+), 17 deletions(-) diff --git a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp index c08e78513..79fcdcf2b 100644 --- a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp +++ b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp @@ -11,18 +11,6 @@ namespace { enum class PreprocessingType { None }; - class CoarseDoubleVIEnvironment { - public: - typedef double ValueType; - static storm::Environment createEnvironment() { - storm::Environment env; - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); - return env; - } - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) {} // TODO - static PreprocessingType const preprocessingType = PreprocessingType::None; - }; class DefaultDoubleVIEnvironment { public: @@ -33,6 +21,8 @@ namespace { env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); return env; } + static bool const isExactModelChecking = false; + static ValueType precision() { return storm::utility::convertNumber(0.1); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -46,6 +36,8 @@ namespace { env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); return env; } + static bool const isExactModelChecking = false; + static ValueType precision() { return storm::utility::convertNumber(0.1); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO }; @@ -59,7 +51,12 @@ namespace { env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); return env; } - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) {} // TODO + static bool const isExactModelChecking = false; + static ValueType precision() { return storm::utility::convertNumber(0.01); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) { + options.resolutionInit = 24; + options.gapThresholdInit = storm::utility::convertNumber(0.001); + } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -72,8 +69,25 @@ namespace { env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); return env; } - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) {} // TODO + static bool const isExactModelChecking = false; + static ValueType precision() { return storm::utility::convertNumber(0.001); } static PreprocessingType const preprocessingType = PreprocessingType::None; + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) {options.refine = true; options.refinePrecision = precision();} + }; + + class PreprocessedRefineDoubleVIEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + return env; + } + static bool const isExactModelChecking = false; + static ValueType precision() { return storm::utility::convertNumber(0.001); } + static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) {options.refine = true; options.refinePrecision = precision();} }; class DefaultDoubleOVIEnvironment { @@ -86,6 +100,8 @@ namespace { env.solver().setForceSoundness(true); return env; } + static bool const isExactModelChecking = false; + static ValueType precision() { return storm::utility::convertNumber(0.1); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -99,6 +115,8 @@ namespace { env.solver().setForceExact(true); return env; } + static bool const isExactModelChecking = true; + static ValueType precision() { return storm::utility::convertNumber(0.1); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -112,6 +130,8 @@ namespace { env.solver().setForceExact(true); return env; } + static bool const isExactModelChecking = true; + static ValueType precision() { return storm::utility::convertNumber(0.1); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions& options) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO }; @@ -155,17 +175,19 @@ namespace { EXPECT_TRUE(input.model->isCanonic()); return input; } + ValueType precision() const { return TestType::precision(); } + ValueType modelcheckingPrecision() const { if (TestType::isExactModelChecking) return storm::utility::zero(); else return storm::utility::convertNumber(1e-6); } private: storm::Environment _environment; }; typedef ::testing::Types< - CoarseDoubleVIEnvironment, DefaultDoubleVIEnvironment, PreprocessedDefaultDoubleVIEnvironment, FineDoubleVIEnvironment, RefineDoubleVIEnvironment, + PreprocessedRefineDoubleVIEnvironment, DefaultDoubleOVIEnvironment, DefaultRationalPIEnvironment, PreprocessedDefaultRationalPIEnvironment @@ -180,8 +202,48 @@ namespace { storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker> checker(data.model, this->options()); auto result = checker.check(*data.formula); - EXPECT_LE(result.lowerBound, this->parseNumber("7/10")); - EXPECT_GE(result.upperBound, this->parseNumber("7/10")); + ValueType expected = this->parseNumber("7/10"); + EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision()); + EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision()); + EXPECT_LE(result.diff(), this->precision()) << "Result [" << result.lowerBound << ", " << result.upperBound << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise." << std::endl; + } + + TYPED_TEST(BeliefExplorationTest, simple_min) { + typedef typename TestFixture::ValueType ValueType; + + auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0"); + storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker> checker(data.model, this->options()); + auto result = checker.check(*data.formula); + + ValueType expected = this->parseNumber("3/10"); + EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision()); + EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision()); + EXPECT_LE(result.diff(), this->precision()) << "Result [" << result.lowerBound << ", " << result.upperBound << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise." << std::endl; + } + + TYPED_TEST(BeliefExplorationTest, simple_slippery_max) { + typedef typename TestFixture::ValueType ValueType; + + auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4"); + storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker> checker(data.model, this->options()); + auto result = checker.check(*data.formula); + + ValueType expected = this->parseNumber("7/10"); + EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision()); + EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision()); + EXPECT_LE(result.diff(), this->precision()) << "Result [" << result.lowerBound << ", " << result.upperBound << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise." << std::endl; + } + + TYPED_TEST(BeliefExplorationTest, simple_slippery_min) { + typedef typename TestFixture::ValueType ValueType; + + auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4"); + storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker> checker(data.model, this->options()); + auto result = checker.check(*data.formula); + ValueType expected = this->parseNumber("3/10"); + EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision()); + EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision()); + EXPECT_LE(result.diff(), this->precision()) << "Result [" << result.lowerBound << ", " << result.upperBound << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise." << std::endl; } }