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