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