Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BeliefExplorationPomdpModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/api/storm-parsers.h"
5#include "storm-pomdp/analysis/QualitativeAnalysisOnGraphs.h"
6#include "storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.h"
7#include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h"
8#include "storm-pomdp/transformer/KnownProbabilityTransformer.h"
9#include "storm/api/storm.h"
10#include "storm/environment/solver/MinMaxSolverEnvironment.h"
11#include "storm/transformer/MakePOMDPCanonic.h"
12
13namespace {
14enum class PreprocessingType { None, SelfloopReduction, QualitativeReduction, All };
15
16class DefaultDoubleVIEnvironment {
17 public:
18 typedef double ValueType;
19 static storm::Environment createEnvironment() {
20 storm::Environment env;
21 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
22 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
23 return env;
24 }
25 static bool const isExactModelChecking = false;
26 static ValueType precision() {
27 return storm::utility::convertNumber<ValueType>(0.12);
28 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
29 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
30 static PreprocessingType const preprocessingType = PreprocessingType::None;
31};
32
33class SelfloopReductionDefaultDoubleVIEnvironment {
34 public:
35 typedef double ValueType;
36 static storm::Environment createEnvironment() {
37 storm::Environment env;
38 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
39 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
40 return env;
41 }
42 static bool const isExactModelChecking = false;
43 static ValueType precision() {
44 return storm::utility::convertNumber<ValueType>(0.12);
45 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
46 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
47 static PreprocessingType const preprocessingType = PreprocessingType::SelfloopReduction;
48};
49
50class QualitativeReductionDefaultDoubleVIEnvironment {
51 public:
52 typedef double ValueType;
53 static storm::Environment createEnvironment() {
54 storm::Environment env;
55 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
56 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
57 return env;
58 }
59 static bool const isExactModelChecking = false;
60 static ValueType precision() {
61 return storm::utility::convertNumber<ValueType>(0.12);
62 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
63 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
64 static PreprocessingType const preprocessingType = PreprocessingType::QualitativeReduction;
65};
66
67class PreprocessedDefaultDoubleVIEnvironment {
68 public:
69 typedef double ValueType;
70 static storm::Environment createEnvironment() {
71 storm::Environment env;
72 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
73 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
74 return env;
75 }
76 static bool const isExactModelChecking = false;
77 static ValueType precision() {
78 return storm::utility::convertNumber<ValueType>(0.12);
79 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
80 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
81 static PreprocessingType const preprocessingType = PreprocessingType::All;
82};
83
84class FineDoubleVIEnvironment {
85 public:
86 typedef double ValueType;
87 static storm::Environment createEnvironment() {
88 storm::Environment env;
89 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
90 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
91 return env;
92 }
93 static bool const isExactModelChecking = false;
94 static ValueType precision() {
95 return storm::utility::convertNumber<ValueType>(0.02);
96 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
97 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {
98 options.resolutionInit = 24;
99 }
100 static PreprocessingType const preprocessingType = PreprocessingType::None;
101};
102
103class RefineDoubleVIEnvironment {
104 public:
105 typedef double ValueType;
106 static storm::Environment createEnvironment() {
107 storm::Environment env;
108 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
109 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
110 return env;
111 }
112 static bool const isExactModelChecking = false;
113 static ValueType precision() {
114 return storm::utility::convertNumber<ValueType>(0.005);
115 }
116 static PreprocessingType const preprocessingType = PreprocessingType::None;
117 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {
118 options.refine = true;
119 options.refinePrecision = precision();
120 }
121};
122
123class PreprocessedRefineDoubleVIEnvironment {
124 public:
125 typedef double ValueType;
126 static storm::Environment createEnvironment() {
127 storm::Environment env;
128 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
129 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
130 return env;
131 }
132 static bool const isExactModelChecking = false;
133 static ValueType precision() {
134 return storm::utility::convertNumber<ValueType>(0.005);
135 }
136 static PreprocessingType const preprocessingType = PreprocessingType::All;
137 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>& options) {
138 options.refine = true;
139 options.refinePrecision = precision();
140 }
141};
142
143class DefaultDoubleOVIEnvironment {
144 public:
145 typedef double ValueType;
146 static storm::Environment createEnvironment() {
147 storm::Environment env;
148 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
149 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
150 env.solver().setForceSoundness(true);
151 return env;
152 }
153 static bool const isExactModelChecking = false;
154 static ValueType precision() {
155 return storm::utility::convertNumber<ValueType>(0.12);
156 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
157 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
158 static PreprocessingType const preprocessingType = PreprocessingType::None;
159};
160
161class DefaultRationalPIEnvironment {
162 public:
163 typedef storm::RationalNumber ValueType;
164 static storm::Environment createEnvironment() {
165 storm::Environment env;
166 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
167 env.solver().setForceExact(true);
168 return env;
169 }
170 static bool const isExactModelChecking = true;
171 static ValueType precision() {
172 return storm::utility::convertNumber<ValueType>(0.12);
173 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
174 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
175 static PreprocessingType const preprocessingType = PreprocessingType::None;
176};
177
178class PreprocessedDefaultRationalPIEnvironment {
179 public:
180 typedef storm::RationalNumber ValueType;
181 static storm::Environment createEnvironment() {
182 storm::Environment env;
183 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
184 env.solver().setForceExact(true);
185 return env;
186 }
187 static bool const isExactModelChecking = true;
188 static ValueType precision() {
189 return storm::utility::convertNumber<ValueType>(0.12);
190 } // there actually aren't any precision guarantees, but we still want to detect if results are weird.
191 static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>&) { /* intentionally left empty */ }
192 static PreprocessingType const preprocessingType = PreprocessingType::All;
193};
194
195template<typename TestType>
196class BeliefExplorationPomdpModelCheckerTest : public ::testing::Test {
197 public:
198 typedef typename TestType::ValueType ValueType;
199 BeliefExplorationPomdpModelCheckerTest() : _environment(TestType::createEnvironment()) {}
200
201 void SetUp() override {
202#ifndef STORM_HAVE_Z3
203 GTEST_SKIP() << "Z3 not available.";
204#endif
205 }
206
207 storm::Environment const& env() const {
208 return _environment;
209 }
210 storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> options() const {
211 storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> opt(true, true); // Always compute both bounds (lower and upper)
212 opt.gapThresholdInit = 0;
213 TestType::adaptOptions(opt);
214 return opt;
215 }
216 storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> optionsWithStateElimination() const {
217 storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> opt(true, true); // Always compute both bounds (lower and upper)
218 opt.gapThresholdInit = 0;
219 TestType::adaptOptions(opt);
220 opt.useStateEliminationCutoff = true;
221 return opt;
222 }
223 storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> optionsWithClipping() const {
224 storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType> opt(true, true); // Always compute both bounds (lower and upper)
225 opt.gapThresholdInit = 0;
226 TestType::adaptOptions(opt);
227 opt.useClipping = true;
228 return opt;
229 }
230 ValueType parseNumber(std::string const& str) {
231 return storm::utility::convertNumber<ValueType>(str);
232 }
233 struct Input {
234 std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> model;
235 std::shared_ptr<storm::logic::Formula const> formula;
236 };
237 Input buildPrism(std::string const& programFile, std::string const& formulaAsString, std::string const& constantsAsString = "") const {
238 // Parse and build input
239 storm::prism::Program program = storm::api::parseProgram(programFile);
240 program = program.preprocess(constantsAsString);
241 Input input;
242 input.formula = storm::api::parsePropertiesForPrismProgram(formulaAsString, program).front().getRawFormula();
243 input.model = storm::api::buildSparseModel<ValueType>(program, {input.formula})->template as<storm::models::sparse::Pomdp<ValueType>>();
244
245 // Preprocess
246 storm::transformer::MakePOMDPCanonic<ValueType> makeCanonic(*input.model);
247 input.model = makeCanonic.transform();
248 EXPECT_TRUE(input.model->isCanonic());
249 if (TestType::preprocessingType == PreprocessingType::SelfloopReduction || TestType::preprocessingType == PreprocessingType::All) {
250 storm::transformer::GlobalPOMDPSelfLoopEliminator<ValueType> selfLoopEliminator(*input.model);
251 if (selfLoopEliminator.preservesFormula(*input.formula)) {
252 input.model = selfLoopEliminator.transform();
253 } else {
254 EXPECT_TRUE(input.formula->isOperatorFormula());
255 EXPECT_TRUE(input.formula->asOperatorFormula().hasOptimalityType());
256 bool maximizing = storm::solver::maximize(input.formula->asOperatorFormula().getOptimalityType());
257 // Valid reasons for unpreserved formulas:
258 EXPECT_TRUE(maximizing || input.formula->isProbabilityOperatorFormula());
259 EXPECT_TRUE(!maximizing || input.formula->isRewardOperatorFormula());
260 }
261 }
262 if (TestType::preprocessingType == PreprocessingType::QualitativeReduction || TestType::preprocessingType == PreprocessingType::All) {
263 EXPECT_TRUE(input.formula->isOperatorFormula());
264 EXPECT_TRUE(input.formula->asOperatorFormula().hasOptimalityType());
265 if (input.formula->isProbabilityOperatorFormula() && storm::solver::maximize(input.formula->asOperatorFormula().getOptimalityType())) {
266 storm::analysis::QualitativeAnalysisOnGraphs<ValueType> qualitativeAnalysis(*input.model);
267 storm::storage::BitVector prob0States = qualitativeAnalysis.analyseProb0(input.formula->asProbabilityOperatorFormula());
268 storm::storage::BitVector prob1States = qualitativeAnalysis.analyseProb1(input.formula->asProbabilityOperatorFormula());
269 storm::pomdp::transformer::KnownProbabilityTransformer<ValueType> kpt;
270 input.model = kpt.transform(*input.model, prob0States, prob1States);
271 }
272 }
273 EXPECT_TRUE(input.model->isCanonic());
274 return input;
275 }
276 ValueType precision() const {
277 return TestType::precision();
278 }
279 ValueType modelcheckingPrecision() const {
280 if (TestType::isExactModelChecking) {
281 return storm::utility::zero<ValueType>();
282 } else {
283 return storm::utility::convertNumber<ValueType>(1e-6);
284 }
285 }
286 bool isExact() const {
287 return TestType::isExactModelChecking;
288 }
289
290 private:
291 storm::Environment _environment;
292};
293
294typedef ::testing::Types<DefaultDoubleVIEnvironment, SelfloopReductionDefaultDoubleVIEnvironment, QualitativeReductionDefaultDoubleVIEnvironment,
295 PreprocessedDefaultDoubleVIEnvironment, FineDoubleVIEnvironment, RefineDoubleVIEnvironment, PreprocessedRefineDoubleVIEnvironment,
296 DefaultDoubleOVIEnvironment, DefaultRationalPIEnvironment, PreprocessedDefaultRationalPIEnvironment>
297 TestingTypes;
298
299TYPED_TEST_SUITE(BeliefExplorationPomdpModelCheckerTest, TestingTypes, );
300
301TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax) {
302 typedef typename TestFixture::ValueType ValueType;
303
304 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
305 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
306 auto result = checker.check(this->env(), *data.formula);
307
308 ValueType expected = this->parseNumber("7/10");
309 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
310 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
311 EXPECT_LE(result.diff(), this->precision())
312 << "Result [" << result.lowerBound << ", " << result.upperBound
313 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
314}
315
316TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax_SE) {
317 typedef typename TestFixture::ValueType ValueType;
318
319 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
320 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
321 this->optionsWithStateElimination());
322 auto result = checker.check(this->env(), *data.formula);
323
324 ValueType expected = this->parseNumber("7/10");
325 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
326 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
327 EXPECT_LE(result.diff(), this->precision())
328 << "Result [" << result.lowerBound << ", " << result.upperBound
329 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
330}
331
332TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin) {
333 typedef typename TestFixture::ValueType ValueType;
334
335 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
336 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
337 auto result = checker.check(this->env(), *data.formula);
338
339 ValueType expected = this->parseNumber("3/10");
340 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
341 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
342 EXPECT_LE(result.diff(), this->precision())
343 << "Result [" << result.lowerBound << ", " << result.upperBound
344 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
345}
346
347TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin_SE) {
348 typedef typename TestFixture::ValueType ValueType;
349
350 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
351 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
352 this->optionsWithStateElimination());
353 auto result = checker.check(this->env(), *data.formula);
354
355 ValueType expected = this->parseNumber("3/10");
356 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
357 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
358 EXPECT_LE(result.diff(), this->precision())
359 << "Result [" << result.lowerBound << ", " << result.upperBound
360 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
361}
362
363TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax) {
364 typedef typename TestFixture::ValueType ValueType;
365
366 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
367 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
368 auto result = checker.check(this->env(), *data.formula);
369
370 ValueType expected = this->parseNumber("7/10");
371 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
372 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
373 EXPECT_LE(result.diff(), this->precision())
374 << "Result [" << result.lowerBound << ", " << result.upperBound
375 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
376}
377
378TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax_SE) {
379 typedef typename TestFixture::ValueType ValueType;
380
381 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
382 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
383 this->optionsWithStateElimination());
384 auto result = checker.check(this->env(), *data.formula);
385
386 ValueType expected = this->parseNumber("7/10");
387 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
388 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
389 EXPECT_LE(result.diff(), this->precision())
390 << "Result [" << result.lowerBound << ", " << result.upperBound
391 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
392}
393
394TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin) {
395 typedef typename TestFixture::ValueType ValueType;
396
397 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
398 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
399 auto result = checker.check(this->env(), *data.formula);
400
401 ValueType expected = this->parseNumber("3/10");
402 if (this->isExact()) {
403 // This model's value can only be approximated arbitrarily close but never reached
404 // Exact arithmetics will thus not reach the value with absoulute precision either.
405 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-5);
406 EXPECT_LE(result.lowerBound, expected + approxPrecision);
407 EXPECT_GE(result.upperBound, expected - approxPrecision);
408 } else {
409 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
410 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
411 }
412 EXPECT_LE(result.diff(), this->precision())
413 << "Result [" << result.lowerBound << ", " << result.upperBound
414 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
415}
416
417TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin_SE) {
418 typedef typename TestFixture::ValueType ValueType;
419
420 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
421 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
422 this->optionsWithStateElimination());
423 auto result = checker.check(this->env(), *data.formula);
424
425 ValueType expected = this->parseNumber("3/10");
426 if (this->isExact()) {
427 // This model's value can only be approximated arbitrarily close but never reached
428 // Exact arithmetics will thus not reach the value with absoulute precision either.
429 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-5);
430 EXPECT_LE(result.lowerBound, expected + approxPrecision);
431 EXPECT_GE(result.upperBound, expected - approxPrecision);
432 } else {
433 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
434 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
435 }
436 EXPECT_LE(result.diff(), this->precision())
437 << "Result [" << result.lowerBound << ", " << result.upperBound
438 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
439}
440
441TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax) {
442 typedef typename TestFixture::ValueType ValueType;
443
444 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
445 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
446 auto result = checker.check(this->env(), *data.formula);
447
448 ValueType expected = this->parseNumber("29/50");
449 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
450 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
451 EXPECT_LE(result.diff(), this->precision())
452 << "Result [" << result.lowerBound << ", " << result.upperBound
453 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
454}
455
456TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax_SE) {
457 typedef typename TestFixture::ValueType ValueType;
458
459 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
460 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
461 this->optionsWithStateElimination());
462 auto result = checker.check(this->env(), *data.formula);
463
464 ValueType expected = this->parseNumber("29/50");
465 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
466 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
467 EXPECT_LE(result.diff(), this->precision())
468 << "Result [" << result.lowerBound << ", " << result.upperBound
469 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
470}
471
472TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin) {
473 typedef typename TestFixture::ValueType ValueType;
474
475 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
476 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
477 auto result = checker.check(this->env(), *data.formula);
478
479 ValueType expected = this->parseNumber("19/50");
480 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
481 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
482 EXPECT_LE(result.diff(), this->precision())
483 << "Result [" << result.lowerBound << ", " << result.upperBound
484 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
485}
486
487TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin_SE) {
488 typedef typename TestFixture::ValueType ValueType;
489
490 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
491 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
492 this->optionsWithStateElimination());
493 auto result = checker.check(this->env(), *data.formula);
494
495 ValueType expected = this->parseNumber("19/50");
496 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
497 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
498 EXPECT_LE(result.diff(), this->precision())
499 << "Result [" << result.lowerBound << ", " << result.upperBound
500 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
501}
502
503TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax) {
504 typedef typename TestFixture::ValueType ValueType;
505
506 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
507 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
508 auto result = checker.check(this->env(), *data.formula);
509
510 ValueType expected = this->parseNumber("29/30");
511 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
512 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
513 EXPECT_LE(result.diff(), this->precision())
514 << "Result [" << result.lowerBound << ", " << result.upperBound
515 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
516}
517
518TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax_SE) {
519 typedef typename TestFixture::ValueType ValueType;
520
521 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
522 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
523 this->optionsWithStateElimination());
524 auto result = checker.check(this->env(), *data.formula);
525
526 ValueType expected = this->parseNumber("29/30");
527 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
528 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
529 EXPECT_LE(result.diff(), this->precision())
530 << "Result [" << result.lowerBound << ", " << result.upperBound
531 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
532}
533
534TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin) {
535 typedef typename TestFixture::ValueType ValueType;
536
537 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
538 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
539 auto result = checker.check(this->env(), *data.formula);
540
541 ValueType expected = this->parseNumber("19/30");
542 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
543 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
544 EXPECT_LE(result.diff(), this->precision())
545 << "Result [" << result.lowerBound << ", " << result.upperBound
546 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
547}
548
549TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin_SE) {
550 typedef typename TestFixture::ValueType ValueType;
551
552 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
553 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
554 this->optionsWithStateElimination());
555 auto result = checker.check(this->env(), *data.formula);
556
557 ValueType expected = this->parseNumber("19/30");
558 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
559 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
560 EXPECT_LE(result.diff(), this->precision())
561 << "Result [" << result.lowerBound << ", " << result.upperBound
562 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
563}
564
565TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin) {
566 typedef typename TestFixture::ValueType ValueType;
567
568 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
569 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
570 auto result = checker.check(this->env(), *data.formula);
571
572 ValueType expected = this->parseNumber("74/91");
573 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
574 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
575 // Use relative difference of bounds for this one
576 EXPECT_LE(result.diff(), this->precision())
577 << "Result [" << result.lowerBound << ", " << result.upperBound
578 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
579}
580
581TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin_SE) {
582 typedef typename TestFixture::ValueType ValueType;
583
584 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
585 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
586 this->optionsWithStateElimination());
587 auto result = checker.check(this->env(), *data.formula);
588
589 ValueType expected = this->parseNumber("74/91");
590 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
591 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
592 // Use relative difference of bounds for this one
593 EXPECT_LE(result.diff(), this->precision())
594 << "Result [" << result.lowerBound << ", " << result.upperBound
595 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
596}
597
598TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax) {
599 typedef typename TestFixture::ValueType ValueType;
600
601 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
602 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
603 auto result = checker.check(this->env(), *data.formula);
604
605 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
606 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
607}
608
609TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax_SE) {
610 typedef typename TestFixture::ValueType ValueType;
611
612 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
613 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
614 this->optionsWithStateElimination());
615 auto result = checker.check(this->env(), *data.formula);
616
617 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
618 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
619}
620
621TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin) {
622 typedef typename TestFixture::ValueType ValueType;
623
624 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
625 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
626 auto result = checker.check(this->env(), *data.formula);
627
628 ValueType expected = this->parseNumber("80/91");
629 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
630 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
631 // Use relative difference of bounds for this one
632 EXPECT_LE(result.diff(), this->precision())
633 << "Result [" << result.lowerBound << ", " << result.upperBound
634 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
635}
636
637TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin_SE) {
638 typedef typename TestFixture::ValueType ValueType;
639
640 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
641 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
642 this->optionsWithStateElimination());
643 auto result = checker.check(this->env(), *data.formula);
644
645 ValueType expected = this->parseNumber("80/91");
646 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
647 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
648 // Use relative difference of bounds for this one
649 EXPECT_LE(result.diff(), this->precision())
650 << "Result [" << result.lowerBound << ", " << result.upperBound
651 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
652}
653
654TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax) {
655 typedef typename TestFixture::ValueType ValueType;
656
657 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
658 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
659 auto result = checker.check(this->env(), *data.formula);
660
661 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
662 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
663}
664
665TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax_SE) {
666 typedef typename TestFixture::ValueType ValueType;
667
668 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
669 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
670 this->optionsWithStateElimination());
671 auto result = checker.check(this->env(), *data.formula);
672
673 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
674 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
675}
676
677TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax) {
678 typedef typename TestFixture::ValueType ValueType;
679
680 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
681 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
682 auto result = checker.check(this->env(), *data.formula);
683
684 ValueType expected = this->parseNumber("38/155");
685 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
686 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
687 // Use relative difference of bounds for this one
688 EXPECT_LE(result.diff(), this->precision())
689 << "Result [" << result.lowerBound << ", " << result.upperBound
690 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
691}
692
693TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax_SE) {
694 typedef typename TestFixture::ValueType ValueType;
695
696 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
697 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
698 this->optionsWithStateElimination());
699 auto result = checker.check(this->env(), *data.formula);
700
701 ValueType expected = this->parseNumber("38/155");
702 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
703 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
704 // Use relative difference of bounds for this one
705 EXPECT_LE(result.diff(), this->precision())
706 << "Result [" << result.lowerBound << ", " << result.upperBound
707 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
708}
709
710TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin) {
711 typedef typename TestFixture::ValueType ValueType;
712
713 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
714 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
715 auto result = checker.check(this->env(), *data.formula);
716
717 ValueType expected = this->parseNumber("0");
718 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
719 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
720 // Use relative difference of bounds for this one
721 EXPECT_LE(result.diff(), this->precision())
722 << "Result [" << result.lowerBound << ", " << result.upperBound
723 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
724}
725
726TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin_SE) {
727 typedef typename TestFixture::ValueType ValueType;
728
729 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
730 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
731 this->optionsWithStateElimination());
732 auto result = checker.check(this->env(), *data.formula);
733
734 ValueType expected = this->parseNumber("0");
735 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
736 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
737 // Use relative difference of bounds for this one
738 EXPECT_LE(result.diff(), this->precision())
739 << "Result [" << result.lowerBound << ", " << result.upperBound
740 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
741}
742
743TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax_Clip) {
744 typedef typename TestFixture::ValueType ValueType;
745
746 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
747 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
748 auto result = checker.check(this->env(), *data.formula);
749
750 ValueType expected = this->parseNumber("7/10");
751 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
752 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
753 EXPECT_LE(result.diff(), this->precision())
754 << "Result [" << result.lowerBound << ", " << result.upperBound
755 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
756}
757
758TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin_Clip) {
759 typedef typename TestFixture::ValueType ValueType;
760
761 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
762 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
763 auto result = checker.check(this->env(), *data.formula);
764
765 ValueType expected = this->parseNumber("3/10");
766 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
767 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
768 EXPECT_LE(result.diff(), this->precision())
769 << "Result [" << result.lowerBound << ", " << result.upperBound
770 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
771}
772
773TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax_Clip) {
774 typedef typename TestFixture::ValueType ValueType;
775
776 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
777 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
778 auto result = checker.check(this->env(), *data.formula);
779
780 ValueType expected = this->parseNumber("7/10");
781 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
782 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
783 EXPECT_LE(result.diff(), this->precision())
784 << "Result [" << result.lowerBound << ", " << result.upperBound
785 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
786}
787
788TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin_Clip) {
789 typedef typename TestFixture::ValueType ValueType;
790
791 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
792 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
793 auto result = checker.check(this->env(), *data.formula);
794
795 ValueType expected = this->parseNumber("3/10");
796 if (this->isExact()) {
797 // This model's value can only be approximated arbitrarily close but never reached
798 // Exact arithmetics will thus not reach the value with absoulute precision either.
799 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-4);
800 EXPECT_LE(result.lowerBound, expected + approxPrecision);
801 EXPECT_GE(result.upperBound, expected - approxPrecision);
802 } else {
803 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision() * 10);
804 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision() * 10);
805 }
806 EXPECT_LE(result.diff(), this->precision())
807 << "Result [" << result.lowerBound << ", " << result.upperBound
808 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
809}
810
811TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax_Clip) {
812 typedef typename TestFixture::ValueType ValueType;
813
814 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
815 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
816 auto result = checker.check(this->env(), *data.formula);
817
818 ValueType expected = this->parseNumber("29/50");
819 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
820 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
821 EXPECT_LE(result.diff(), this->precision())
822 << "Result [" << result.lowerBound << ", " << result.upperBound
823 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
824}
825
826TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin_Clip) {
827 typedef typename TestFixture::ValueType ValueType;
828
829 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
830 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
831 auto result = checker.check(this->env(), *data.formula);
832
833 ValueType expected = this->parseNumber("19/50");
834 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
835 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
836 EXPECT_LE(result.diff(), this->precision())
837 << "Result [" << result.lowerBound << ", " << result.upperBound
838 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
839}
840
841TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax_Clip) {
842 typedef typename TestFixture::ValueType ValueType;
843
844 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
845 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
846 auto result = checker.check(this->env(), *data.formula);
847
848 ValueType expected = this->parseNumber("29/30");
849 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
850 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
851 EXPECT_LE(result.diff(), this->precision())
852 << "Result [" << result.lowerBound << ", " << result.upperBound
853 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
854}
855
856TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin_Clip) {
857 typedef typename TestFixture::ValueType ValueType;
858
859 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
860 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
861 auto result = checker.check(this->env(), *data.formula);
862
863 ValueType expected = this->parseNumber("19/30");
864 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
865 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
866 EXPECT_LE(result.diff(), this->precision())
867 << "Result [" << result.lowerBound << ", " << result.upperBound
868 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
869}
870
871TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin_Clip) {
872 typedef typename TestFixture::ValueType ValueType;
873
874 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
875 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
876 auto result = checker.check(this->env(), *data.formula);
877
878 ValueType expected = this->parseNumber("74/91");
879 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
880 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
881 // Use relative difference of bounds for this one
882 EXPECT_LE(result.diff(), this->precision())
883 << "Result [" << result.lowerBound << ", " << result.upperBound
884 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
885}
886
887TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax_Clip) {
888 typedef typename TestFixture::ValueType ValueType;
889
890 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
891 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
892 auto result = checker.check(this->env(), *data.formula);
893
894 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
895 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
896}
897
898TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin_Clip) {
899 typedef typename TestFixture::ValueType ValueType;
900
901 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
902 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
903 auto result = checker.check(this->env(), *data.formula);
904
905 ValueType expected = this->parseNumber("80/91");
906 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
907 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
908 // Use relative difference of bounds for this one
909 EXPECT_LE(result.diff(), this->precision())
910 << "Result [" << result.lowerBound << ", " << result.upperBound
911 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
912}
913
914TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax_Clip) {
915 typedef typename TestFixture::ValueType ValueType;
916
917 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
918 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
919 auto result = checker.check(this->env(), *data.formula);
920
921 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
922 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
923}
924
925TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax_Clip) {
926 typedef typename TestFixture::ValueType ValueType;
927
928 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
929 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
930 auto result = checker.check(this->env(), *data.formula);
931
932 ValueType expected = this->parseNumber("38/155");
933 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
934 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
935 // Use relative difference of bounds for this one
936 EXPECT_LE(result.diff(), this->precision())
937 << "Result [" << result.lowerBound << ", " << result.upperBound
938 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
939}
940
941TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin_Clip) {
942 typedef typename TestFixture::ValueType ValueType;
943
944 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
945 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
946 auto result = checker.check(this->env(), *data.formula);
947
948 ValueType expected = this->parseNumber("0");
949 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
950 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
951 // Use relative difference of bounds for this one
952 EXPECT_LE(result.diff(), this->precision())
953 << "Result [" << result.lowerBound << ", " << result.upperBound
954 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
955}
956
957} // namespace
DefaultDoubleVIEnvironment::adaptOptions
static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions< ValueType > &)
Definition BeliefExplorationAPITest.cpp:26
DefaultDoubleVIEnvironment::createEnvironment
static storm::Environment createEnvironment()
Definition BeliefExplorationAPITest.cpp:16
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:26
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::MinMaxSolverEnvironment::setMethod
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
Definition MinMaxSolverEnvironment.cpp:43
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:48
storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker
Model checker for checking reachability queries on POMDPs using approximations based on exploration o...
Definition BeliefExplorationPomdpModelChecker.h:50
storm::pomdp::transformer::KnownProbabilityTransformer::transform
std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > transform(storm::models::sparse::Pomdp< ValueType > const &pomdp, storm::storage::BitVector &prob0States, storm::storage::BitVector &prob1States)
Definition KnownProbabilityTransformer.cpp:13
storm::prism::Program::preprocess
Program preprocess(std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
Preprocesses the program by defining the given constant definitions, substituting constants and formu...
Definition Program.cpp:1170
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options, typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &explorationOptions=typename storm::builder::ExplicitModelBuilder< ValueType >::Options())
Definition builder.h:117
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:55
storm::solver::maximize
bool constexpr maximize(OptimizationDirection d)
Definition OptimizationDirection.h:13
storm::utility::zero
ValueType zero()
Definition constants.cpp:24
storm::utility::isInfinity
bool isInfinity(ValueType const &a)
Definition constants.cpp:111
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:143
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:64
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h