Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DtmcPrctlModelCheckerTest.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-parsers/parser/FormulaParser.h"
8#include "storm-parsers/parser/PrismParser.h"
9#include "storm/api/builder.h"
10#include "storm/api/properties.h"
11#include "storm/environment/solver/EigenSolverEnvironment.h"
12#include "storm/environment/solver/GmmxxSolverEnvironment.h"
13#include "storm/environment/solver/NativeSolverEnvironment.h"
14#include "storm/environment/solver/TopologicalSolverEnvironment.h"
15#include "storm/logic/Formulas.h"
16#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
17#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
18#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
19#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
20#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
21#include "storm/modelchecker/results/QualitativeCheckResult.h"
22#include "storm/modelchecker/results/QuantitativeCheckResult.h"
23#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
24#include "storm/models/sparse/Dtmc.h"
25#include "storm/models/sparse/StandardRewardModel.h"
26#include "storm/models/symbolic/Dtmc.h"
27#include "storm/models/symbolic/StandardRewardModel.h"
28#include "storm/settings/modules/CoreSettings.h"
29#include "storm/solver/EigenLinearEquationSolver.h"
30#include "storm/storage/expressions/ExpressionManager.h"
31
32namespace {
33
34enum class DtmcEngine { PrismSparse, JaniSparse, Hybrid, PrismDd, JaniDd };
35
36#ifdef STORM_HAVE_GMM
37class SparseGmmxxGmresIluEnvironment {
38 public:
39 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
40 static const DtmcEngine engine = DtmcEngine::PrismSparse;
41 static const bool isExact = false;
42 typedef double ValueType;
43 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
44 static storm::Environment createEnvironment() {
45 storm::Environment env;
46 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
47 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
48 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
49 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
50 return env;
51 }
52};
53
54class JaniSparseGmmxxGmresIluEnvironment {
55 public:
56 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
57 static const DtmcEngine engine = DtmcEngine::JaniSparse;
58 static const bool isExact = false;
59 typedef double ValueType;
60 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
61 static storm::Environment createEnvironment() {
62 storm::Environment env;
63 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
64 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
65 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
66 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
67 return env;
68 }
69};
70
71class SparseGmmxxGmresDiagEnvironment {
72 public:
73 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
74 static const DtmcEngine engine = DtmcEngine::PrismSparse;
75 static const bool isExact = false;
76 typedef double ValueType;
77 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
78 static storm::Environment createEnvironment() {
79 storm::Environment env;
80 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
81 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
82 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
83 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
84 return env;
85 }
86};
87
88class SparseGmmxxBicgstabIluEnvironment {
89 public:
90 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
91 static const DtmcEngine engine = DtmcEngine::PrismSparse;
92 static const bool isExact = false;
93 typedef double ValueType;
94 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
95 static storm::Environment createEnvironment() {
96 storm::Environment env;
97 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
98 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
99 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
100 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
101 return env;
102 }
103};
104#endif
105
106class SparseEigenDGmresEnvironment {
107 public:
108 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
109 static const DtmcEngine engine = DtmcEngine::PrismSparse;
110 static const bool isExact = false;
111 typedef double ValueType;
112 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
113 static storm::Environment createEnvironment() {
114 storm::Environment env;
115 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
116 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
117 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
118 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
119 return env;
120 }
121};
122
123class SparseEigenDoubleLUEnvironment {
124 public:
125 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
126 static const DtmcEngine engine = DtmcEngine::PrismSparse;
127 static const bool isExact = false;
128 typedef double ValueType;
129 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
130 static storm::Environment createEnvironment() {
131 storm::Environment env;
132 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
133 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
134 return env;
135 }
136};
137
138class SparseEigenRationalLUEnvironment {
139 public:
140 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
141 static const DtmcEngine engine = DtmcEngine::PrismSparse;
142 static const bool isExact = true;
143 typedef storm::RationalNumber ValueType;
144 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
145 static storm::Environment createEnvironment() {
146 storm::Environment env;
147 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
148 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
149 return env;
150 }
151};
152
153class SparseRationalEliminationEnvironment {
154 public:
155 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
156 static const DtmcEngine engine = DtmcEngine::PrismSparse;
157 static const bool isExact = true;
158 typedef storm::RationalNumber ValueType;
159 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
160 static storm::Environment createEnvironment() {
161 storm::Environment env;
162 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
163 return env;
164 }
165};
166
167class SparseNativeJacobiEnvironment {
168 public:
169 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
170 static const DtmcEngine engine = DtmcEngine::PrismSparse;
171 static const bool isExact = false;
172 typedef double ValueType;
173 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
174 static storm::Environment createEnvironment() {
175 storm::Environment env;
176 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
177 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
178 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
179 return env;
180 }
181};
182
183class SparseNativeWalkerChaeEnvironment {
184 public:
185 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
186 static const DtmcEngine engine = DtmcEngine::PrismSparse;
187 static const bool isExact = false;
188 typedef double ValueType;
189 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
190 static storm::Environment createEnvironment() {
191 storm::Environment env;
192 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
193 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
194 env.solver().native().setMaximalNumberOfIterations(1000000);
195 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-7));
196 return env;
197 }
198};
199
200class SparseNativeSorEnvironment {
201 public:
202 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
203 static const DtmcEngine engine = DtmcEngine::PrismSparse;
204 static const bool isExact = false;
205 typedef double ValueType;
206 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
207 static storm::Environment createEnvironment() {
208 storm::Environment env;
209 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
210 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
211 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
212 return env;
213 }
214};
215
216class SparseNativePowerEnvironment {
217 public:
218 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
219 static const DtmcEngine engine = DtmcEngine::PrismSparse;
220 static const bool isExact = false;
221 typedef double ValueType;
222 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
223 static storm::Environment createEnvironment() {
224 storm::Environment env;
225 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
226 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
227 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
228 return env;
229 }
230};
231
232class SparseNativeSoundValueIterationEnvironment {
233 public:
234 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
235 static const DtmcEngine engine = DtmcEngine::PrismSparse;
236 static const bool isExact = false;
237 typedef double ValueType;
238 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
239 static storm::Environment createEnvironment() {
240 storm::Environment env;
241 env.solver().setForceSoundness(true);
242 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
243 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration);
244 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
245 return env;
246 }
247};
248
249class SparseNativeOptimisticValueIterationEnvironment {
250 public:
251 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
252 static const DtmcEngine engine = DtmcEngine::PrismSparse;
253 static const bool isExact = false;
254 typedef double ValueType;
255 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
256 static storm::Environment createEnvironment() {
257 storm::Environment env;
258 env.solver().setForceSoundness(true);
259 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
260 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration);
261 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
262 return env;
263 }
264};
265
266class SparseNativeGuessingValueIterationEnvironment {
267 public:
268 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
269 static const DtmcEngine engine = DtmcEngine::PrismSparse;
270 static const bool isExact = false;
271 typedef double ValueType;
272 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
273 static storm::Environment createEnvironment() {
274 storm::Environment env;
275 env.solver().setForceSoundness(true);
276 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
277 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::GuessingValueIteration);
278 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
279 return env;
280 }
281};
282
283class SparseNativeIntervalIterationEnvironment {
284 public:
285 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
286 static const DtmcEngine engine = DtmcEngine::PrismSparse;
287 static const bool isExact = false;
288 typedef double ValueType;
289 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
290 static storm::Environment createEnvironment() {
291 storm::Environment env;
292 env.solver().setForceSoundness(true);
293 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
294 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::IntervalIteration);
295 env.solver().native().setRelativeTerminationCriterion(false);
296 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
297 return env;
298 }
299};
300
301class SparseNativeRationalSearchEnvironment {
302 public:
303 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
304 static const DtmcEngine engine = DtmcEngine::PrismSparse;
305 static const bool isExact = true;
306 typedef storm::RationalNumber ValueType;
307 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
308 static storm::Environment createEnvironment() {
309 storm::Environment env;
310 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
311 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
312 return env;
313 }
314};
315
316class SparseTopologicalEigenLUEnvironment {
317 public:
318 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
319 static const DtmcEngine engine = DtmcEngine::PrismSparse;
320 static const bool isExact = true;
321 typedef storm::RationalNumber ValueType;
322 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
323 static storm::Environment createEnvironment() {
324 storm::Environment env;
325 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
326 env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
327 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
328 return env;
329 }
330};
331
332#ifdef STORM_HAVE_GMM
333class HybridSylvanGmmxxGmresEnvironment {
334 public:
335 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
336 static const DtmcEngine engine = DtmcEngine::Hybrid;
337 static const bool isExact = false;
338 typedef double ValueType;
339 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
340
341 static void checkLibraryAvailable() {
342#ifndef STORM_HAVE_SYLVAN
343 GTEST_SKIP() << "Library Sylvan not available.";
344#endif
345 }
346
347 static storm::Environment createEnvironment() {
348 storm::Environment env;
349 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
350 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
351 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
352 return env;
353 }
354};
355#endif
356
357class HybridCuddNativeJacobiEnvironment {
358 public:
359 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
360 static const DtmcEngine engine = DtmcEngine::Hybrid;
361 static const bool isExact = false;
362 typedef double ValueType;
363 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
364
365 static void checkLibraryAvailable() {
366#ifndef STORM_HAVE_CUDD
367 GTEST_SKIP() << "Library CUDD not available.";
368#endif
369 }
370
371 static storm::Environment createEnvironment() {
372 storm::Environment env;
373 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
374 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
375 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
376 return env;
377 }
378};
379
380class HybridCuddNativeSoundValueIterationEnvironment {
381 public:
382 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
383 static const DtmcEngine engine = DtmcEngine::Hybrid;
384 static const bool isExact = false;
385 typedef double ValueType;
386 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
387
388 static void checkLibraryAvailable() {
389#ifndef STORM_HAVE_CUDD
390 GTEST_SKIP() << "Library CUDD not available.";
391#endif
392 }
393
394 static storm::Environment createEnvironment() {
395 storm::Environment env;
396 env.solver().setForceSoundness(true);
397 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
398 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
399 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
400 return env;
401 }
402};
403
404class HybridSylvanNativeRationalSearchEnvironment {
405 public:
406 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
407 static const DtmcEngine engine = DtmcEngine::Hybrid;
408 static const bool isExact = true;
409 typedef storm::RationalNumber ValueType;
410 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
411
412 static void checkLibraryAvailable() {
413#ifndef STORM_HAVE_SYLVAN
414 GTEST_SKIP() << "Library Sylvan not available.";
415#endif
416 }
417
418 static storm::Environment createEnvironment() {
419 storm::Environment env;
420 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
421 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
422 return env;
423 }
424};
425
426class DdSylvanNativePowerEnvironment {
427 public:
428 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
429 static const DtmcEngine engine = DtmcEngine::PrismDd;
430 static const bool isExact = false;
431 typedef double ValueType;
432 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
433
434 static void checkLibraryAvailable() {
435#ifndef STORM_HAVE_SYLVAN
436 GTEST_SKIP() << "Library Sylvan not available.";
437#endif
438 }
439
440 static storm::Environment createEnvironment() {
441 storm::Environment env;
442 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
443 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
444 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
445 return env;
446 }
447};
448
449class JaniDdSylvanNativePowerEnvironment {
450 public:
451 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
452 static const DtmcEngine engine = DtmcEngine::JaniDd;
453 static const bool isExact = false;
454 typedef double ValueType;
455 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
456
457 static void checkLibraryAvailable() {
458#ifndef STORM_HAVE_SYLVAN
459 GTEST_SKIP() << "Library Sylvan not available.";
460#endif
461 }
462
463 static storm::Environment createEnvironment() {
464 storm::Environment env;
465 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
466 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
467 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
468 return env;
469 }
470};
471
472class DdCuddNativeJacobiEnvironment {
473 public:
474 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
475 static const DtmcEngine engine = DtmcEngine::PrismDd;
476 static const bool isExact = false;
477 typedef double ValueType;
478 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
479
480 static void checkLibraryAvailable() {
481#ifndef STORM_HAVE_CUDD
482 GTEST_SKIP() << "Library CUDD not available.";
483#endif
484 }
485
486 static storm::Environment createEnvironment() {
487 storm::Environment env;
488 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
489 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
490 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
491 return env;
492 }
493};
494
495class DdSylvanRationalSearchEnvironment {
496 public:
497 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
498 static const DtmcEngine engine = DtmcEngine::PrismDd;
499 static const bool isExact = true;
500 typedef storm::RationalNumber ValueType;
501 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
502
503 static void checkLibraryAvailable() {
504#ifndef STORM_HAVE_SYLVAN
505 GTEST_SKIP() << "Library Sylvan not available.";
506#endif
507 }
508
509 static storm::Environment createEnvironment() {
510 storm::Environment env;
511 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
512 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
513 return env;
514 }
515};
516
517template<typename TestType>
518class DtmcPrctlModelCheckerTest : public ::testing::Test {
519 public:
520 typedef typename TestType::ValueType ValueType;
521 typedef typename storm::models::sparse::Dtmc<ValueType> SparseModelType;
522 typedef typename storm::models::symbolic::Dtmc<TestType::ddType, ValueType> SymbolicModelType;
523
524 DtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
525
526 void SetUp() override {
527#ifndef STORM_HAVE_Z3
528 GTEST_SKIP() << "Z3 not available.";
529#endif
530 if constexpr (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) {
531 TestType::checkLibraryAvailable();
532 }
533 }
534
535 storm::Environment const& env() const {
536 return _environment;
537 }
538 ValueType parseNumber(std::string const& input) const {
539 return storm::utility::convertNumber<ValueType>(input);
540 }
541 ValueType precision() const {
542 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
543 }
544 bool isSparseModel() const {
545 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
546 }
547 bool isSymbolicModel() const {
548 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
549 }
550
551 template<typename MT = typename TestType::ModelType>
552 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
553 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
554 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
555 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
556 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
557 program = storm::utility::prism::preprocess(program, constantDefinitionString);
558 if (TestType::engine == DtmcEngine::PrismSparse) {
559 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
560 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
561 } else if (TestType::engine == DtmcEngine::JaniSparse) {
562 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
563 result.second = storm::api::extractFormulasFromProperties(janiData.second);
564 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
565 }
566
567 return result;
568 }
569
570 template<typename MT = typename TestType::ModelType>
571 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
572 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
573 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
574 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
575 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
576 program = storm::utility::prism::preprocess(program, constantDefinitionString);
577 if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) {
578 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
579 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
580 } else if (TestType::engine == DtmcEngine::JaniDd) {
581 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
582 janiData.first.substituteFunctions();
583 result.second = storm::api::extractFormulasFromProperties(janiData.second);
584 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
585 }
586 return result;
587 }
588
589 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
590 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
591 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
592 for (auto const& f : formulas) {
593 result.emplace_back(*f);
594 }
595 return result;
596 }
597
598 template<typename MT = typename TestType::ModelType>
599 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
600 std::shared_ptr<MT> const& model) const {
601 if (TestType::engine == DtmcEngine::PrismSparse || TestType::engine == DtmcEngine::JaniSparse) {
602 return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<SparseModelType>>(*model);
603 }
604 }
605
606 template<typename MT = typename TestType::ModelType>
607 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
608 createModelChecker(std::shared_ptr<MT> const& model) const {
609 if (TestType::engine == DtmcEngine::Hybrid) {
610 return std::make_shared<storm::modelchecker::HybridDtmcPrctlModelChecker<SymbolicModelType>>(*model);
611 } else if (TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) {
612 return std::make_shared<storm::modelchecker::SymbolicDtmcPrctlModelChecker<SymbolicModelType>>(*model);
613 }
614 }
615
616 template<typename MT = typename TestType::ModelType>
617 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
618 std::function<void()> const& f) const {
619 f();
620 }
621
622 template<typename MT = typename TestType::ModelType>
623 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
624 std::function<void()> const& f) const {
625 model->getManager().execute(f);
626 }
627
628 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
629 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
630 auto filter = getInitialStateFilter(model);
631 result->filter(*filter);
632 return result->asQualitativeCheckResult().forallTrue();
633 }
634
635 ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
636 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
637 auto filter = getInitialStateFilter(model);
638 result->filter(*filter);
639 return result->asQuantitativeCheckResult<ValueType>().getMin();
640 }
641
642 private:
643 storm::Environment _environment;
644
645 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
646 if (isSparseModel()) {
647 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
648 } else {
649 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
650 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
651 }
652 }
653};
654
655typedef ::testing::Types<
656#ifdef STORM_HAVE_GMM
657 SparseGmmxxGmresIluEnvironment, JaniSparseGmmxxGmresIluEnvironment, SparseGmmxxGmresDiagEnvironment, SparseGmmxxBicgstabIluEnvironment,
658 HybridSylvanGmmxxGmresEnvironment,
659#endif
660 SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment, SparseEigenRationalLUEnvironment, SparseRationalEliminationEnvironment,
661 SparseNativeJacobiEnvironment, SparseNativeWalkerChaeEnvironment, SparseNativeSorEnvironment, SparseNativePowerEnvironment,
662 SparseNativeSoundValueIterationEnvironment, SparseNativeOptimisticValueIterationEnvironment, SparseNativeGuessingValueIterationEnvironment,
663 SparseNativeIntervalIterationEnvironment, SparseNativeRationalSearchEnvironment, SparseTopologicalEigenLUEnvironment, HybridCuddNativeJacobiEnvironment,
664 HybridCuddNativeSoundValueIterationEnvironment, HybridSylvanNativeRationalSearchEnvironment, DdSylvanNativePowerEnvironment,
665 JaniDdSylvanNativePowerEnvironment, DdCuddNativeJacobiEnvironment, DdSylvanRationalSearchEnvironment>
666 TestingTypes;
667
668TYPED_TEST_SUITE(DtmcPrctlModelCheckerTest, TestingTypes, );
669
670TYPED_TEST(DtmcPrctlModelCheckerTest, Die) {
671 std::string formulasString = "P=? [F \"one\"]";
672 formulasString += "; P=? [F \"two\"]";
673 formulasString += "; P=? [F \"three\"]";
674 formulasString += "; R=? [F \"done\"]";
675
676 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
677 auto model = std::move(modelFormulas.first);
678 auto tasks = this->getTasks(modelFormulas.second);
679 this->execute(model, [&]() {
680 EXPECT_EQ(13ul, model->getNumberOfStates());
681 EXPECT_EQ(20ul, model->getNumberOfTransitions());
682 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
683 auto checker = this->createModelChecker(model);
684 std::unique_ptr<storm::modelchecker::CheckResult> result;
685
686 result = checker->check(this->env(), tasks[0]);
687 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
688
689 result = checker->check(this->env(), tasks[1]);
690 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
691
692 result = checker->check(this->env(), tasks[2]);
693 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
694
695 result = checker->check(this->env(), tasks[3]);
696 EXPECT_NEAR(this->parseNumber("11/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
697 });
698}
699
700TYPED_TEST(DtmcPrctlModelCheckerTest, Crowds) {
701 std::string formulasString = "P=? [F observe0>1]";
702 formulasString += "; P=? [F \"observeIGreater1\"]";
703 formulasString += "; P=? [F observe1>1]";
704
705 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", formulasString);
706 auto model = std::move(modelFormulas.first);
707 auto tasks = this->getTasks(modelFormulas.second);
708 this->execute(model, [&]() {
709 EXPECT_EQ(726ul, model->getNumberOfStates());
710 EXPECT_EQ(1146ul, model->getNumberOfTransitions());
711 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
712 auto checker = this->createModelChecker(model);
713 std::unique_ptr<storm::modelchecker::CheckResult> result;
714
715 result = checker->check(this->env(), tasks[0]);
716 EXPECT_NEAR(this->parseNumber("78686542099694893/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
717
718 result = checker->check(this->env(), tasks[1]);
719 EXPECT_NEAR(this->parseNumber("40300855878315123/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
720
721 result = checker->check(this->env(), tasks[2]);
722 EXPECT_NEAR(this->parseNumber("13433618626105041/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
723 });
724}
725
726TYPED_TEST(DtmcPrctlModelCheckerTest, SynchronousLeader) {
727 std::string formulasString = "P=? [F \"elected\"]";
728 formulasString += "; P=? [F<=5 \"elected\"]";
729 formulasString += "; R=? [F \"elected\"]";
730
731 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
732 auto model = std::move(modelFormulas.first);
733 auto tasks = this->getTasks(modelFormulas.second);
734 this->execute(model, [&]() {
735 EXPECT_EQ(273ul, model->getNumberOfStates());
736 EXPECT_EQ(397ul, model->getNumberOfTransitions());
737 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
738 auto checker = this->createModelChecker(model);
739 std::unique_ptr<storm::modelchecker::CheckResult> result;
740
741 result = checker->check(this->env(), tasks[0]);
742 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
743
744 result = checker->check(this->env(), tasks[1]);
745 EXPECT_NEAR(this->parseNumber("24/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
746
747 result = checker->check(this->env(), tasks[2]);
748 EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
749 });
750}
751
752TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) {
753#ifndef STORM_HAVE_Z3
754 GTEST_SKIP() << "Z3 not available.";
755#endif
756 std::string formulasString = "P=? [F \"one\"]";
757 formulasString += "; P=? [F \"two\"]";
758 formulasString += "; P=? [F \"three\"]";
759
760 storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
761 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
762 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, double>> tasks;
763 for (auto const& f : formulas) {
764 tasks.emplace_back(*f);
765 }
766 auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::Dtmc<double>>();
767 EXPECT_EQ(13ul, model->getNumberOfStates());
768 EXPECT_EQ(20ul, model->getNumberOfTransitions());
769
770 storm::storage::SparseMatrix<double> matrix = model->getTransitionMatrix();
771 storm::storage::BitVector initialStates(13);
772 initialStates.set(0);
773 storm::storage::BitVector phiStates(13);
774 storm::storage::BitVector psiStates(13);
775 psiStates.set(7);
776 psiStates.set(8);
777 psiStates.set(9);
778 psiStates.set(10);
779 psiStates.set(11);
780 psiStates.set(12);
781 storm::Environment env;
782 storm::solver::SolveGoal<double> goal(*model, tasks[0]);
783 std::vector<double> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix,
784 initialStates, phiStates, psiStates);
785
786 EXPECT_NEAR(1.0 / 6, result[7], 1e-6);
787 EXPECT_NEAR(1.0 / 6, result[8], 1e-6);
788 EXPECT_NEAR(1.0 / 6, result[9], 1e-6);
789 EXPECT_NEAR(1.0 / 6, result[10], 1e-6);
790 EXPECT_NEAR(1.0 / 6, result[11], 1e-6);
791 EXPECT_NEAR(1.0 / 6, result[12], 1e-6);
792
793 phiStates.set(6);
794 psiStates.set(1);
795 result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates,
796 psiStates);
797
798 EXPECT_NEAR(1, result[0], 1e-6);
799 EXPECT_NEAR(0.5, result[1], 1e-6);
800 EXPECT_NEAR(0.5, result[2], 1e-6);
801 EXPECT_NEAR(0.25, result[5], 1e-6);
802 EXPECT_NEAR(0, result[7], 1e-6);
803 EXPECT_NEAR(0, result[8], 1e-6);
804 EXPECT_NEAR(0, result[9], 1e-6);
805 EXPECT_NEAR(0.125, result[10], 1e-6);
806 EXPECT_NEAR(0.125, result[11], 1e-6);
807 EXPECT_NEAR(0, result[12], 1e-6);
808}
809
810TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesDie) {
811#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
812 std::string formulasString = "P=? [(X s>0) U (s=7 & d=2)]";
813 formulasString += "; P=? [ X (((s=1) U (s=3)) U (s=7))]";
814 formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]";
815 formulasString += "; P=? [ F (s=3 U (\"three\"))]";
816 formulasString += "; P=? [ F s=3 U (\"three\")]";
817 formulasString += "; P=? [ F (s=6) & X \"done\"]";
818 formulasString += "; P=? [ (F s=6) & (X \"done\")]";
819
820 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
821 auto model = std::move(modelFormulas.first);
822 auto tasks = this->getTasks(modelFormulas.second);
823 this->execute(model, [&]() {
824 EXPECT_EQ(13ul, model->getNumberOfStates());
825 EXPECT_EQ(20ul, model->getNumberOfTransitions());
826 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
827 auto checker = this->createModelChecker(model);
828 std::unique_ptr<storm::modelchecker::CheckResult> result;
829
830 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
831 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
832 result = checker->check(tasks[0]);
833 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
834
835 result = checker->check(tasks[1]);
836 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
837
838 result = checker->check(tasks[2]);
839 EXPECT_NEAR(this->parseNumber("1/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
840
841 result = checker->check(tasks[3]);
842 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
843
844 result = checker->check(tasks[4]);
845 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
846
847 result = checker->check(tasks[5]);
848 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
849
850 result = checker->check(tasks[6]);
851 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
852 } else {
853 EXPECT_FALSE(checker->canHandle(tasks[0]));
854 }
855 });
856#else
857 GTEST_SKIP();
858#endif
859}
860
861TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesSynchronousLeader) {
862#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
863 std::string formulasString = "P=? [X (u1=true U \"elected\")]";
864 formulasString += "; P=? [X !(u1=true U \"elected\")]";
865 formulasString += "; P=? [X v1=2 & X v1=1]";
866 formulasString += "; P=? [(X v1=2) & (X v1=1)]";
867 formulasString += "; P=? [(!X v1=2) & (X v1=1)]";
868
869 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
870 auto model = std::move(modelFormulas.first);
871 auto tasks = this->getTasks(modelFormulas.second);
872 this->execute(model, [&]() {
873 EXPECT_EQ(273ul, model->getNumberOfStates());
874 EXPECT_EQ(397ul, model->getNumberOfTransitions());
875 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
876 auto checker = this->createModelChecker(model);
877 std::unique_ptr<storm::modelchecker::CheckResult> result;
878
879 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
880 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
881 result = checker->check(tasks[0]);
882 EXPECT_NEAR(this->parseNumber("16/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
883
884 result = checker->check(tasks[1]);
885 EXPECT_NEAR(this->parseNumber("9/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
886
887 result = checker->check(tasks[2]);
888 EXPECT_NEAR(this->parseNumber("1/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
889
890 result = checker->check(tasks[3]);
891 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
892
893 result = checker->check(tasks[4]);
894 EXPECT_NEAR(this->parseNumber("1/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
895
896 } else {
897 EXPECT_FALSE(checker->canHandle(tasks[0]));
898 }
899 });
900#else
901 GTEST_SKIP();
902#endif
903}
904
905TYPED_TEST(DtmcPrctlModelCheckerTest, HOAProbabilitiesDie) {
906 // "P=? [(X s>0) U (s=7 & d=2)]"
907 std::string formulasString = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (s=7 & d=2) }]";
908 // "P=? [(X s>0) U (d=4 | d=2)]"
909 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (d=4 | d=2) }]";
910 // "P=? [ (F s=4) & (X \"three\")]"
911 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4), \"p1\" -> \"three\" }]";
912 // "P=? [ (F s=6) & (X \"done\")]"
913 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> \"done\" }]";
914 // "P=? [ (F s=6) & (X !\"done\")]"
915 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> !\"done\" }]";
916 // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]"
917 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]";
918 // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]"
919 formulasString += "; P>0.3[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]";
920
921 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
922 auto model = std::move(modelFormulas.first);
923 auto tasks = this->getTasks(modelFormulas.second);
924 this->execute(model, [&]() {
925 EXPECT_EQ(13ul, model->getNumberOfStates());
926 EXPECT_EQ(20ul, model->getNumberOfTransitions());
927 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
928 auto checker = this->createModelChecker(model);
929 std::unique_ptr<storm::modelchecker::CheckResult> result;
930
931 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
932 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
933 result = checker->check(tasks[0]);
934 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
935
936 result = checker->check(tasks[1]);
937 EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
938
939 result = checker->check(tasks[2]);
940 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
941
942 result = checker->check(tasks[3]);
943 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
944
945 result = checker->check(tasks[4]);
946 EXPECT_NEAR(this->parseNumber("1/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
947
948 result = checker->check(tasks[5]);
949 EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
950
951 result = checker->check(tasks[6]);
952 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
953 } else {
954 EXPECT_FALSE(checker->canHandle(tasks[0]));
955 }
956 });
957}
958
959TYPED_TEST(DtmcPrctlModelCheckerTest, SmallDiscount) {
960 if (TypeParam::isExact) {
961 GTEST_SKIP() << "Exact computations for discounted properties are not supported.";
962 }
963 std::string formulasString = "R=? [ C ]";
964 formulasString += "; R=? [ Cdiscount=9/10 ]";
965 formulasString += "; R=? [ Cdiscount=15/16 ]";
966 formulasString += "; R=? [ C<5discount=9/10 ]";
967 formulasString += "; R=? [ C<5discount=15/16 ]";
968 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/small_discount.nm", formulasString);
969 auto model = std::move(modelFormulas.first);
970 auto tasks = this->getTasks(modelFormulas.second);
971 EXPECT_EQ(3ul, model->getNumberOfStates());
972 EXPECT_EQ(4ul, model->getNumberOfTransitions());
973 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
974 auto checker = this->createModelChecker(model);
975
976 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
977 std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(this->env(), tasks[0]);
978 EXPECT_NEAR(this->parseNumber("5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
979
980 result = checker->check(this->env(), tasks[1]);
981 EXPECT_NEAR(this->parseNumber("45/14"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
982 result = checker->check(this->env(), tasks[2]);
983 EXPECT_NEAR(this->parseNumber("15/4"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
984 result = checker->check(this->env(), tasks[3]);
985 EXPECT_NEAR(this->parseNumber("12591/6250"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
986 result = checker->check(this->env(), tasks[4]);
987 EXPECT_NEAR(this->parseNumber("555/256"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
988 } else {
989 EXPECT_FALSE(checker->canHandle(tasks[0]));
990 EXPECT_FALSE(checker->canHandle(tasks[1]));
991 EXPECT_FALSE(checker->canHandle(tasks[2]));
992 EXPECT_FALSE(checker->canHandle(tasks[3]));
993 EXPECT_FALSE(checker->canHandle(tasks[4]));
994 }
995}
996
997} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:15
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::EigenSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition EigenSolverEnvironment.cpp:70
storm::EigenSolverEnvironment::setPreconditioner
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
Definition EigenSolverEnvironment.cpp:46
storm::EigenSolverEnvironment::setMethod
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
Definition EigenSolverEnvironment.cpp:37
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::GmmxxSolverEnvironment::setMethod
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
Definition GmmxxSolverEnvironment.cpp:32
storm::GmmxxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition GmmxxSolverEnvironment.cpp:64
storm::GmmxxSolverEnvironment::setPreconditioner
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
Definition GmmxxSolverEnvironment.cpp:40
storm::NativeSolverEnvironment::setMaximalNumberOfIterations
void setMaximalNumberOfIterations(uint64_t value)
Definition NativeSolverEnvironment.cpp:52
storm::NativeSolverEnvironment::setMethod
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
Definition NativeSolverEnvironment.cpp:43
storm::NativeSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition NativeSolverEnvironment.cpp:60
storm::SolverEnvironment::topological
TopologicalSolverEnvironment & topological()
Definition SolverEnvironment.cpp:91
storm::SolverEnvironment::setLinearEquationSolverType
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
Definition SolverEnvironment.cpp:127
storm::SolverEnvironment::eigen
EigenSolverEnvironment & eigen()
Definition SolverEnvironment.cpp:59
storm::SolverEnvironment::native
NativeSolverEnvironment & native()
Definition SolverEnvironment.cpp:75
storm::SolverEnvironment::gmmxx
GmmxxSolverEnvironment & gmmxx()
Definition SolverEnvironment.cpp:67
storm::TopologicalSolverEnvironment::setUnderlyingEquationSolverType
void setUnderlyingEquationSolverType(storm::solver::EquationSolverType value)
Definition TopologicalSolverEnvironment.cpp:33
storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities
static std::vector< ValueType > computeAllUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition SparseDtmcPrctlHelper.cpp:247
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:328
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
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:62
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59
storm_gtest.h