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