Storm 1.11.1.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-pomdp/transformer/MakePOMDPCanonic.h"
10#include "storm/api/storm.h"
11#include "storm/environment/solver/MinMaxSolverEnvironment.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
742#if defined STORM_HAVE_Z3_OPTIMIZE
743
744TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmax_Clip) {
745 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
746 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
747 }
748 typedef typename TestFixture::ValueType ValueType;
749
750 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0");
751 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
752 auto result = checker.check(this->env(), *data.formula);
753
754 ValueType expected = this->parseNumber("7/10");
755 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
756 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
757 EXPECT_LE(result.diff(), this->precision())
758 << "Result [" << result.lowerBound << ", " << result.upperBound
759 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
760}
761
762TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Pmin_Clip) {
763 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
764 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
765 }
766 typedef typename TestFixture::ValueType ValueType;
767
768 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0");
769 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
770 auto result = checker.check(this->env(), *data.formula);
771
772 ValueType expected = this->parseNumber("3/10");
773 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
774 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
775 EXPECT_LE(result.diff(), this->precision())
776 << "Result [" << result.lowerBound << ", " << result.upperBound
777 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
778}
779
780TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmax_Clip) {
781 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
782 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
783 }
784 typedef typename TestFixture::ValueType ValueType;
785
786 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmax=? [F \"goal\" ]", "slippery=0.4");
787 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
788 auto result = checker.check(this->env(), *data.formula);
789
790 ValueType expected = this->parseNumber("7/10");
791 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
792 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
793 EXPECT_LE(result.diff(), this->precision())
794 << "Result [" << result.lowerBound << ", " << result.upperBound
795 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
796}
797
798TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Pmin_Clip) {
799 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
800 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
801 }
802 typedef typename TestFixture::ValueType ValueType;
803
804 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Pmin=? [F \"goal\" ]", "slippery=0.4");
805 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
806 auto result = checker.check(this->env(), *data.formula);
807
808 ValueType expected = this->parseNumber("3/10");
809 if (this->isExact()) {
810 // This model's value can only be approximated arbitrarily close but never reached
811 // Exact arithmetics will thus not reach the value with absoulute precision either.
812 ValueType approxPrecision = storm::utility::convertNumber<ValueType>(1e-4);
813 EXPECT_LE(result.lowerBound, expected + approxPrecision);
814 EXPECT_GE(result.upperBound, expected - approxPrecision);
815 } else {
816 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision() * 10);
817 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision() * 10);
818 }
819 EXPECT_LE(result.diff(), this->precision())
820 << "Result [" << result.lowerBound << ", " << result.upperBound
821 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
822}
823
824TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmax_Clip) {
825 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
826 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
827 }
828 typedef typename TestFixture::ValueType ValueType;
829
830 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0");
831 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
832 auto result = checker.check(this->env(), *data.formula);
833
834 ValueType expected = this->parseNumber("29/50");
835 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
836 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
837 EXPECT_LE(result.diff(), this->precision())
838 << "Result [" << result.lowerBound << ", " << result.upperBound
839 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
840}
841
842TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_Rmin_Clip) {
843 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
844 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
845 }
846 typedef typename TestFixture::ValueType ValueType;
847
848 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0");
849 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
850 auto result = checker.check(this->env(), *data.formula);
851
852 ValueType expected = this->parseNumber("19/50");
853 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
854 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
855 EXPECT_LE(result.diff(), this->precision())
856 << "Result [" << result.lowerBound << ", " << result.upperBound
857 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
858}
859
860TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmax_Clip) {
861 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
862 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
863 }
864 typedef typename TestFixture::ValueType ValueType;
865
866 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmax=? [F s>4 ]", "slippery=0.4");
867 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
868 auto result = checker.check(this->env(), *data.formula);
869
870 ValueType expected = this->parseNumber("29/30");
871 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
872 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
873 EXPECT_LE(result.diff(), this->precision())
874 << "Result [" << result.lowerBound << ", " << result.upperBound
875 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
876}
877
878TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, simple_slippery_Rmin_Clip) {
879 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
880 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
881 }
882 typedef typename TestFixture::ValueType ValueType;
883
884 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism", "Rmin=? [F s>4 ]", "slippery=0.4");
885 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
886 auto result = checker.check(this->env(), *data.formula);
887
888 ValueType expected = this->parseNumber("19/30");
889 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
890 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
891 EXPECT_LE(result.diff(), this->precision())
892 << "Result [" << result.lowerBound << ", " << result.upperBound
893 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
894}
895
896TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmin_Clip) {
897 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
898 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
899 }
900 typedef typename TestFixture::ValueType ValueType;
901
902 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0");
903 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
904 auto result = checker.check(this->env(), *data.formula);
905
906 ValueType expected = this->parseNumber("74/91");
907 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
908 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
909 // Use relative difference of bounds for this one
910 EXPECT_LE(result.diff(), this->precision())
911 << "Result [" << result.lowerBound << ", " << result.upperBound
912 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
913}
914
915TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_Rmax_Clip) {
916 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
917 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
918 }
919 typedef typename TestFixture::ValueType ValueType;
920
921 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0");
922 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
923 auto result = checker.check(this->env(), *data.formula);
924
925 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
926 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
927}
928
929TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmin_Clip) {
930 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
931 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
932 }
933 typedef typename TestFixture::ValueType ValueType;
934
935 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmin=? [F \"goal\"]", "sl=0.075");
936 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
937 auto result = checker.check(this->env(), *data.formula);
938
939 ValueType expected = this->parseNumber("80/91");
940 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
941 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
942 // Use relative difference of bounds for this one
943 EXPECT_LE(result.diff(), this->precision())
944 << "Result [" << result.lowerBound << ", " << result.upperBound
945 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
946}
947
948TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, maze2_slippery_Rmax_Clip) {
949 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
950 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
951 }
952 typedef typename TestFixture::ValueType ValueType;
953
954 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism", "Rmax=? [F \"goal\"]", "sl=0.075");
955 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
956 auto result = checker.check(this->env(), *data.formula);
957
958 EXPECT_TRUE(storm::utility::isInfinity(result.lowerBound));
959 EXPECT_TRUE(storm::utility::isInfinity(result.upperBound));
960}
961
962TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmax_Clip) {
963 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
964 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
965 }
966 typedef typename TestFixture::ValueType ValueType;
967
968 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmax=?[\"notbad\" U \"goal\"]", "N=4");
969 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
970 auto result = checker.check(this->env(), *data.formula);
971
972 ValueType expected = this->parseNumber("38/155");
973 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
974 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
975 // Use relative difference of bounds for this one
976 EXPECT_LE(result.diff(), this->precision())
977 << "Result [" << result.lowerBound << ", " << result.upperBound
978 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
979}
980
981TYPED_TEST(BeliefExplorationPomdpModelCheckerTest, refuel_Pmin_Clip) {
982 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
983 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
984 }
985 typedef typename TestFixture::ValueType ValueType;
986
987 auto data = this->buildPrism(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism", "Pmin=?[\"notbad\" U \"goal\"]", "N=4");
988 storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<storm::models::sparse::Pomdp<ValueType>> checker(data.model, this->optionsWithClipping());
989 auto result = checker.check(this->env(), *data.formula);
990
991 ValueType expected = this->parseNumber("0");
992 EXPECT_LE(result.lowerBound, expected + this->modelcheckingPrecision());
993 EXPECT_GE(result.upperBound, expected - this->modelcheckingPrecision());
994 // Use relative difference of bounds for this one
995 EXPECT_LE(result.diff(), this->precision())
996 << "Result [" << result.lowerBound << ", " << result.upperBound
997 << "] is not precise enough. If (only) this fails, the result bounds are still correct, but they might be unexpectedly imprecise.\n";
998}
999#endif // defined STORM_HAVE_Z3_OPTIMIZE
1000
1001} // 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::models::sparse::Pomdp
This class represents a partially observable Markov decision process.
Definition Pomdp.h:13
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::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
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::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:53
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:19
storm::utility::isInfinity
bool isInfinity(ValueType const &a)
Definition constants.cpp:107
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