From 5536cda9027a070932f765436a9c701a6dcbdd27 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 8 Jun 2020 15:53:38 +0200 Subject: [PATCH] BeliefExplorationModelCheckerTest: added refuel test case --- .../examples/testfiles/pomdp/refuel.prism | 98 +++++++++++++++++++ ...BeliefExplorationPomdpModelCheckerTest.cpp | 43 ++++++-- 2 files changed, 134 insertions(+), 7 deletions(-) create mode 100644 resources/examples/testfiles/pomdp/refuel.prism diff --git a/resources/examples/testfiles/pomdp/refuel.prism b/resources/examples/testfiles/pomdp/refuel.prism new file mode 100644 index 000000000..34298b388 --- /dev/null +++ b/resources/examples/testfiles/pomdp/refuel.prism @@ -0,0 +1,98 @@ +pomdp + +observables +start, fuel +endobservables + +const int N; +const int fuelCAP = N-1; +const int axMAX = N; +const int ayMAX = N; +const int axMIN = 0; +const int ayMIN = 0; +const double slippery = 0.4; +const int ob1x = axMAX-1; +const int ob1y = ayMAX-1; +const int rf1x = axMIN; +const int rf1y = ayMIN; +const int rf2x = axMIN + ceil((axMAX - axMIN) / 3); +const int rf2y = ayMIN + ceil((ayMAX - ayMIN) / 3); +const int rf3x = axMIN + floor(2 * (axMAX - axMIN) / 3); +const int rf3y = ayMIN + floor(2 * (ayMAX - ayMIN) / 3); + +formula northenabled = ax != axMIN; +formula southenabled = ax != axMAX; +formula westenabled = ay != ayMIN; +formula eastenabled = ay != ayMAX; +observable "cangonorth" = northenabled; +observable "cangosouth" = southenabled; +observable "cangowest" = westenabled; +observable "cangoeast" = eastenabled; +formula done = start & ax = axMAX & ay = ayMAX; +observable "amdone" = done; +formula crash = (ax = ob1x & ay = ob1y); +observable "hascrash" = crash; +formula atStation = (ax = rf1x & ay = rf1y) | (ax = rf2x & ay = rf2y) | (ax = rf3x & ay = rf3y); +formula canRefuel = atStation & fuel < fuelCAP; +observable "refuelAllowed" = canRefuel; + +module master + start : bool init false; + + [placement] !start -> (start'=true); + [north] start & !done -> true; + [south] start & !done -> true; + [east] start & !done-> true; + [west] start & !done -> true; + + +endmodule + + +module tank + fuel : [0..fuelCAP] init fuelCAP; + + [refuel] canRefuel -> 1:(fuel'=fuelCAP); + [north] fuel > 0 & !canRefuel -> 1:(fuel'=fuel-1); + [south] fuel > 0 & !canRefuel -> 1:(fuel'=fuel-1); + [east] fuel > 0 & !canRefuel -> 1:(fuel'=fuel-1); + [west] fuel > 0 & !canRefuel -> 1:(fuel'=fuel-1); + [empty] fuel = 0 & !canRefuel -> 1:(fuel'=0); +endmodule + +module alice + ax : [axMIN..axMAX] init 0; + ay : [ayMIN..ayMAX] init 0; + + [placement] true -> 1: (ax'=0) & (ay'=0); //+ 1/4: (ax'=1) & (ay'=1) + 1/4: (ax'=2) & (ay'=1) + 1/4: (ax'=1) & (ay'=3); + + [west] northenabled -> (1-slippery): (ax'=max(ax-1,axMIN)) + slippery: (ax'=max(ax-2,axMIN)); + [east] southenabled -> (1-slippery): (ax'=min(ax+1,axMAX)) + slippery: (ax'=min(ax+2,axMAX)); + [south] eastenabled -> (1-slippery): (ay'=min(ay+1,ayMAX)) + slippery: (ay'=min(ay+2,ayMAX)); + [north] westenabled -> (1-slippery): (ay'=max(ay-1,ayMIN)) + slippery: (ay'=max(ay-2,ayMIN)); +endmodule + +rewards "steps" + [north] true : 1; + [south] true : 1; + [west] true : 1; + [east] true : 1; +endrewards + +rewards "refuels" + [refuel] true : 1; +endrewards + +rewards "costs" + [north] true : 1; + [south] true : 1; + [west] true : 1; + [east] true : 1; + [refuel] true : 3; +endrewards + + +label "goal" = done; +label "traps" = crash; +label "stationvisit" = atStation; +label "notbad" = !crash & (fuel > 0 | canRefuel); diff --git a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp index 0cbe5c7c7..afb617692 100644 --- a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp +++ b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp @@ -25,7 +25,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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; }; @@ -40,7 +40,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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::SelfloopReduction; }; @@ -55,7 +55,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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::QualitativeReduction; }; @@ -70,7 +70,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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::All; }; @@ -134,7 +134,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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; }; @@ -149,7 +149,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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; }; @@ -164,7 +164,7 @@ namespace { 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 ValueType precision() { return storm::utility::convertNumber(0.12); } // 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::All; }; @@ -402,5 +402,34 @@ namespace { EXPECT_TRUE(storm::utility::isInfinity(result.upperBound)); } + TYPED_TEST(BeliefExplorationTest, refuel_Pmax) { + typedef typename TestFixture::ValueType ValueType; + + auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4"); + storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker> checker(data.model, this->options()); + auto result = checker.check(*data.formula); + + ValueType expected = this->parseNumber("38/155"); + EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision()); + EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision()); + // Use relative difference of bounds for this one + 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, refuel_Pmin) { + typedef typename TestFixture::ValueType ValueType; + + auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4"); + storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker> checker(data.model, this->options()); + auto result = checker.check(*data.formula); + + ValueType expected = this->parseNumber("0"); + EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision()); + EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision()); + // Use relative difference of bounds for this one + 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; + } + + }