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

Added some tests for BeliefExplorationPomdpModelChecker and made the testing more sensible towards very imprecise results

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
31c39d1dc7
commit
eeeb3df4f8
1 changed files with 79 additions and 17 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. 96
      src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp

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

@ -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<storm::RationalNumber>(1e-6));
return env;
}
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {} // TODO
static PreprocessingType const preprocessingType = PreprocessingType::None;
};
class DefaultDoubleVIEnvironment {
public:
@ -33,6 +21,8 @@ namespace {
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(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<ValueType>&) { /* intentionally left empty */ }
static PreprocessingType const preprocessingType = PreprocessingType::None;
};
@ -46,6 +36,8 @@ namespace {
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(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<ValueType>& options) { /* intentionally left empty */ }
static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO
};
@ -59,7 +51,12 @@ namespace {
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {} // TODO
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 void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {
options.resolutionInit = 24;
options.gapThresholdInit = storm::utility::convertNumber<ValueType>(0.001);
}
static PreprocessingType const preprocessingType = PreprocessingType::None;
};
@ -72,8 +69,25 @@ namespace {
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {} // TODO
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.001); }
static PreprocessingType const preprocessingType = PreprocessingType::None;
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& 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<storm::RationalNumber>(1e-6));
return env;
}
static bool const isExactModelChecking = false;
static ValueType precision() { return storm::utility::convertNumber<ValueType>(0.001); }
static PreprocessingType const preprocessingType = PreprocessingType::None; // TODO
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& 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<ValueType>(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<ValueType>& 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<ValueType>(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<ValueType>& 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<ValueType>(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<ValueType>& 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<ValueType>(); else return storm::utility::convertNumber<ValueType>(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<storm::models::sparse::Pomdp<ValueType>> 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<storm::models::sparse::Pomdp<ValueType>> 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<storm::models::sparse::Pomdp<ValueType>> 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<storm::models::sparse::Pomdp<ValueType>> 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;
}
}
Write Preview
Loading…
Cancel
Save