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

BeliefExplorationModelCheckerTest: added maze2 test case

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
5076ff00c6
commit
1313e3c096
2 changed files with 192 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 139
      resources/examples/testfiles/pomdp/maze2.prism
  2. 56
      src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp

139
resources/examples/testfiles/pomdp/maze2.prism
View File

@ -0,0 +1,139 @@
// maze example (POMDP)
// slightly extends that presented in
// Littman, Cassandra and Kaelbling
// Learning policies for partially observable environments: Scaling up
// Technical Report CS, Brown University
// gxn 29/01/16
// state space (value of variable "s")
// 0 1 2 3 4
// 5 6 7
// 8 9 10
// 11 13 12
// 13 is the target
pomdp
// can observe the walls and target
observables
o
endobservables
// o=0 - observation in initial state
// o=1 - west and north walls (s0)
// o=2 - north and south ways (s1 and s3)
// o=3 - north wall (s2)
// o=4 - east and north way (s4)
// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10)
// o=6 - east, west and south walls (s11 and s12)
// o=7 - the target (s13)
const double sl;
module maze
s : [-1..13];
o : [0..7];
// initialisation
[] s=-1 -> 1/13 : (s'=0) & (o'=1)
+ 1/13 : (s'=1) & (o'=2)
+ 1/13 : (s'=2) & (o'=3)
+ 1/13 : (s'=3) & (o'=2)
+ 1/13 : (s'=4) & (o'=4)
+ 1/13 : (s'=5) & (o'=5)
+ 1/13 : (s'=6) & (o'=5)
+ 1/13 : (s'=7) & (o'=5)
+ 1/13 : (s'=8) & (o'=5)
+ 1/13 : (s'=9) & (o'=5)
+ 1/13 : (s'=10) & (o'=5)
+ 1/13 : (s'=11) & (o'=6)
+ 1/13 : (s'=12) & (o'=6);
// moving around the maze
[east] s=0 -> (1-sl):(s'=1) & (o'=2) + sl:(s'=s) & (o'=o);
[west] s=0 -> (s'=0);
[north] s=0 -> (s'=0);
[south] s=0 -> (1-sl):(s'=5) & (o'=5) + sl:(s'=s) & (o'=o);
[east] s=1 -> (1-sl):(s'=2) & (o'=3) + sl:(s'=s) & (o'=o);
[west] s=1 -> (1-sl):(s'=0) & (o'=1) + sl:(s'=s) & (o'=o);
[north] s=1 -> (s'=1);
[south] s=1 -> (s'=1);
[east] s=2 -> (1-sl):(s'=3) & (o'=2) + sl:(s'=s) & (o'=o);
[west] s=2 -> (1-sl):(s'=1) & (o'=2) + sl:(s'=s) & (o'=o);
[north] s=2 -> (s'=2);
[south] s=2 -> (1-sl):(s'=6) & (o'=5) + sl:(s'=s) & (o'=o);
[east] s=3 -> (1-sl):(s'=4) & (o'=4) + sl:(s'=s) & (o'=o);
[west] s=3 -> (1-sl):(s'=2) & (o'=3) + sl:(s'=s) & (o'=o);
[north] s=3 -> (s'=3);
[south] s=3 -> (s'=3);
[east] s=4 -> (s'=4);
[west] s=4 -> (1-sl):(s'=3) & (o'=2) + sl:(s'=s) & (o'=o);
[north] s=4 -> (s'=4);
[south] s=4 -> (1-sl):(s'=7) & (o'=5) + sl:(s'=s) & (o'=o);
[east] s=5 -> (s'=5);
[west] s=5 -> (s'=5);
[north] s=5 -> (1-sl):(s'=0) & (o'=1) + sl:(s'=s) & (o'=o);
[south] s=5 -> (1-sl):(s'=8) + sl:(s'=s) & (o'=o);
[east] s=6 -> (s'=6);
[west] s=6 -> (s'=6);
[north] s=6 -> (1-sl):(s'=2) & (o'=3) + sl:(s'=s) & (o'=o);
[south] s=6 -> (1-sl):(s'=9) + sl:(s'=s) & (o'=o);
[east] s=7 -> (s'=7);
[west] s=7 -> (s'=7);
[north] s=7 -> (1-sl):(s'=4) & (o'=4) + sl:(s'=s) & (o'=o);
[south] s=7 -> (1-sl):(s'=10) + sl:(s'=s) & (o'=o);
[east] s=8 -> (s'=8);
[west] s=8 -> (s'=8);
[north] s=8 -> (1-sl):(s'=5) + sl:(s'=s) & (o'=o);
[south] s=8 -> (1-sl):(s'=11) & (o'=6) + sl:(s'=s) & (o'=o);
[east] s=9 -> (s'=9);
[west] s=9 -> (s'=9);
[north] s=9 -> (1-sl):(s'=6) + sl:(s'=s) & (o'=o);
[south] s=9 -> (1-sl):(s'=13) & (o'=7) + sl:(s'=s) & (o'=o);
[east] s=10 -> (s'=10);
[west] s=10 -> (s'=10);
[north] s=10 -> (1-sl):(s'=7) + sl:(s'=s) & (o'=o);
[south] s=10 -> (1-sl):(s'=12) & (o'=6) + sl:(s'=s) & (o'=o);
[east] s=11 -> (s'=11);
[west] s=11 -> (s'=11);
[north] s=11 -> (1-sl):(s'=8) & (o'=5) + sl:(s'=s) & (o'=o);
[south] s=11 -> (s'=11);
[east] s=12 -> (s'=12);
[west] s=12 -> (s'=12);
[north] s=12 -> (1-sl):(s'=10) & (o'=5) + sl:(s'=s) & (o'=o);
[south] s=12 -> (s'=12);
// loop when we reach the target
[done] s=13 -> true;
endmodule
// reward structure (number of steps to reach the target)/7
rewards
[east] true : 1/7;
[west] true : 1/7;
[north] true : 1/7;
[south] true : 1/7;
endrewards
// target observation
label "goal" = o=7;

56
src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp
View File

@ -85,7 +85,7 @@ namespace {
return env;
}
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.01); } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.02); } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {
options.resolutionInit = 24;
options.gapThresholdInit = storm::utility::convertNumber<ValueType>(0.001);
@ -103,7 +103,7 @@ namespace {
return env;
}
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.001); }
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.005); }
static PreprocessingType const preprocessingType = PreprocessingType::None;
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {options.refine = true; options.refinePrecision = precision();}
};
@ -118,7 +118,7 @@ namespace {
return env;
}
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.001); }
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.005); }
static PreprocessingType const preprocessingType = PreprocessingType::All;
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {options.refine = true; options.refinePrecision = precision();}
};
@ -352,5 +352,55 @@ namespace {
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, maze2_Rmin) {
typedef typename TestFixture::ValueType ValueType;
auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "R[exp]min=? [F \"goal\"]", "sl=0");
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
auto result = checker.check(*data.formula);
ValueType expected = this->parseNumber("74/91");
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, maze2_Rmax) {
typedef typename TestFixture::ValueType ValueType;
auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "R[exp]max=? [F \"goal\"]", "sl=0");
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
auto result = checker.check(*data.formula);
EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
}
TYPED_TEST(BeliefExplorationTest, maze2_slippery_Rmin) {
typedef typename TestFixture::ValueType ValueType;
auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "R[exp]min=? [F \"goal\"]", "sl=0.075");
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
auto result = checker.check(*data.formula);
ValueType expected = this->parseNumber("80/91");
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, maze2_slippery_Rmax) {
typedef typename TestFixture::ValueType ValueType;
auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "R[exp]max=? [F \"goal\"]", "sl=0.075");
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
auto result = checker.check(*data.formula);
EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
}
}
Write Preview
Loading…
Cancel
Save