Storm 1.13.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 = storm::utility::prism::preprocess(program, 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 bool isExact() const {
286 return TestType::isExactModelChecking;
287 }
288
289 private:
290 storm::Environment _environment;
291};
292
293typedef ::testing::Types<DefaultDoubleVIEnvironment, SelfloopReductionDefaultDoubleVIEnvironment, QualitativeReductionDefaultDoubleVIEnvironment,
294 PreprocessedDefaultDoubleVIEnvironment, FineDoubleVIEnvironment, RefineDoubleVIEnvironment, PreprocessedRefineDoubleVIEnvironment,
295 DefaultDoubleOVIEnvironment, DefaultRationalPIEnvironment, PreprocessedDefaultRationalPIEnvironment>
296 TestingTypes;
297
298TYPED_TEST_SUITE(BeliefExplorationPomdpModelCheckerTest, TestingTypes, );
299
300TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax) {
301 typedef typename TestFixture::ValueType ValueType;
302
303 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
304 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
305 auto result = checker.check(this->env(), *data.formula);
306
307 ValueType expected = this->parseNumber("7/10");
308 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
309 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
310 EXPECT_LE(result.diff(), this->precision())
311 << "Result [" << result.lowerBound << ", " << result.upperBound
312 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
313}
314
315TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax_SE) {
316 typedef typename TestFixture::ValueType ValueType;
317
318 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
319 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
320 this->optionsWithStateElimination());
321 auto result = checker.check(this->env(), *data.formula);
322
323 ValueType expected = this->parseNumber("7/10");
324 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
325 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
326 EXPECT_LE(result.diff(), this->precision())
327 << "Result [" << result.lowerBound << ", " << result.upperBound
328 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
329}
330
331TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin) {
332 typedef typename TestFixture::ValueType ValueType;
333
334 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
335 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
336 auto result = checker.check(this->env(), *data.formula);
337
338 ValueType expected = this->parseNumber("3/10");
339 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
340 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
341 EXPECT_LE(result.diff(), this->precision())
342 << "Result [" << result.lowerBound << ", " << result.upperBound
343 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
344}
345
346TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin_SE) {
347 typedef typename TestFixture::ValueType ValueType;
348
349 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
350 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
351 this->optionsWithStateElimination());
352 auto result = checker.check(this->env(), *data.formula);
353
354 ValueType expected = this->parseNumber("3/10");
355 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
356 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
357 EXPECT_LE(result.diff(), this->precision())
358 << "Result [" << result.lowerBound << ", " << result.upperBound
359 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
360}
361
362TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax) {
363 typedef typename TestFixture::ValueType ValueType;
364
365 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
366 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
367 auto result = checker.check(this->env(), *data.formula);
368
369 ValueType expected = this->parseNumber("7/10");
370 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
371 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
372 EXPECT_LE(result.diff(), this->precision())
373 << "Result [" << result.lowerBound << ", " << result.upperBound
374 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
375}
376
377TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax_SE) {
378 typedef typename TestFixture::ValueType ValueType;
379
380 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
381 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
382 this->optionsWithStateElimination());
383 auto result = checker.check(this->env(), *data.formula);
384
385 ValueType expected = this->parseNumber("7/10");
386 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
387 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
388 EXPECT_LE(result.diff(), this->precision())
389 << "Result [" << result.lowerBound << ", " << result.upperBound
390 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
391}
392
393TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin) {
394 typedef typename TestFixture::ValueType ValueType;
395
396 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
397 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
398 auto result = checker.check(this->env(), *data.formula);
399
400 ValueType expected = this->parseNumber("3/10");
401 if (this->isExact()) {
402 // This model's value can only be approximated arbitrarily close but never reached
403 // Exact arithmetics will thus not reach the value with absoulute precision either.
404 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-5);
405 EXPECT_LE(result.lowerBound, expected + approxPrecision);
406 EXPECT_GE(result.upperBound, expected - approxPrecision);
407 } else {
408 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
409 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
410 }
411 EXPECT_LE(result.diff(), this->precision())
412 << "Result [" << result.lowerBound << ", " << result.upperBound
413 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
414}
415
416TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin_SE) {
417 typedef typename TestFixture::ValueType ValueType;
418
419 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
420 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
421 this->optionsWithStateElimination());
422 auto result = checker.check(this->env(), *data.formula);
423
424 ValueType expected = this->parseNumber("3/10");
425 if (this->isExact()) {
426 // This model's value can only be approximated arbitrarily close but never reached
427 // Exact arithmetics will thus not reach the value with absoulute precision either.
428 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-5);
429 EXPECT_LE(result.lowerBound, expected + approxPrecision);
430 EXPECT_GE(result.upperBound, expected - approxPrecision);
431 } else {
432 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
433 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
434 }
435 EXPECT_LE(result.diff(), this->precision())
436 << "Result [" << result.lowerBound << ", " << result.upperBound
437 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
438}
439
440TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax) {
441 typedef typename TestFixture::ValueType ValueType;
442
443 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
444 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
445 auto result = checker.check(this->env(), *data.formula);
446
447 ValueType expected = this->parseNumber("29/50");
448 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
449 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
450 EXPECT_LE(result.diff(), this->precision())
451 << "Result [" << result.lowerBound << ", " << result.upperBound
452 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
453}
454
455TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax_SE) {
456 typedef typename TestFixture::ValueType ValueType;
457
458 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
459 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
460 this->optionsWithStateElimination());
461 auto result = checker.check(this->env(), *data.formula);
462
463 ValueType expected = this->parseNumber("29/50");
464 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
465 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
466 EXPECT_LE(result.diff(), this->precision())
467 << "Result [" << result.lowerBound << ", " << result.upperBound
468 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
469}
470
471TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin) {
472 typedef typename TestFixture::ValueType ValueType;
473
474 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
475 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
476 auto result = checker.check(this->env(), *data.formula);
477
478 ValueType expected = this->parseNumber("19/50");
479 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
480 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
481 EXPECT_LE(result.diff(), this->precision())
482 << "Result [" << result.lowerBound << ", " << result.upperBound
483 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
484}
485
486TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin_SE) {
487 typedef typename TestFixture::ValueType ValueType;
488
489 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
490 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
491 this->optionsWithStateElimination());
492 auto result = checker.check(this->env(), *data.formula);
493
494 ValueType expected = this->parseNumber("19/50");
495 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
496 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
497 EXPECT_LE(result.diff(), this->precision())
498 << "Result [" << result.lowerBound << ", " << result.upperBound
499 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
500}
501
502TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax) {
503 typedef typename TestFixture::ValueType ValueType;
504
505 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
506 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
507 auto result = checker.check(this->env(), *data.formula);
508
509 ValueType expected = this->parseNumber("29/30");
510 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
511 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
512 EXPECT_LE(result.diff(), this->precision())
513 << "Result [" << result.lowerBound << ", " << result.upperBound
514 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
515}
516
517TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax_SE) {
518 typedef typename TestFixture::ValueType ValueType;
519
520 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
521 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
522 this->optionsWithStateElimination());
523 auto result = checker.check(this->env(), *data.formula);
524
525 ValueType expected = this->parseNumber("29/30");
526 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
527 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
528 EXPECT_LE(result.diff(), this->precision())
529 << "Result [" << result.lowerBound << ", " << result.upperBound
530 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
531}
532
533TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin) {
534 typedef typename TestFixture::ValueType ValueType;
535
536 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
537 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
538 auto result = checker.check(this->env(), *data.formula);
539
540 ValueType expected = this->parseNumber("19/30");
541 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
542 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
543 EXPECT_LE(result.diff(), this->precision())
544 << "Result [" << result.lowerBound << ", " << result.upperBound
545 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
546}
547
548TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin_SE) {
549 typedef typename TestFixture::ValueType ValueType;
550
551 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
552 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
553 this->optionsWithStateElimination());
554 auto result = checker.check(this->env(), *data.formula);
555
556 ValueType expected = this->parseNumber("19/30");
557 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
558 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
559 EXPECT_LE(result.diff(), this->precision())
560 << "Result [" << result.lowerBound << ", " << result.upperBound
561 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
562}
563
564TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin) {
565 typedef typename TestFixture::ValueType ValueType;
566
567 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
568 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
569 auto result = checker.check(this->env(), *data.formula);
570
571 ValueType expected = this->parseNumber("74/91");
572 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
573 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
574 // Use relative difference of bounds for this one
575 EXPECT_LE(result.diff(), this->precision())
576 << "Result [" << result.lowerBound << ", " << result.upperBound
577 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
578}
579
580TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin_SE) {
581 typedef typename TestFixture::ValueType ValueType;
582
583 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
584 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
585 this->optionsWithStateElimination());
586 auto result = checker.check(this->env(), *data.formula);
587
588 ValueType expected = this->parseNumber("74/91");
589 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
590 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
591 // Use relative difference of bounds for this one
592 EXPECT_LE(result.diff(), this->precision())
593 << "Result [" << result.lowerBound << ", " << result.upperBound
594 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
595}
596
597TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax) {
598 typedef typename TestFixture::ValueType ValueType;
599
600 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
601 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
602 auto result = checker.check(this->env(), *data.formula);
603
604 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
605 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
606}
607
608TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax_SE) {
609 typedef typename TestFixture::ValueType ValueType;
610
611 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
612 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
613 this->optionsWithStateElimination());
614 auto result = checker.check(this->env(), *data.formula);
615
616 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
617 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
618}
619
620TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin) {
621 typedef typename TestFixture::ValueType ValueType;
622
623 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
624 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
625 auto result = checker.check(this->env(), *data.formula);
626
627 ValueType expected = this->parseNumber("80/91");
628 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
629 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
630 // Use relative difference of bounds for this one
631 EXPECT_LE(result.diff(), this->precision())
632 << "Result [" << result.lowerBound << ", " << result.upperBound
633 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
634}
635
636TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin_SE) {
637 typedef typename TestFixture::ValueType ValueType;
638
639 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
640 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
641 this->optionsWithStateElimination());
642 auto result = checker.check(this->env(), *data.formula);
643
644 ValueType expected = this->parseNumber("80/91");
645 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
646 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
647 // Use relative difference of bounds for this one
648 EXPECT_LE(result.diff(), this->precision())
649 << "Result [" << result.lowerBound << ", " << result.upperBound
650 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
651}
652
653TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax) {
654 typedef typename TestFixture::ValueType ValueType;
655
656 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
657 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
658 auto result = checker.check(this->env(), *data.formula);
659
660 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
661 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
662}
663
664TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax_SE) {
665 typedef typename TestFixture::ValueType ValueType;
666
667 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
668 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
669 this->optionsWithStateElimination());
670 auto result = checker.check(this->env(), *data.formula);
671
672 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
673 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
674}
675
676TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax) {
677 typedef typename TestFixture::ValueType ValueType;
678
679 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
680 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
681 auto result = checker.check(this->env(), *data.formula);
682
683 ValueType expected = this->parseNumber("38/155");
684 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
685 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
686 // Use relative difference of bounds for this one
687 EXPECT_LE(result.diff(), this->precision())
688 << "Result [" << result.lowerBound << ", " << result.upperBound
689 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
690}
691
692TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax_SE) {
693 typedef typename TestFixture::ValueType ValueType;
694
695 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
696 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
697 this->optionsWithStateElimination());
698 auto result = checker.check(this->env(), *data.formula);
699
700 ValueType expected = this->parseNumber("38/155");
701 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
702 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
703 // Use relative difference of bounds for this one
704 EXPECT_LE(result.diff(), this->precision())
705 << "Result [" << result.lowerBound << ", " << result.upperBound
706 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
707}
708
709TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin) {
710 typedef typename TestFixture::ValueType ValueType;
711
712 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
713 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->options());
714 auto result = checker.check(this->env(), *data.formula);
715
716 ValueType expected = this->parseNumber("0");
717 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
718 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
719 // Use relative difference of bounds for this one
720 EXPECT_LE(result.diff(), this->precision())
721 << "Result [" << result.lowerBound << ", " << result.upperBound
722 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
723}
724
725TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin_SE) {
726 typedef typename TestFixture::ValueType ValueType;
727
728 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
729 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model,
730 this->optionsWithStateElimination());
731 auto result = checker.check(this->env(), *data.formula);
732
733 ValueType expected = this->parseNumber("0");
734 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
735 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
736 // Use relative difference of bounds for this one
737 EXPECT_LE(result.diff(), this->precision())
738 << "Result [" << result.lowerBound << ", " << result.upperBound
739 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
740}
741
742TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax_Clip) {
743 typedef typename TestFixture::ValueType ValueType;
744
745 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
746 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
747 auto result = checker.check(this->env(), *data.formula);
748
749 ValueType expected = this->parseNumber("7/10");
750 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
751 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
752 EXPECT_LE(result.diff(), this->precision())
753 << "Result [" << result.lowerBound << ", " << result.upperBound
754 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
755}
756
757TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin_Clip) {
758 typedef typename TestFixture::ValueType ValueType;
759
760 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
761 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
762 auto result = checker.check(this->env(), *data.formula);
763
764 ValueType expected = this->parseNumber("3/10");
765 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
766 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
767 EXPECT_LE(result.diff(), this->precision())
768 << "Result [" << result.lowerBound << ", " << result.upperBound
769 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
770}
771
772TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax_Clip) {
773 typedef typename TestFixture::ValueType ValueType;
774
775 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
776 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
777 auto result = checker.check(this->env(), *data.formula);
778
779 ValueType expected = this->parseNumber("7/10");
780 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
781 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
782 EXPECT_LE(result.diff(), this->precision())
783 << "Result [" << result.lowerBound << ", " << result.upperBound
784 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
785}
786
787TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin_Clip) {
788 typedef typename TestFixture::ValueType ValueType;
789
790 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
791 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
792 auto result = checker.check(this->env(), *data.formula);
793
794 ValueType expected = this->parseNumber("3/10");
795 if (this->isExact()) {
796 // This model's value can only be approximated arbitrarily close but never reached
797 // Exact arithmetics will thus not reach the value with absoulute precision either.
798 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-4);
799 EXPECT_LE(result.lowerBound, expected + approxPrecision);
800 EXPECT_GE(result.upperBound, expected - approxPrecision);
801 } else {
802 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision() * 10);
803 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision() * 10);
804 }
805 EXPECT_LE(result.diff(), this->precision())
806 << "Result [" << result.lowerBound << ", " << result.upperBound
807 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
808}
809
810TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax_Clip) {
811 typedef typename TestFixture::ValueType ValueType;
812
813 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
814 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
815 auto result = checker.check(this->env(), *data.formula);
816
817 ValueType expected = this->parseNumber("29/50");
818 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
819 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
820 EXPECT_LE(result.diff(), this->precision())
821 << "Result [" << result.lowerBound << ", " << result.upperBound
822 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
823}
824
825TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin_Clip) {
826 typedef typename TestFixture::ValueType ValueType;
827
828 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
829 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
830 auto result = checker.check(this->env(), *data.formula);
831
832 ValueType expected = this->parseNumber("19/50");
833 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
834 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
835 EXPECT_LE(result.diff(), this->precision())
836 << "Result [" << result.lowerBound << ", " << result.upperBound
837 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
838}
839
840TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax_Clip) {
841 typedef typename TestFixture::ValueType ValueType;
842
843 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
844 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
845 auto result = checker.check(this->env(), *data.formula);
846
847 ValueType expected = this->parseNumber("29/30");
848 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
849 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
850 EXPECT_LE(result.diff(), this->precision())
851 << "Result [" << result.lowerBound << ", " << result.upperBound
852 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
853}
854
855TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin_Clip) {
856 typedef typename TestFixture::ValueType ValueType;
857
858 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
859 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
860 auto result = checker.check(this->env(), *data.formula);
861
862 ValueType expected = this->parseNumber("19/30");
863 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
864 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
865 EXPECT_LE(result.diff(), this->precision())
866 << "Result [" << result.lowerBound << ", " << result.upperBound
867 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
868}
869
870TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin_Clip) {
871 typedef typename TestFixture::ValueType ValueType;
872
873 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
874 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
875 auto result = checker.check(this->env(), *data.formula);
876
877 ValueType expected = this->parseNumber("74/91");
878 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
879 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
880 // Use relative difference of bounds for this one
881 EXPECT_LE(result.diff(), this->precision())
882 << "Result [" << result.lowerBound << ", " << result.upperBound
883 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
884}
885
886TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax_Clip) {
887 typedef typename TestFixture::ValueType ValueType;
888
889 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
890 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
891 auto result = checker.check(this->env(), *data.formula);
892
893 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
894 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
895}
896
897TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin_Clip) {
898 typedef typename TestFixture::ValueType ValueType;
899
900 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
901 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
902 auto result = checker.check(this->env(), *data.formula);
903
904 ValueType expected = this->parseNumber("80/91");
905 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
906 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
907 // Use relative difference of bounds for this one
908 EXPECT_LE(result.diff(), this->precision())
909 << "Result [" << result.lowerBound << ", " << result.upperBound
910 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
911}
912
913TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax_Clip) {
914 typedef typename TestFixture::ValueType ValueType;
915
916 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
917 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
918 auto result = checker.check(this->env(), *data.formula);
919
920 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
921 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
922}
923
924TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax_Clip) {
925 typedef typename TestFixture::ValueType ValueType;
926
927 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
928 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
929 auto result = checker.check(this->env(), *data.formula);
930
931 ValueType expected = this->parseNumber("38/155");
932 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
933 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
934 // Use relative difference of bounds for this one
935 EXPECT_LE(result.diff(), this->precision())
936 << "Result [" << result.lowerBound << ", " << result.upperBound
937 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
938}
939
940TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin_Clip) {
941 typedef typename TestFixture::ValueType ValueType;
942
943 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
944 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
945 auto result = checker.check(this->env(), *data.formula);
946
947 ValueType expected = this->parseNumber("0");
948 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
949 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
950 // Use relative difference of bounds for this one
951 EXPECT_LE(result.diff(), this->precision())
952 << "Result [" << result.lowerBound << ", " << result.upperBound
953 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
954}
955
956} // 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:25
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:43
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::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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
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:14
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:13
storm::utility::zero
ValueType zero()
Definition constants.cpp:24
storm::utility::isInfinity
bool isInfinity(ValueType const &a)
Definition constants.cpp:108
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:135
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:62
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59
storm_gtest.h