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