Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MdpPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-conv/api/storm-conv.h"
5#include "storm-parsers/api/model_descriptions.h"
6#include "storm-parsers/api/properties.h"
7#include "storm/api/builder.h"
8#include "storm/api/properties.h"
9#include "storm/environment/solver/MinMaxSolverEnvironment.h"
10#include "storm/environment/solver/MultiplierEnvironment.h"
11#include "storm/environment/solver/TopologicalSolverEnvironment.h"
12#include "storm/exceptions/UncheckedRequirementException.h"
13#include "storm/logic/Formulas.h"
14#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
15#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
16#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
17#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
18#include "storm/modelchecker/results/QualitativeCheckResult.h"
19#include "storm/modelchecker/results/QuantitativeCheckResult.h"
20#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
21#include "storm/models/sparse/Mdp.h"
22#include "storm/models/sparse/StandardRewardModel.h"
23#include "storm/models/symbolic/Mdp.h"
24#include "storm/models/symbolic/StandardRewardModel.h"
25#include "storm/settings/modules/CoreSettings.h"
26#include "storm/storage/jani/Property.h"
27
28namespace {
29
30enum class MdpEngine { PrismSparse, JaniSparse, Hybrid, PrismDd, JaniDd };
31
32class SparseDoubleValueIterationViOpGaussSeidelMultEnvironment {
33 public:
34 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
35 static const MdpEngine engine = MdpEngine::PrismSparse;
36 static const bool isExact = false;
37 typedef double ValueType;
38 typedef storm::models::sparse::Mdp<ValueType> ModelType;
39 static storm::Environment createEnvironment() {
40 storm::Environment env;
41 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
42 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
43 env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel);
44 env.solver().multiplier().setType(storm::solver::MultiplierType::ViOperator);
45 return env;
46 }
47};
48
49class SparseDoubleValueIterationViOpRegularMultEnvironment {
50 public:
51 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
52 static const MdpEngine engine = MdpEngine::PrismSparse;
53 static const bool isExact = false;
54 typedef double ValueType;
55 typedef storm::models::sparse::Mdp<ValueType> ModelType;
56 static storm::Environment createEnvironment() {
57 storm::Environment env;
58 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
59 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
60 env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular);
61 env.solver().multiplier().setType(storm::solver::MultiplierType::ViOperator);
62 return env;
63 }
64};
65
66class SparseDoubleValueIterationNativeGaussSeidelMultEnvironment {
67 public:
68 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
69 static const MdpEngine engine = MdpEngine::PrismSparse;
70 static const bool isExact = false;
71 typedef double ValueType;
72 typedef storm::models::sparse::Mdp<ValueType> ModelType;
73 static storm::Environment createEnvironment() {
74 storm::Environment env;
75 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
76 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
77 env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel);
78 env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
79 return env;
80 }
81};
82
83class SparseDoubleValueIterationNativeRegularMultEnvironment {
84 public:
85 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
86 static const MdpEngine engine = MdpEngine::PrismSparse;
87 static const bool isExact = false;
88 typedef double ValueType;
89 typedef storm::models::sparse::Mdp<ValueType> ModelType;
90 static storm::Environment createEnvironment() {
91 storm::Environment env;
92 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
93 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
94 env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular);
95 env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
96 return env;
97 }
98};
99
100class JaniSparseDoubleValueIterationEnvironment {
101 public:
102 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
103 static const MdpEngine engine = MdpEngine::JaniSparse;
104 static const bool isExact = false;
105 typedef double ValueType;
106 typedef storm::models::sparse::Mdp<ValueType> ModelType;
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-10));
111 return env;
112 }
113};
114
115class SparseDoubleIntervalIterationEnvironment {
116 public:
117 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
118 static const MdpEngine engine = MdpEngine::PrismSparse;
119 static const bool isExact = false;
120 typedef double ValueType;
121 typedef storm::models::sparse::Mdp<ValueType> ModelType;
122 static storm::Environment createEnvironment() {
123 storm::Environment env;
124 env.solver().setForceSoundness(true);
125 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration);
126 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
127 env.solver().minMax().setRelativeTerminationCriterion(false);
128 return env;
129 }
130};
131
132class SparseDoubleSoundValueIterationEnvironment {
133 public:
134 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
135 static const MdpEngine engine = MdpEngine::PrismSparse;
136 static const bool isExact = false;
137 typedef double ValueType;
138 typedef storm::models::sparse::Mdp<ValueType> ModelType;
139 static storm::Environment createEnvironment() {
140 storm::Environment env;
141 env.solver().setForceSoundness(true);
142 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
143 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
144 env.solver().minMax().setRelativeTerminationCriterion(false);
145 return env;
146 }
147};
148
149class SparseDoubleOptimisticValueIterationEnvironment {
150 public:
151 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
152 static const MdpEngine engine = MdpEngine::PrismSparse;
153 static const bool isExact = false;
154 typedef double ValueType;
155 typedef storm::models::sparse::Mdp<ValueType> ModelType;
156 static storm::Environment createEnvironment() {
157 storm::Environment env;
158 env.solver().setForceSoundness(true);
159 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration);
160 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
161 env.solver().minMax().setRelativeTerminationCriterion(false);
162 return env;
163 }
164};
165
166class SparseDoubleGuessingValueIterationEnvironment {
167 public:
168 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
169 static const MdpEngine engine = MdpEngine::PrismSparse;
170 static const bool isExact = false;
171 typedef double ValueType;
172 typedef storm::models::sparse::Mdp<ValueType> ModelType;
173 static storm::Environment createEnvironment() {
174 storm::Environment env;
175 env.solver().setForceSoundness(true);
176 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::GuessingValueIteration);
177 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
178 env.solver().minMax().setRelativeTerminationCriterion(false);
179 return env;
180 }
181};
182
183class SparseDoubleTopologicalValueIterationEnvironment {
184 public:
185 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
186 static const MdpEngine engine = MdpEngine::PrismSparse;
187 static const bool isExact = false;
188 typedef double ValueType;
189 typedef storm::models::sparse::Mdp<ValueType> ModelType;
190 static storm::Environment createEnvironment() {
191 storm::Environment env;
192 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
193 env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration);
194 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
195 env.solver().minMax().setRelativeTerminationCriterion(false);
196 return env;
197 }
198};
199
200class SparseDoubleTopologicalSoundValueIterationEnvironment {
201 public:
202 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
203 static const MdpEngine engine = MdpEngine::PrismSparse;
204 static const bool isExact = false;
205 typedef double ValueType;
206 typedef storm::models::sparse::Mdp<ValueType> ModelType;
207 static storm::Environment createEnvironment() {
208 storm::Environment env;
209 env.solver().setForceSoundness(true);
210 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
211 env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::SoundValueIteration);
212 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
213 env.solver().minMax().setRelativeTerminationCriterion(false);
214 return env;
215 }
216};
217
218class SparseDoubleTopologicalGuessingValueIterationEnvironment {
219 public:
220 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
221 static const MdpEngine engine = MdpEngine::PrismSparse;
222 static const bool isExact = false;
223 typedef double ValueType;
224 typedef storm::models::sparse::Mdp<ValueType> ModelType;
225 static storm::Environment createEnvironment() {
226 storm::Environment env;
227 env.solver().setForceSoundness(true);
228 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
229 env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::GuessingValueIteration);
230 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
231 env.solver().minMax().setRelativeTerminationCriterion(false);
232 return env;
233 }
234};
235
236class SparseDoubleLPEnvironment {
237 public:
238 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
239 static const MdpEngine engine = MdpEngine::PrismSparse;
240 static const bool isExact = false;
241 typedef double ValueType;
242 typedef storm::models::sparse::Mdp<ValueType> ModelType;
243 static storm::Environment createEnvironment() {
244 storm::Environment env;
245 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::LinearProgramming);
246 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
247 return env;
248 }
249};
250
251class SparseDoubleViToLPEnvironment {
252 public:
253 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
254 static const MdpEngine engine = MdpEngine::PrismSparse;
255 static const bool isExact = false;
256 typedef double ValueType;
257 typedef storm::models::sparse::Mdp<ValueType> ModelType;
258 static storm::Environment createEnvironment() {
259 storm::Environment env;
260 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ViToLp);
261 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
262 return env;
263 }
264};
265
266class SparseRationalPolicyIterationEnvironment {
267 public:
268 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
269 static const MdpEngine engine = MdpEngine::PrismSparse;
270 static const bool isExact = true;
271 typedef storm::RationalNumber ValueType;
272 typedef storm::models::sparse::Mdp<ValueType> ModelType;
273 static storm::Environment createEnvironment() {
274 storm::Environment env;
275 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
276 return env;
277 }
278};
279
280class SparseRationalViToPiEnvironment {
281 public:
282 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
283 static const MdpEngine engine = MdpEngine::PrismSparse;
284 static const bool isExact = true;
285 typedef storm::RationalNumber ValueType;
286 typedef storm::models::sparse::Mdp<ValueType> ModelType;
287 static storm::Environment createEnvironment() {
288 storm::Environment env;
289 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ViToPi);
290 return env;
291 }
292};
293
294class SparseRationalRationalSearchEnvironment {
295 public:
296 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
297 static const MdpEngine engine = MdpEngine::PrismSparse;
298 static const bool isExact = true;
299 typedef storm::RationalNumber ValueType;
300 typedef storm::models::sparse::Mdp<ValueType> ModelType;
301 static storm::Environment createEnvironment() {
302 storm::Environment env;
303 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
304 return env;
305 }
306};
307class HybridCuddDoubleValueIterationEnvironment {
308 public:
309 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
310 static const MdpEngine engine = MdpEngine::Hybrid;
311 static const bool isExact = false;
312 typedef double ValueType;
313 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
314
315 static void checkLibraryAvailable() {
316#ifndef STORM_HAVE_CUDD
317 GTEST_SKIP() << "Library CUDD not available.";
318#endif
319 }
320
321 static storm::Environment createEnvironment() {
322 storm::Environment env;
323 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
324 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
325 return env;
326 }
327};
328class HybridSylvanDoubleValueIterationEnvironment {
329 public:
330 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
331 static const MdpEngine engine = MdpEngine::Hybrid;
332 static const bool isExact = false;
333 typedef double ValueType;
334 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
335
336 static void checkLibraryAvailable() {
337#ifndef STORM_HAVE_SYLVAN
338 GTEST_SKIP() << "Library Sylvan not available.";
339#endif
340 }
341
342 static storm::Environment createEnvironment() {
343 storm::Environment env;
344 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
345 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
346 return env;
347 }
348};
349class HybridCuddDoubleSoundValueIterationEnvironment {
350 public:
351 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
352 static const MdpEngine engine = MdpEngine::Hybrid;
353 static const bool isExact = false;
354 typedef double ValueType;
355 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
356
357 static void checkLibraryAvailable() {
358#ifndef STORM_HAVE_CUDD
359 GTEST_SKIP() << "Library CUDD not available.";
360#endif
361 }
362
363 static storm::Environment createEnvironment() {
364 storm::Environment env;
365 env.solver().setForceSoundness(true);
366 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
367 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
368 env.solver().minMax().setRelativeTerminationCriterion(false);
369 return env;
370 }
371};
372class HybridCuddDoubleOptimisticValueIterationEnvironment {
373 public:
374 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
375 static const MdpEngine engine = MdpEngine::Hybrid;
376 static const bool isExact = false;
377 typedef double ValueType;
378 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
379
380 static void checkLibraryAvailable() {
381#ifndef STORM_HAVE_CUDD
382 GTEST_SKIP() << "Library CUDD not available.";
383#endif
384 }
385
386 static storm::Environment createEnvironment() {
387 storm::Environment env;
388 env.solver().setForceSoundness(true);
389 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration);
390 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
391 env.solver().minMax().setRelativeTerminationCriterion(false);
392 return env;
393 }
394};
395class HybridCuddDoubleGuessingValueIterationEnvironment {
396 public:
397 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
398 static const MdpEngine engine = MdpEngine::Hybrid;
399 static const bool isExact = false;
400 typedef double ValueType;
401 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
402
403 static void checkLibraryAvailable() {
404#ifndef STORM_HAVE_CUDD
405 GTEST_SKIP() << "Library CUDD not available.";
406#endif
407 }
408
409 static storm::Environment createEnvironment() {
410 storm::Environment env;
411 env.solver().setForceSoundness(true);
412 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::GuessingValueIteration);
413 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
414 env.solver().minMax().setRelativeTerminationCriterion(false);
415 return env;
416 }
417};
418class HybridSylvanRationalPolicyIterationEnvironment {
419 public:
420 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
421 static const MdpEngine engine = MdpEngine::Hybrid;
422 static const bool isExact = true;
423 typedef storm::RationalNumber ValueType;
424 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
425
426 static void checkLibraryAvailable() {
427#ifndef STORM_HAVE_SYLVAN
428 GTEST_SKIP() << "Library Sylvan not available.";
429#endif
430 }
431
432 static storm::Environment createEnvironment() {
433 storm::Environment env;
434 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
435 return env;
436 }
437};
438class DdCuddDoubleValueIterationEnvironment {
439 public:
440 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
441 static const MdpEngine engine = MdpEngine::PrismDd;
442 static const bool isExact = false;
443 typedef double ValueType;
444 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
445
446 static void checkLibraryAvailable() {
447#ifndef STORM_HAVE_CUDD
448 GTEST_SKIP() << "Library CUDD not available.";
449#endif
450 }
451
452 static storm::Environment createEnvironment() {
453 storm::Environment env;
454 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
455 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
456 return env;
457 }
458};
459class JaniDdCuddDoubleValueIterationEnvironment {
460 public:
461 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
462 static const MdpEngine engine = MdpEngine::JaniDd;
463 static const bool isExact = false;
464 typedef double ValueType;
465 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
466
467 static void checkLibraryAvailable() {
468#ifndef STORM_HAVE_CUDD
469 GTEST_SKIP() << "Library CUDD not available.";
470#endif
471 }
472
473 static storm::Environment createEnvironment() {
474 storm::Environment env;
475 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
476 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
477 return env;
478 }
479};
480class DdSylvanDoubleValueIterationEnvironment {
481 public:
482 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
483 static const MdpEngine engine = MdpEngine::PrismDd;
484 static const bool isExact = false;
485 typedef double ValueType;
486 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
487
488 static void checkLibraryAvailable() {
489#ifndef STORM_HAVE_SYLVAN
490 GTEST_SKIP() << "Library Sylvan not available.";
491#endif
492 }
493
494 static storm::Environment createEnvironment() {
495 storm::Environment env;
496 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
497 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
498 return env;
499 }
500};
501class DdCuddDoublePolicyIterationEnvironment {
502 public:
503 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
504 static const MdpEngine engine = MdpEngine::PrismDd;
505 static const bool isExact = false;
506 typedef double ValueType;
507 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
508
509 static void checkLibraryAvailable() {
510#ifndef STORM_HAVE_CUDD
511 GTEST_SKIP() << "Library CUDD not available.";
512#endif
513 }
514
515 static storm::Environment createEnvironment() {
516 storm::Environment env;
517 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
518 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
519 return env;
520 }
521};
522class DdSylvanRationalRationalSearchEnvironment {
523 public:
524 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
525 static const MdpEngine engine = MdpEngine::PrismDd;
526 static const bool isExact = true;
527 typedef storm::RationalNumber ValueType;
528 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
529
530 static void checkLibraryAvailable() {
531#ifndef STORM_HAVE_SYLVAN
532 GTEST_SKIP() << "Library Sylvan not available.";
533#endif
534 }
535
536 static storm::Environment createEnvironment() {
537 storm::Environment env;
538 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
539 return env;
540 }
541};
542
543template<typename TestType>
544class MdpPrctlModelCheckerTest : public ::testing::Test {
545 public:
546 typedef typename TestType::ValueType ValueType;
547 typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
548 typedef typename storm::models::symbolic::Mdp<TestType::ddType, ValueType> SymbolicModelType;
549
550 MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
551
552 void SetUp() override {
553#ifndef STORM_HAVE_Z3
554 GTEST_SKIP() << "Z3 not available.";
555#endif
556 if constexpr (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) {
557 TestType::checkLibraryAvailable();
558 }
559 }
560
561 storm::Environment const& env() const {
562 return _environment;
563 }
564 ValueType parseNumber(std::string const& input) const {
565 return storm::utility::convertNumber<ValueType>(input);
566 }
567 ValueType precision() const {
568 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
569 }
570 bool isSparseModel() const {
571 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
572 }
573 bool isSymbolicModel() const {
574 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
575 }
576
577 template<typename MT = typename TestType::ModelType>
578 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
579 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
580 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
581 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
582 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
583 program = storm::utility::prism::preprocess(program, constantDefinitionString);
584 if (TestType::engine == MdpEngine::PrismSparse) {
585 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
586 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
587 } else if (TestType::engine == MdpEngine::JaniSparse) {
588 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
589 janiData.first.substituteFunctions();
590 result.second = storm::api::extractFormulasFromProperties(janiData.second);
591 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
592 }
593 return result;
594 }
595
596 template<typename MT = typename TestType::ModelType>
597 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
598 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
599 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
600 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
601 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
602 program = storm::utility::prism::preprocess(program, constantDefinitionString);
603 if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) {
604 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
605 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
606 } else if (TestType::engine == MdpEngine::JaniDd) {
607 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
608 janiData.first.substituteFunctions();
609 result.second = storm::api::extractFormulasFromProperties(janiData.second);
610 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
611 }
612 return result;
613 }
614
615 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
616 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
617 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
618 for (auto const& f : formulas) {
619 result.emplace_back(*f);
620 }
621 return result;
622 }
623
624 template<typename MT = typename TestType::ModelType>
625 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
626 std::shared_ptr<MT> const& model) const {
627 if (TestType::engine == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse) {
628 return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model);
629 }
630 }
631
632 template<typename MT = typename TestType::ModelType>
633 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
634 createModelChecker(std::shared_ptr<MT> const& model) const {
635 if (TestType::engine == MdpEngine::Hybrid) {
636 return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*model);
637 } else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) {
638 return std::make_shared<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*model);
639 }
640 }
641
642 template<typename MT = typename TestType::ModelType>
643 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
644 std::function<void()> const& f) const {
645 f();
646 }
647
648 template<typename MT = typename TestType::ModelType>
649 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
650 std::function<void()> const& f) const {
651 model->getManager().execute(f);
652 }
653
654 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
655 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
656 auto filter = getInitialStateFilter(model);
657 result->filter(*filter);
658 return result->asQualitativeCheckResult().forallTrue();
659 }
660
661 ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
662 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
663 auto filter = getInitialStateFilter(model);
664 result->filter(*filter);
665 return result->asQuantitativeCheckResult<ValueType>().getMin();
666 }
667
668 private:
669 storm::Environment _environment;
670
671 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
672 if (isSparseModel()) {
673 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
674 } else {
675 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
676 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
677 }
678 }
679};
680
681typedef ::testing::Types<SparseDoubleValueIterationViOpGaussSeidelMultEnvironment, SparseDoubleValueIterationViOpRegularMultEnvironment,
682 SparseDoubleValueIterationNativeGaussSeidelMultEnvironment, SparseDoubleValueIterationNativeRegularMultEnvironment,
683 JaniSparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseDoubleSoundValueIterationEnvironment,
684 SparseDoubleOptimisticValueIterationEnvironment, SparseDoubleGuessingValueIterationEnvironment,
685 SparseDoubleTopologicalValueIterationEnvironment, SparseDoubleTopologicalSoundValueIterationEnvironment,
686 SparseDoubleTopologicalGuessingValueIterationEnvironment, SparseDoubleLPEnvironment, SparseDoubleViToLPEnvironment,
687 SparseRationalPolicyIterationEnvironment, SparseRationalViToPiEnvironment, SparseRationalRationalSearchEnvironment,
688 HybridCuddDoubleValueIterationEnvironment, HybridSylvanDoubleValueIterationEnvironment, HybridCuddDoubleSoundValueIterationEnvironment,
689 HybridCuddDoubleOptimisticValueIterationEnvironment, HybridCuddDoubleGuessingValueIterationEnvironment,
690 HybridSylvanRationalPolicyIterationEnvironment, DdCuddDoubleValueIterationEnvironment, JaniDdCuddDoubleValueIterationEnvironment,
691 DdSylvanDoubleValueIterationEnvironment, DdCuddDoublePolicyIterationEnvironment, DdSylvanRationalRationalSearchEnvironment>
692 TestingTypes;
693
694TYPED_TEST_SUITE(MdpPrctlModelCheckerTest, TestingTypes, );
695
696TYPED_TEST(MdpPrctlModelCheckerTest, Dice) {
697 std::string formulasString = "Pmin=? [F \"two\"]";
698 formulasString += "; Pmax=? [F \"two\"]";
699 formulasString += "; Pmin=? [F \"three\"]";
700 formulasString += "; Pmax=? [F \"three\"]";
701 formulasString += "; Pmin=? [F \"four\"]";
702 formulasString += "; Pmax=? [F \"four\"]";
703 formulasString += "; Rmin=? [F \"done\"]";
704 formulasString += "; Rmax=? [F \"done\"]";
705
706 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
707 auto model = std::move(modelFormulas.first);
708 auto tasks = this->getTasks(modelFormulas.second);
709 this->execute(model, [&]() {
710 EXPECT_EQ(169ul, model->getNumberOfStates());
711 EXPECT_EQ(436ul, model->getNumberOfTransitions());
712 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
713
714 auto checker = this->createModelChecker(model);
715 std::unique_ptr<storm::modelchecker::CheckResult> result;
716
717 result = checker->check(this->env(), tasks[0]);
718 EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
719
720 result = checker->check(this->env(), tasks[1]);
721 EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
722
723 result = checker->check(this->env(), tasks[2]);
724 EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
725
726 result = checker->check(this->env(), tasks[3]);
727 EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
728
729 result = checker->check(this->env(), tasks[4]);
730 EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
731
732 result = checker->check(this->env(), tasks[5]);
733 EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
734
735 result = checker->check(this->env(), tasks[6]);
736 EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
737
738 result = checker->check(this->env(), tasks[7]);
739 EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
740 });
741}
742
743TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) {
744 std::string formulasString = "Pmin=? [F \"elected\"]";
745 formulasString += "; Pmax=? [F \"elected\"]";
746 formulasString += "; Pmin=? [F<=25 \"elected\"]";
747 formulasString += "; Pmax=? [F<=25 \"elected\"]";
748 formulasString += "; Rmin=? [F \"elected\"]";
749 formulasString += "; Rmax=? [F \"elected\"]";
750
751 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString);
752 auto model = std::move(modelFormulas.first);
753 auto tasks = this->getTasks(modelFormulas.second);
754 this->execute(model, [&]() {
755 EXPECT_EQ(3172ul, model->getNumberOfStates());
756 EXPECT_EQ(7144ul, model->getNumberOfTransitions());
757 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
758 auto checker = this->createModelChecker(model);
759 std::unique_ptr<storm::modelchecker::CheckResult> result;
760
761 result = checker->check(this->env(), tasks[0]);
762 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
763
764 result = checker->check(this->env(), tasks[1]);
765 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
766
767 result = checker->check(this->env(), tasks[2]);
768 EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
769
770 result = checker->check(this->env(), tasks[3]);
771 EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
772
773 result = checker->check(this->env(), tasks[4]);
774 EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
775
776 result = checker->check(this->env(), tasks[5]);
777 EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
778 });
779}
780
781TYPED_TEST(MdpPrctlModelCheckerTest, consensus) {
782 std::string formulasString = "Pmax=? [F \"finished\"]";
783 formulasString += "; Pmax=? [F \"all_coins_equal_1\"]";
784 formulasString += "; P<0.8 [F \"all_coins_equal_1\"]";
785 formulasString += "; P<0.9 [F \"all_coins_equal_1\"]";
786 formulasString += "; Rmax=? [F \"all_coins_equal_1\"]";
787 formulasString += "; Rmin=? [F \"all_coins_equal_1\"]";
788 formulasString += "; Rmax=? [F \"finished\"]";
789 formulasString += "; Rmin=? [F \"finished\"]";
790
791 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
792 auto model = std::move(modelFormulas.first);
793 auto tasks = this->getTasks(modelFormulas.second);
794 this->execute(model, [&]() {
795 EXPECT_EQ(272ul, model->getNumberOfStates());
796 EXPECT_EQ(492ul, model->getNumberOfTransitions());
797 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
798 auto checker = this->createModelChecker(model);
799 std::unique_ptr<storm::modelchecker::CheckResult> result;
800
801 result = checker->check(this->env(), tasks[0]);
802 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
803
804 result = checker->check(this->env(), tasks[1]);
805 EXPECT_NEAR(this->parseNumber("57/64"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
806
807 result = checker->check(this->env(), tasks[2]);
808 EXPECT_FALSE(this->getQualitativeResultAtInitialState(model, result));
809
810 result = checker->check(this->env(), tasks[3]);
811 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
812
813 result = checker->check(this->env(), tasks[4]);
814 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
815
816 result = checker->check(this->env(), tasks[5]);
817 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
818
819 result = checker->check(this->env(), tasks[6]);
820 EXPECT_NEAR(this->parseNumber("75"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
821
822 result = checker->check(this->env(), tasks[7]);
823 EXPECT_NEAR(this->parseNumber("48"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
824 });
825}
826
827TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) {
828 std::string formulasString = "Rmin=? [F \"target\"]";
829 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString);
830 auto model = std::move(modelFormulas.first);
831 auto tasks = this->getTasks(modelFormulas.second);
832 this->execute(model, [&]() {
833 EXPECT_EQ(3ul, model->getNumberOfStates());
834 EXPECT_EQ(4ul, model->getNumberOfTransitions());
835 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
836 auto checker = this->createModelChecker(model);
837 std::unique_ptr<storm::modelchecker::CheckResult> result;
838
839 // This example considers a zero-reward end component that does not reach the target
840 // For some methods this requires end-component elimination which is (currently) not supported in the Dd engine
841
842 if (TypeParam::engine == MdpEngine::PrismDd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) {
843 STORM_SILENT_EXPECT_THROW(checker->check(this->env(), tasks[0]), storm::exceptions::UncheckedRequirementException);
844 } else {
845 result = checker->check(this->env(), tasks[0]);
846 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
847 }
848 });
849}
850
851TYPED_TEST(MdpPrctlModelCheckerTest, Team) {
852 std::string formulasString = "R{\"w_1_total\"}max=? [ C ]";
853 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm", formulasString);
854 auto model = std::move(modelFormulas.first);
855 auto tasks = this->getTasks(modelFormulas.second);
856 this->execute(model, [&]() {
857 EXPECT_EQ(12475ul, model->getNumberOfStates());
858 EXPECT_EQ(15228ul, model->getNumberOfTransitions());
859 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
860 auto checker = this->createModelChecker(model);
861 std::unique_ptr<storm::modelchecker::CheckResult> result;
862
863 // This example considers an expected total reward formula, which is not supported in all engines
864
865 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
866 result = checker->check(this->env(), tasks[0]);
867 EXPECT_NEAR(this->parseNumber("114/49"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
868 } else {
869 EXPECT_FALSE(checker->canHandle(tasks[0]));
870 }
871 });
872}
873
874TYPED_TEST(MdpPrctlModelCheckerTest, LtlProbabilitiesCoin) {
875#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
876 std::string formulasString = "Pmin=? [!(GF \"all_coins_equal_1\")]";
877 formulasString += "; Pmax=? [F \"all_coins_equal_1\" U \"finished\"]";
878 formulasString += "; P>0.4 [!(GF \"all_coins_equal_1\")]";
879 formulasString += "; P<0.6 [F \"all_coins_equal_1\" U \"finished\"]";
880 // The following example results in an automaton with acceptance condition not in DNF (Streett, using Spot)
881 formulasString += "; Pmax=?[ (GF \"all_coins_equal_1\") & ((GF \"all_coins_equal_0\") | (FG \"finished\"))]";
882
883 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
884 auto model = std::move(modelFormulas.first);
885 auto tasks = this->getTasks(modelFormulas.second);
886 this->execute(model, [&]() {
887 EXPECT_EQ(272ul, model->getNumberOfStates());
888 EXPECT_EQ(492ul, model->getNumberOfTransitions());
889 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
890 auto checker = this->createModelChecker(model);
891 std::unique_ptr<storm::modelchecker::CheckResult> result;
892
893 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
894 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
895 result = checker->check(this->env(), tasks[0]);
896 EXPECT_NEAR(this->parseNumber("4/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
897
898 result = checker->check(this->env(), tasks[1]);
899 EXPECT_NEAR(this->parseNumber("5/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
900
901 result = checker->check(this->env(), tasks[2]);
902 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
903
904 result = checker->check(this->env(), tasks[3]);
905 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
906
907 result = checker->check(this->env(), tasks[4]);
908 EXPECT_NEAR(this->parseNumber("5/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
909
910 } else {
911 EXPECT_FALSE(checker->canHandle(tasks[0]));
912 }
913 });
914#else
915 GTEST_SKIP();
916#endif
917}
918
919TYPED_TEST(MdpPrctlModelCheckerTest, LtlDice) {
920#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
921 std::string formulasString = "Pmax=? [ X (((s1=1) U (s1=3)) U (s1=7))]";
922 formulasString += "; Pmax=? [ (F (X (s1=6 & (XX s1=5)))) & (F G (d1!=5))]";
923 formulasString += "; Pmax=? [ F s1=3 U (\"three\")]";
924 formulasString += "; Pmin=? [! F (s2=6) & X \"done\"]";
925 // Acceptance condition not in DNF (Streett, using Spot)
926 formulasString += "; Pmax=? [ ( (G F !(\"two\")) | F G (\"three\") ) & ( (G F !(\"five\") ) | F G (\"seven\") )]";
927
928 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
929 auto model = std::move(modelFormulas.first);
930 auto tasks = this->getTasks(modelFormulas.second);
931 this->execute(model, [&]() {
932 EXPECT_EQ(169ul, model->getNumberOfStates());
933 EXPECT_EQ(436ul, model->getNumberOfTransitions());
934 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
935 auto checker = this->createModelChecker(model);
936 std::unique_ptr<storm::modelchecker::CheckResult> result;
937
938 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
939 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
940 result = checker->check(this->env(), tasks[0]);
941 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
942
943 result = checker->check(this->env(), tasks[1]);
944 EXPECT_NEAR(this->parseNumber("1/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
945
946 result = checker->check(this->env(), tasks[2]);
947 EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
948
949 result = checker->check(this->env(), tasks[3]);
950 EXPECT_NEAR(this->parseNumber("5/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
951
952 result = checker->check(this->env(), tasks[4]);
953 EXPECT_NEAR(this->parseNumber("31/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
954
955 } else {
956 EXPECT_FALSE(checker->canHandle(tasks[0]));
957 }
958 });
959#else
960 GTEST_SKIP();
961#endif
962}
963
964TYPED_TEST(MdpPrctlModelCheckerTest, LtlCoinFlips) {
965#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
966 std::string formulasString = "Pmax=? [ G (true U (heads | \"done\")) ]";
967 formulasString += "; Pmin=? [ G (true U (heads | \"done\")) ]";
968 formulasString += "; Pmax=? [ G (true U<=10 (heads | \"done\")) ]";
969 formulasString += "; Pmin=? [ G (true U<=10 (heads | \"done\")) ]";
970 formulasString += "; Pmax=? [ X G (true U<=0 (heads | \"done\")) ]";
971 formulasString += "; Pmax=? [ true U[10,12] heads ]";
972 formulasString += "; Pmax=? [ X (true U[0,0] heads) ]";
973 formulasString += "; Pmax=? [ G (!(P>=1 [\"done\"]) U<=10 (heads | P>=1 [ \"done\"])) ]";
974 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin_flips.nm", formulasString);
975 auto model = std::move(modelFormulas.first);
976 auto tasks = this->getTasks(modelFormulas.second);
977 this->execute(model, [&]() {
978 EXPECT_EQ(61ul, model->getNumberOfStates());
979 EXPECT_EQ(177ul, model->getNumberOfTransitions());
980 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
981 auto checker = this->createModelChecker(model);
982 std::unique_ptr<storm::modelchecker::CheckResult> result;
983
984 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
985 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
986 result = checker->check(this->env(), tasks[0]);
987 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
988
989 result = checker->check(this->env(), tasks[1]);
990 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
991
992 result = checker->check(this->env(), tasks[2]);
993 EXPECT_NEAR(this->parseNumber("1021/1024"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
994
995 result = checker->check(this->env(), tasks[3]);
996 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
997
998 result = checker->check(this->env(), tasks[4]);
999 EXPECT_NEAR(this->parseNumber("1/524288"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1000
1001 result = checker->check(this->env(), tasks[5]);
1002 EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1003
1004 result = checker->check(this->env(), tasks[6]);
1005 EXPECT_NEAR(this->parseNumber("1/2"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1006
1007 result = checker->check(this->env(), tasks[7]);
1008 EXPECT_NEAR(this->parseNumber("1021/1024"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1009
1010 } else {
1011 EXPECT_FALSE(checker->canHandle(tasks[0]));
1012 }
1013 });
1014#else
1015 GTEST_SKIP();
1016#endif
1017}
1018
1019TYPED_TEST(MdpPrctlModelCheckerTest, HOADice) {
1020 // "P=? [ F "three" & (X s=1)]"
1021 std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"three\", \"p1\" -> s2=1 }]";
1022 // "P=? [!(s2=6) U "done"]"
1023 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s2=6), \"p1\" -> \"done\" }]";
1024
1025 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
1026 auto model = std::move(modelFormulas.first);
1027 auto tasks = this->getTasks(modelFormulas.second);
1028 this->execute(model, [&]() {
1029 EXPECT_EQ(169ul, model->getNumberOfStates());
1030 EXPECT_EQ(436ul, model->getNumberOfTransitions());
1031 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
1032 auto checker = this->createModelChecker(model);
1033 std::unique_ptr<storm::modelchecker::CheckResult> result;
1034
1035 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
1036 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
1037 result = checker->check(tasks[0]);
1038 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1039
1040 result = checker->check(tasks[1]);
1041 EXPECT_NEAR(this->parseNumber("3/4"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1042 } else {
1043 EXPECT_FALSE(checker->canHandle(tasks[0]));
1044 }
1045 });
1046}
1047
1048TYPED_TEST(MdpPrctlModelCheckerTest, SmallDiscount) {
1049 if (TypeParam::isExact || std::is_same<TypeParam, SparseDoubleLPEnvironment>::value || std::is_same<TypeParam, SparseDoubleViToLPEnvironment>::value) {
1050 GTEST_SKIP() << "Exact computations for discounted properties are not supported.";
1051 }
1052 std::string formulasString = "Rmax=? [ C ]";
1053 formulasString += "; Rmax=? [ Cdiscount=9/10 ]";
1054 formulasString += "; Rmax=? [ Cdiscount=15/16 ]";
1055 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/small_discount.nm", formulasString);
1056 auto model = std::move(modelFormulas.first);
1057 auto tasks = this->getTasks(modelFormulas.second);
1058 EXPECT_EQ(4ul, model->getNumberOfStates());
1059 EXPECT_EQ(6ul, model->getNumberOfTransitions());
1060 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
1061 auto checker = this->createModelChecker(model);
1062
1063 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
1064 std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(this->env(), tasks[0]);
1065 EXPECT_NEAR(this->parseNumber("5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1066 result = checker->check(this->env(), tasks[1]);
1067 EXPECT_NEAR(this->parseNumber("18/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1068 result = checker->check(this->env(), tasks[2]);
1069 EXPECT_NEAR(this->parseNumber("15/4"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1070 } else {
1071 EXPECT_FALSE(checker->canHandle(tasks[0]));
1072 EXPECT_FALSE(checker->canHandle(tasks[1]));
1073 EXPECT_FALSE(checker->canHandle(tasks[2]));
1074 }
1075}
1076
1077TYPED_TEST(MdpPrctlModelCheckerTest, OneStateDiscounting) {
1078 if (TypeParam::isExact || std::is_same<TypeParam, SparseDoubleLPEnvironment>::value || std::is_same<TypeParam, SparseDoubleViToLPEnvironment>::value) {
1079 GTEST_SKIP() << "Exact computations for discounted properties are not supported.";
1080 }
1081 std::string formulasString = "Rmax=? [ Cdiscount=9/10 ]";
1082 formulasString += "; Rmax=? [ C<=5discount=9/10 ]";
1083 formulasString += "; Rmax=? [ C<=10discount=9/10 ]";
1084 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/one_state.nm", formulasString);
1085 auto model = std::move(modelFormulas.first);
1086 auto tasks = this->getTasks(modelFormulas.second);
1087 EXPECT_EQ(1ul, model->getNumberOfStates());
1088 EXPECT_EQ(2ul, model->getNumberOfTransitions());
1089 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
1090 auto checker = this->createModelChecker(model);
1091
1092 if ((TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse)) {
1093 std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(this->env(), tasks[0]);
1094 EXPECT_NEAR(this->parseNumber("1000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1095 result = checker->check(this->env(), tasks[1]);
1096 EXPECT_NEAR(this->parseNumber("40951/100"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1097 result = checker->check(this->env(), tasks[2]);
1098 EXPECT_NEAR(this->parseNumber("6513215599/10000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
1099 } else {
1100 EXPECT_FALSE(checker->canHandle(tasks[0]));
1101 EXPECT_FALSE(checker->canHandle(tasks[1]));
1102 EXPECT_FALSE(checker->canHandle(tasks[2]));
1103 }
1104}
1105} // namespace
getInitialStateFilter
std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model)
Definition RobustMdpPrctlModelCheckerTest.cpp:18
getQuantitativeResultAtInitialState
double getQuantitativeResultAtInitialState(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
Definition RobustMdpPrctlModelCheckerTest.cpp:27
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::MinMaxSolverEnvironment::setMultiplicationStyle
void setMultiplicationStyle(storm::solver::MultiplicationStyle value)
Definition MinMaxSolverEnvironment.cpp:76
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::MultiplierEnvironment::setType
void setType(storm::solver::MultiplierType value, bool isSetFromDefault=false)
Definition MultiplierEnvironment.cpp:28
storm::SolverEnvironment::topological
TopologicalSolverEnvironment & topological()
Definition SolverEnvironment.cpp:91
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:43
storm::SolverEnvironment::multiplier
MultiplierEnvironment & multiplier()
Definition SolverEnvironment.cpp:51
storm::TopologicalSolverEnvironment::setUnderlyingMinMaxMethod
void setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod value)
Definition TopologicalSolverEnvironment.cpp:48
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::models::symbolic::Mdp
This class represents a discrete-time Markov decision process.
Definition Mdp.h:13
model_descriptions.h
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::api::convertPrismToJani
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > convertPrismToJani(storm::prism::Program const &program, storm::converter::PrismToJaniConverterOptions options)
Definition storm-conv.cpp:111
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::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::vector::filter
storm::storage::BitVector filter(std::vector< T > const &values, std::function< bool(T const &value)> const &function)
Retrieves a bit vector containing all the indices for which the value at this position makes the give...
Definition vector.h:490
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
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:31