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