Storm 1.10.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
10#include "storm/environment/solver/MinMaxSolverEnvironment.h"
11#include "storm/environment/solver/MultiplierEnvironment.h"
12#include "storm/environment/solver/TopologicalSolverEnvironment.h"
13#include "storm/exceptions/UncheckedRequirementException.h"
14#include "storm/logic/Formulas.h"
15#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
16#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
17#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
18#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.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 static storm::Environment createEnvironment() {
316 storm::Environment env;
317 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
318 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
319 return env;
320 }
321};
322class HybridSylvanDoubleValueIterationEnvironment {
323 public:
324 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
325 static const MdpEngine engine = MdpEngine::Hybrid;
326 static const bool isExact = false;
327 typedef double ValueType;
328 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
329 static storm::Environment createEnvironment() {
330 storm::Environment env;
331 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
332 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
333 return env;
334 }
335};
336class HybridCuddDoubleSoundValueIterationEnvironment {
337 public:
338 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
339 static const MdpEngine engine = MdpEngine::Hybrid;
340 static const bool isExact = false;
341 typedef double ValueType;
342 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
343 static storm::Environment createEnvironment() {
344 storm::Environment env;
345 env.solver().setForceSoundness(true);
346 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
347 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
348 env.solver().minMax().setRelativeTerminationCriterion(false);
349 return env;
350 }
351};
352class HybridCuddDoubleOptimisticValueIterationEnvironment {
353 public:
354 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
355 static const MdpEngine engine = MdpEngine::Hybrid;
356 static const bool isExact = false;
357 typedef double ValueType;
358 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
359 static storm::Environment createEnvironment() {
360 storm::Environment env;
361 env.solver().setForceSoundness(true);
362 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration);
363 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
364 env.solver().minMax().setRelativeTerminationCriterion(false);
365 return env;
366 }
367};
368class HybridCuddDoubleGuessingValueIterationEnvironment {
369 public:
370 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
371 static const MdpEngine engine = MdpEngine::Hybrid;
372 static const bool isExact = false;
373 typedef double ValueType;
374 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
375 static storm::Environment createEnvironment() {
376 storm::Environment env;
377 env.solver().setForceSoundness(true);
378 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::GuessingValueIteration);
379 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
380 env.solver().minMax().setRelativeTerminationCriterion(false);
381 return env;
382 }
383};
384class HybridSylvanRationalPolicyIterationEnvironment {
385 public:
386 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
387 static const MdpEngine engine = MdpEngine::Hybrid;
388 static const bool isExact = true;
389 typedef storm::RationalNumber ValueType;
390 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
391 static storm::Environment createEnvironment() {
392 storm::Environment env;
393 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
394 return env;
395 }
396};
397class DdCuddDoubleValueIterationEnvironment {
398 public:
399 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
400 static const MdpEngine engine = MdpEngine::PrismDd;
401 static const bool isExact = false;
402 typedef double ValueType;
403 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
404 static storm::Environment createEnvironment() {
405 storm::Environment env;
406 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
407 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
408 return env;
409 }
410};
411class JaniDdCuddDoubleValueIterationEnvironment {
412 public:
413 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
414 static const MdpEngine engine = MdpEngine::JaniDd;
415 static const bool isExact = false;
416 typedef double ValueType;
417 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
418 static storm::Environment createEnvironment() {
419 storm::Environment env;
420 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
421 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
422 return env;
423 }
424};
425class DdSylvanDoubleValueIterationEnvironment {
426 public:
427 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
428 static const MdpEngine engine = MdpEngine::PrismDd;
429 static const bool isExact = false;
430 typedef double ValueType;
431 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
432 static storm::Environment createEnvironment() {
433 storm::Environment env;
434 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
435 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
436 return env;
437 }
438};
439class DdCuddDoublePolicyIterationEnvironment {
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 static storm::Environment createEnvironment() {
447 storm::Environment env;
448 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
449 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
450 return env;
451 }
452};
453class DdSylvanRationalRationalSearchEnvironment {
454 public:
455 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
456 static const MdpEngine engine = MdpEngine::PrismDd;
457 static const bool isExact = true;
458 typedef storm::RationalNumber ValueType;
459 typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
460 static storm::Environment createEnvironment() {
461 storm::Environment env;
462 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
463 return env;
464 }
465};
466
467template<typename TestType>
468class MdpPrctlModelCheckerTest : public ::testing::Test {
469 public:
470 typedef typename TestType::ValueType ValueType;
471 typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
472 typedef typename storm::models::symbolic::Mdp<TestType::ddType, ValueType> SymbolicModelType;
473
474 MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
475
476 void SetUp() override {
477#ifndef STORM_HAVE_Z3
478 GTEST_SKIP() << "Z3 not available.";
479#endif
480 }
481
482 storm::Environment const& env() const {
483 return _environment;
484 }
485 ValueType parseNumber(std::string const& input) const {
486 return storm::utility::convertNumber<ValueType>(input);
487 }
488 ValueType precision() const {
489 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
490 }
491 bool isSparseModel() const {
492 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
493 }
494 bool isSymbolicModel() const {
495 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
496 }
497
498 template<typename MT = typename TestType::ModelType>
499 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
500 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
501 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
502 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
503 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
504 program = storm::utility::prism::preprocess(program, constantDefinitionString);
505 if (TestType::engine == MdpEngine::PrismSparse) {
506 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
507 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
508 } else if (TestType::engine == MdpEngine::JaniSparse) {
509 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
510 janiData.first.substituteFunctions();
511 result.second = storm::api::extractFormulasFromProperties(janiData.second);
512 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
513 }
514 return result;
515 }
516
517 template<typename MT = typename TestType::ModelType>
518 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
519 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
520 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
521 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
522 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
523 program = storm::utility::prism::preprocess(program, constantDefinitionString);
524 if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) {
525 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
526 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
527 } else if (TestType::engine == MdpEngine::JaniDd) {
528 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
529 janiData.first.substituteFunctions();
530 result.second = storm::api::extractFormulasFromProperties(janiData.second);
531 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
532 }
533 return result;
534 }
535
536 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
537 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
538 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
539 for (auto const& f : formulas) {
540 result.emplace_back(*f);
541 }
542 return result;
543 }
544
545 template<typename MT = typename TestType::ModelType>
546 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
547 std::shared_ptr<MT> const& model) const {
548 if (TestType::engine == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse) {
549 return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model);
550 }
551 }
552
553 template<typename MT = typename TestType::ModelType>
554 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
555 createModelChecker(std::shared_ptr<MT> const& model) const {
556 if (TestType::engine == MdpEngine::Hybrid) {
557 return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*model);
558 } else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) {
559 return std::make_shared<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*model);
560 }
561 }
562
563 template<typename MT = typename TestType::ModelType>
564 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
565 std::function<void()> const& f) const {
566 f();
567 }
568
569 template<typename MT = typename TestType::ModelType>
570 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
571 std::function<void()> const& f) const {
572 model->getManager().execute(f);
573 }
574
575 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
576 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
577 auto filter = getInitialStateFilter(model);
578 result->filter(*filter);
579 return result->asQualitativeCheckResult().forallTrue();
580 }
581
582 ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
583 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
584 auto filter = getInitialStateFilter(model);
585 result->filter(*filter);
586 return result->asQuantitativeCheckResult<ValueType>().getMin();
587 }
588
589 private:
590 storm::Environment _environment;
591
592 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
593 if (isSparseModel()) {
594 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
595 } else {
596 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
597 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
598 }
599 }
600};
601
602typedef ::testing::Types<SparseDoubleValueIterationViOpGaussSeidelMultEnvironment, SparseDoubleValueIterationViOpRegularMultEnvironment,
603 SparseDoubleValueIterationNativeGaussSeidelMultEnvironment, SparseDoubleValueIterationNativeRegularMultEnvironment,
604 JaniSparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseDoubleSoundValueIterationEnvironment,
605 SparseDoubleOptimisticValueIterationEnvironment, SparseDoubleGuessingValueIterationEnvironment,
606 SparseDoubleTopologicalValueIterationEnvironment, SparseDoubleTopologicalSoundValueIterationEnvironment,
607 SparseDoubleTopologicalGuessingValueIterationEnvironment, SparseDoubleLPEnvironment, SparseDoubleViToLPEnvironment,
608 SparseRationalPolicyIterationEnvironment, SparseRationalViToPiEnvironment, SparseRationalRationalSearchEnvironment,
609 HybridCuddDoubleValueIterationEnvironment, HybridSylvanDoubleValueIterationEnvironment, HybridCuddDoubleSoundValueIterationEnvironment,
610 HybridCuddDoubleOptimisticValueIterationEnvironment, HybridCuddDoubleGuessingValueIterationEnvironment,
611 HybridSylvanRationalPolicyIterationEnvironment, DdCuddDoubleValueIterationEnvironment, JaniDdCuddDoubleValueIterationEnvironment,
612 DdSylvanDoubleValueIterationEnvironment, DdCuddDoublePolicyIterationEnvironment, DdSylvanRationalRationalSearchEnvironment>
613 TestingTypes;
614
615TYPED_TEST_SUITE(MdpPrctlModelCheckerTest, TestingTypes, );
616
617TYPED_TEST(MdpPrctlModelCheckerTest, Dice) {
618 std::string formulasString = "Pmin=? [F \"two\"]";
619 formulasString += "; Pmax=? [F \"two\"]";
620 formulasString += "; Pmin=? [F \"three\"]";
621 formulasString += "; Pmax=? [F \"three\"]";
622 formulasString += "; Pmin=? [F \"four\"]";
623 formulasString += "; Pmax=? [F \"four\"]";
624 formulasString += "; Rmin=? [F \"done\"]";
625 formulasString += "; Rmax=? [F \"done\"]";
626
627 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
628 auto model = std::move(modelFormulas.first);
629 auto tasks = this->getTasks(modelFormulas.second);
630 this->execute(model, [&]() {
631 EXPECT_EQ(169ul, model->getNumberOfStates());
632 EXPECT_EQ(436ul, model->getNumberOfTransitions());
633 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
634
635 auto checker = this->createModelChecker(model);
636 std::unique_ptr<storm::modelchecker::CheckResult> result;
637
638 result = checker->check(this->env(), tasks[0]);
639 EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
640
641 result = checker->check(this->env(), tasks[1]);
642 EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
643
644 result = checker->check(this->env(), tasks[2]);
645 EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
646
647 result = checker->check(this->env(), tasks[3]);
648 EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
649
650 result = checker->check(this->env(), tasks[4]);
651 EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
652
653 result = checker->check(this->env(), tasks[5]);
654 EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
655
656 result = checker->check(this->env(), tasks[6]);
657 EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
658
659 result = checker->check(this->env(), tasks[7]);
660 EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
661 });
662}
663
664TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) {
665 std::string formulasString = "Pmin=? [F \"elected\"]";
666 formulasString += "; Pmax=? [F \"elected\"]";
667 formulasString += "; Pmin=? [F<=25 \"elected\"]";
668 formulasString += "; Pmax=? [F<=25 \"elected\"]";
669 formulasString += "; Rmin=? [F \"elected\"]";
670 formulasString += "; Rmax=? [F \"elected\"]";
671
672 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString);
673 auto model = std::move(modelFormulas.first);
674 auto tasks = this->getTasks(modelFormulas.second);
675 this->execute(model, [&]() {
676 EXPECT_EQ(3172ul, model->getNumberOfStates());
677 EXPECT_EQ(7144ul, model->getNumberOfTransitions());
678 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
679 auto checker = this->createModelChecker(model);
680 std::unique_ptr<storm::modelchecker::CheckResult> result;
681
682 result = checker->check(this->env(), tasks[0]);
683 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
684
685 result = checker->check(this->env(), tasks[1]);
686 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
687
688 result = checker->check(this->env(), tasks[2]);
689 EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
690
691 result = checker->check(this->env(), tasks[3]);
692 EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
693
694 result = checker->check(this->env(), tasks[4]);
695 EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
696
697 result = checker->check(this->env(), tasks[5]);
698 EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
699 });
700}
701
702TYPED_TEST(MdpPrctlModelCheckerTest, consensus) {
703 std::string formulasString = "Pmax=? [F \"finished\"]";
704 formulasString += "; Pmax=? [F \"all_coins_equal_1\"]";
705 formulasString += "; P<0.8 [F \"all_coins_equal_1\"]";
706 formulasString += "; P<0.9 [F \"all_coins_equal_1\"]";
707 formulasString += "; Rmax=? [F \"all_coins_equal_1\"]";
708 formulasString += "; Rmin=? [F \"all_coins_equal_1\"]";
709 formulasString += "; Rmax=? [F \"finished\"]";
710 formulasString += "; Rmin=? [F \"finished\"]";
711
712 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
713 auto model = std::move(modelFormulas.first);
714 auto tasks = this->getTasks(modelFormulas.second);
715 this->execute(model, [&]() {
716 EXPECT_EQ(272ul, model->getNumberOfStates());
717 EXPECT_EQ(492ul, model->getNumberOfTransitions());
718 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
719 auto checker = this->createModelChecker(model);
720 std::unique_ptr<storm::modelchecker::CheckResult> result;
721
722 result = checker->check(this->env(), tasks[0]);
723 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
724
725 result = checker->check(this->env(), tasks[1]);
726 EXPECT_NEAR(this->parseNumber("57/64"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
727
728 result = checker->check(this->env(), tasks[2]);
729 EXPECT_FALSE(this->getQualitativeResultAtInitialState(model, result));
730
731 result = checker->check(this->env(), tasks[3]);
732 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
733
734 result = checker->check(this->env(), tasks[4]);
735 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
736
737 result = checker->check(this->env(), tasks[5]);
738 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
739
740 result = checker->check(this->env(), tasks[6]);
741 EXPECT_NEAR(this->parseNumber("75"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
742
743 result = checker->check(this->env(), tasks[7]);
744 EXPECT_NEAR(this->parseNumber("48"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
745 });
746}
747
748TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) {
749 std::string formulasString = "Rmin=? [F \"target\"]";
750 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString);
751 auto model = std::move(modelFormulas.first);
752 auto tasks = this->getTasks(modelFormulas.second);
753 this->execute(model, [&]() {
754 EXPECT_EQ(3ul, model->getNumberOfStates());
755 EXPECT_EQ(4ul, model->getNumberOfTransitions());
756 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
757 auto checker = this->createModelChecker(model);
758 std::unique_ptr<storm::modelchecker::CheckResult> result;
759
760 // This example considers a zero-reward end component that does not reach the target
761 // For some methods this requires end-component elimination which is (currently) not supported in the Dd engine
762
763 if (TypeParam::engine == MdpEngine::PrismDd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) {
764 STORM_SILENT_EXPECT_THROW(checker->check(this->env(), tasks[0]), storm::exceptions::UncheckedRequirementException);
765 } else {
766 result = checker->check(this->env(), tasks[0]);
767 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
768 }
769 });
770}
771
772TYPED_TEST(MdpPrctlModelCheckerTest, Team) {
773 std::string formulasString = "R{\"w_1_total\"}max=? [ C ]";
774 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm", formulasString);
775 auto model = std::move(modelFormulas.first);
776 auto tasks = this->getTasks(modelFormulas.second);
777 this->execute(model, [&]() {
778 EXPECT_EQ(12475ul, model->getNumberOfStates());
779 EXPECT_EQ(15228ul, model->getNumberOfTransitions());
780 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
781 auto checker = this->createModelChecker(model);
782 std::unique_ptr<storm::modelchecker::CheckResult> result;
783
784 // This example considers an expected total reward formula, which is not supported in all engines
785
786 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
787 result = checker->check(this->env(), tasks[0]);
788 EXPECT_NEAR(this->parseNumber("114/49"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
789 } else {
790 EXPECT_FALSE(checker->canHandle(tasks[0]));
791 }
792 });
793}
794
795TYPED_TEST(MdpPrctlModelCheckerTest, LtlProbabilitiesCoin) {
796#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
797 std::string formulasString = "Pmin=? [!(GF \"all_coins_equal_1\")]";
798 formulasString += "; Pmax=? [F \"all_coins_equal_1\" U \"finished\"]";
799 formulasString += "; P>0.4 [!(GF \"all_coins_equal_1\")]";
800 formulasString += "; P<0.6 [F \"all_coins_equal_1\" U \"finished\"]";
801 // The following example results in an automaton with acceptance condition not in DNF (Streett, using Spot)
802 formulasString += "; Pmax=?[ (GF \"all_coins_equal_1\") & ((GF \"all_coins_equal_0\") | (FG \"finished\"))]";
803
804 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
805 auto model = std::move(modelFormulas.first);
806 auto tasks = this->getTasks(modelFormulas.second);
807 this->execute(model, [&]() {
808 EXPECT_EQ(272ul, model->getNumberOfStates());
809 EXPECT_EQ(492ul, model->getNumberOfTransitions());
810 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
811 auto checker = this->createModelChecker(model);
812 std::unique_ptr<storm::modelchecker::CheckResult> result;
813
814 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
815 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
816 result = checker->check(this->env(), tasks[0]);
817 EXPECT_NEAR(this->parseNumber("4/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
818
819 result = checker->check(this->env(), tasks[1]);
820 EXPECT_NEAR(this->parseNumber("5/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
821
822 result = checker->check(this->env(), tasks[2]);
823 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
824
825 result = checker->check(this->env(), tasks[3]);
826 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
827
828 result = checker->check(this->env(), tasks[4]);
829 EXPECT_NEAR(this->parseNumber("5/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
830
831 } else {
832 EXPECT_FALSE(checker->canHandle(tasks[0]));
833 }
834 });
835#else
836 GTEST_SKIP();
837#endif
838}
839
840TYPED_TEST(MdpPrctlModelCheckerTest, LtlDice) {
841#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
842 std::string formulasString = "Pmax=? [ X (((s1=1) U (s1=3)) U (s1=7))]";
843 formulasString += "; Pmax=? [ (F (X (s1=6 & (XX s1=5)))) & (F G (d1!=5))]";
844 formulasString += "; Pmax=? [ F s1=3 U (\"three\")]";
845 formulasString += "; Pmin=? [! F (s2=6) & X \"done\"]";
846 // Acceptance condition not in DNF (Streett, using Spot)
847 formulasString += "; Pmax=? [ ( (G F !(\"two\")) | F G (\"three\") ) & ( (G F !(\"five\") ) | F G (\"seven\") )]";
848
849 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
850 auto model = std::move(modelFormulas.first);
851 auto tasks = this->getTasks(modelFormulas.second);
852 this->execute(model, [&]() {
853 EXPECT_EQ(169ul, model->getNumberOfStates());
854 EXPECT_EQ(436ul, model->getNumberOfTransitions());
855 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
856 auto checker = this->createModelChecker(model);
857 std::unique_ptr<storm::modelchecker::CheckResult> result;
858
859 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
860 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
861 result = checker->check(this->env(), tasks[0]);
862 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
863
864 result = checker->check(this->env(), tasks[1]);
865 EXPECT_NEAR(this->parseNumber("1/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
866
867 result = checker->check(this->env(), tasks[2]);
868 EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
869
870 result = checker->check(this->env(), tasks[3]);
871 EXPECT_NEAR(this->parseNumber("5/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
872
873 result = checker->check(this->env(), tasks[4]);
874 EXPECT_NEAR(this->parseNumber("31/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
875
876 } else {
877 EXPECT_FALSE(checker->canHandle(tasks[0]));
878 }
879 });
880#else
881 GTEST_SKIP();
882#endif
883}
884
885TYPED_TEST(MdpPrctlModelCheckerTest, LtlCoinFlips) {
886#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
887 std::string formulasString = "Pmax=? [ G (true U (heads | \"done\")) ]";
888 formulasString += "; Pmin=? [ G (true U (heads | \"done\")) ]";
889 formulasString += "; Pmax=? [ G (true U<=10 (heads | \"done\")) ]";
890 formulasString += "; Pmin=? [ G (true U<=10 (heads | \"done\")) ]";
891 formulasString += "; Pmax=? [ X G (true U<=0 (heads | \"done\")) ]";
892 formulasString += "; Pmax=? [ true U[10,12] heads ]";
893 formulasString += "; Pmax=? [ X (true U[0,0] heads) ]";
894 formulasString += "; Pmax=? [ G (!(P>=1 [\"done\"]) U<=10 (heads | P>=1 [ \"done\"])) ]";
895 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin_flips.nm", formulasString);
896 auto model = std::move(modelFormulas.first);
897 auto tasks = this->getTasks(modelFormulas.second);
898 this->execute(model, [&]() {
899 EXPECT_EQ(61ul, model->getNumberOfStates());
900 EXPECT_EQ(177ul, model->getNumberOfTransitions());
901 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
902 auto checker = this->createModelChecker(model);
903 std::unique_ptr<storm::modelchecker::CheckResult> result;
904
905 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
906 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
907 result = checker->check(this->env(), tasks[0]);
908 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
909
910 result = checker->check(this->env(), tasks[1]);
911 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
912
913 result = checker->check(this->env(), tasks[2]);
914 EXPECT_NEAR(this->parseNumber("1021/1024"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
915
916 result = checker->check(this->env(), tasks[3]);
917 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
918
919 result = checker->check(this->env(), tasks[4]);
920 EXPECT_NEAR(this->parseNumber("1/524288"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
921
922 result = checker->check(this->env(), tasks[5]);
923 EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
924
925 result = checker->check(this->env(), tasks[6]);
926 EXPECT_NEAR(this->parseNumber("1/2"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
927
928 result = checker->check(this->env(), tasks[7]);
929 EXPECT_NEAR(this->parseNumber("1021/1024"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
930
931 } else {
932 EXPECT_FALSE(checker->canHandle(tasks[0]));
933 }
934 });
935#else
936 GTEST_SKIP();
937#endif
938}
939
940TYPED_TEST(MdpPrctlModelCheckerTest, HOADice) {
941 // "P=? [ F "three" & (X s=1)]"
942 std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"three\", \"p1\" -> s2=1 }]";
943 // "P=? [!(s2=6) U "done"]"
944 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s2=6), \"p1\" -> \"done\" }]";
945
946 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
947 auto model = std::move(modelFormulas.first);
948 auto tasks = this->getTasks(modelFormulas.second);
949 this->execute(model, [&]() {
950 EXPECT_EQ(169ul, model->getNumberOfStates());
951 EXPECT_EQ(436ul, model->getNumberOfTransitions());
952 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
953 auto checker = this->createModelChecker(model);
954 std::unique_ptr<storm::modelchecker::CheckResult> result;
955
956 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
957 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
958 result = checker->check(tasks[0]);
959 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
960
961 result = checker->check(tasks[1]);
962 EXPECT_NEAR(this->parseNumber("3/4"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
963 } else {
964 EXPECT_FALSE(checker->canHandle(tasks[0]));
965 }
966 });
967}
968
969} // 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:14
storm::models::symbolic::Mdp
This class represents a discrete-time Markov decision process.
Definition Mdp.h:14
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:71
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:104