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