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