Storm
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 SparseNativeIntervalIterationEnvironment {
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::IntervalIteration);
276 env.solver().native().setRelativeTerminationCriterion(false);
277 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
278 return env;
279 }
280};
281
282class SparseNativeRationalSearchEnvironment {
283 public:
284 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
285 static const DtmcEngine engine = DtmcEngine::PrismSparse;
286 static const bool isExact = true;
287 typedef storm::RationalNumber ValueType;
288 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
289 static storm::Environment createEnvironment() {
290 storm::Environment env;
291 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
292 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
293 return env;
294 }
295};
296
297class SparseTopologicalEigenLUEnvironment {
298 public:
299 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
300 static const DtmcEngine engine = DtmcEngine::PrismSparse;
301 static const bool isExact = true;
302 typedef storm::RationalNumber ValueType;
303 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
304 static storm::Environment createEnvironment() {
305 storm::Environment env;
306 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
307 env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
308 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
309 return env;
310 }
311};
312
313class HybridSylvanGmmxxGmresEnvironment {
314 public:
315 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
316 static const DtmcEngine engine = DtmcEngine::Hybrid;
317 static const bool isExact = false;
318 typedef double ValueType;
319 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
320 static storm::Environment createEnvironment() {
321 storm::Environment env;
322 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
323 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
324 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
325 return env;
326 }
327};
328
329class HybridCuddNativeJacobiEnvironment {
330 public:
331 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
332 static const DtmcEngine engine = DtmcEngine::Hybrid;
333 static const bool isExact = false;
334 typedef double ValueType;
335 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
336 static storm::Environment createEnvironment() {
337 storm::Environment env;
338 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
339 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
340 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
341 return env;
342 }
343};
344
345class HybridCuddNativeSoundValueIterationEnvironment {
346 public:
347 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
348 static const DtmcEngine engine = DtmcEngine::Hybrid;
349 static const bool isExact = false;
350 typedef double ValueType;
351 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
352 static storm::Environment createEnvironment() {
353 storm::Environment env;
354 env.solver().setForceSoundness(true);
355 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
356 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
357 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
358 return env;
359 }
360};
361
362class HybridSylvanNativeRationalSearchEnvironment {
363 public:
364 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
365 static const DtmcEngine engine = DtmcEngine::Hybrid;
366 static const bool isExact = true;
367 typedef storm::RationalNumber ValueType;
368 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
369 static storm::Environment createEnvironment() {
370 storm::Environment env;
371 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
372 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
373 return env;
374 }
375};
376
377class DdSylvanNativePowerEnvironment {
378 public:
379 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
380 static const DtmcEngine engine = DtmcEngine::PrismDd;
381 static const bool isExact = false;
382 typedef double ValueType;
383 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
384 static storm::Environment createEnvironment() {
385 storm::Environment env;
386 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
387 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
388 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
389 return env;
390 }
391};
392
393class JaniDdSylvanNativePowerEnvironment {
394 public:
395 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
396 static const DtmcEngine engine = DtmcEngine::JaniDd;
397 static const bool isExact = false;
398 typedef double ValueType;
399 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
400 static storm::Environment createEnvironment() {
401 storm::Environment env;
402 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
403 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
404 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
405 return env;
406 }
407};
408
409class DdCuddNativeJacobiEnvironment {
410 public:
411 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
412 static const DtmcEngine engine = DtmcEngine::PrismDd;
413 static const bool isExact = false;
414 typedef double ValueType;
415 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
416 static storm::Environment createEnvironment() {
417 storm::Environment env;
418 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
419 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
420 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
421 return env;
422 }
423};
424
425class DdSylvanRationalSearchEnvironment {
426 public:
427 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
428 static const DtmcEngine engine = DtmcEngine::PrismDd;
429 static const bool isExact = true;
430 typedef storm::RationalNumber ValueType;
431 typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
432 static storm::Environment createEnvironment() {
433 storm::Environment env;
434 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
435 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
436 return env;
437 }
438};
439
440template<typename TestType>
441class DtmcPrctlModelCheckerTest : public ::testing::Test {
442 public:
443 typedef typename TestType::ValueType ValueType;
444 typedef typename storm::models::sparse::Dtmc<ValueType> SparseModelType;
445 typedef typename storm::models::symbolic::Dtmc<TestType::ddType, ValueType> SymbolicModelType;
446
447 DtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
448
449 void SetUp() override {
450#ifndef STORM_HAVE_Z3
451 GTEST_SKIP() << "Z3 not available.";
452#endif
453 }
454
455 storm::Environment const& env() const {
456 return _environment;
457 }
458 ValueType parseNumber(std::string const& input) const {
459 return storm::utility::convertNumber<ValueType>(input);
460 }
461 ValueType precision() const {
462 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
463 }
464 bool isSparseModel() const {
465 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
466 }
467 bool isSymbolicModel() const {
468 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
469 }
470
471 template<typename MT = typename TestType::ModelType>
472 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
473 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
474 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
475 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
476 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
477 program = storm::utility::prism::preprocess(program, constantDefinitionString);
478 if (TestType::engine == DtmcEngine::PrismSparse) {
479 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
480 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
481 } else if (TestType::engine == DtmcEngine::JaniSparse) {
482 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
483 result.second = storm::api::extractFormulasFromProperties(janiData.second);
484 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
485 }
486
487 return result;
488 }
489
490 template<typename MT = typename TestType::ModelType>
491 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
492 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
493 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
494 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
495 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
496 program = storm::utility::prism::preprocess(program, constantDefinitionString);
497 if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) {
498 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
499 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
500 } else if (TestType::engine == DtmcEngine::JaniDd) {
501 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
502 janiData.first.substituteFunctions();
503 result.second = storm::api::extractFormulasFromProperties(janiData.second);
504 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
505 }
506 return result;
507 }
508
509 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
510 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
511 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
512 for (auto const& f : formulas) {
513 result.emplace_back(*f);
514 }
515 return result;
516 }
517
518 template<typename MT = typename TestType::ModelType>
519 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
520 std::shared_ptr<MT> const& model) const {
521 if (TestType::engine == DtmcEngine::PrismSparse || TestType::engine == DtmcEngine::JaniSparse) {
522 return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<SparseModelType>>(*model);
523 }
524 }
525
526 template<typename MT = typename TestType::ModelType>
527 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
528 createModelChecker(std::shared_ptr<MT> const& model) const {
529 if (TestType::engine == DtmcEngine::Hybrid) {
530 return std::make_shared<storm::modelchecker::HybridDtmcPrctlModelChecker<SymbolicModelType>>(*model);
531 } else if (TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) {
532 return std::make_shared<storm::modelchecker::SymbolicDtmcPrctlModelChecker<SymbolicModelType>>(*model);
533 }
534 }
535
536 template<typename MT = typename TestType::ModelType>
537 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
538 std::function<void()> const& f) const {
539 f();
540 }
541
542 template<typename MT = typename TestType::ModelType>
543 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
544 std::function<void()> const& f) const {
545 model->getManager().execute(f);
546 }
547
548 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
549 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
550 auto filter = getInitialStateFilter(model);
551 result->filter(*filter);
552 return result->asQualitativeCheckResult().forallTrue();
553 }
554
555 ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
556 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
557 auto filter = getInitialStateFilter(model);
558 result->filter(*filter);
559 return result->asQuantitativeCheckResult<ValueType>().getMin();
560 }
561
562 private:
563 storm::Environment _environment;
564
565 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
566 if (isSparseModel()) {
567 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
568 } else {
569 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
570 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
571 }
572 }
573};
574
575typedef ::testing::Types<SparseGmmxxGmresIluEnvironment, JaniSparseGmmxxGmresIluEnvironment, SparseGmmxxGmresDiagEnvironment, SparseGmmxxBicgstabIluEnvironment,
576 SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment, SparseEigenRationalLUEnvironment, SparseRationalEliminationEnvironment,
577 SparseNativeJacobiEnvironment, SparseNativeWalkerChaeEnvironment, SparseNativeSorEnvironment, SparseNativePowerEnvironment,
578 SparseNativeSoundValueIterationEnvironment, SparseNativeOptimisticValueIterationEnvironment, SparseNativeIntervalIterationEnvironment,
579 SparseNativeRationalSearchEnvironment, SparseTopologicalEigenLUEnvironment, HybridSylvanGmmxxGmresEnvironment,
580 HybridCuddNativeJacobiEnvironment, HybridCuddNativeSoundValueIterationEnvironment, HybridSylvanNativeRationalSearchEnvironment,
581 DdSylvanNativePowerEnvironment, JaniDdSylvanNativePowerEnvironment, DdCuddNativeJacobiEnvironment, DdSylvanRationalSearchEnvironment>
582 TestingTypes;
583
584TYPED_TEST_SUITE(DtmcPrctlModelCheckerTest, TestingTypes, );
585
586TYPED_TEST(DtmcPrctlModelCheckerTest, Die) {
587 std::string formulasString = "P=? [F \"one\"]";
588 formulasString += "; P=? [F \"two\"]";
589 formulasString += "; P=? [F \"three\"]";
590 formulasString += "; R=? [F \"done\"]";
591
592 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
593 auto model = std::move(modelFormulas.first);
594 auto tasks = this->getTasks(modelFormulas.second);
595 this->execute(model, [&]() {
596 EXPECT_EQ(13ul, model->getNumberOfStates());
597 EXPECT_EQ(20ul, model->getNumberOfTransitions());
598 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
599 auto checker = this->createModelChecker(model);
600 std::unique_ptr<storm::modelchecker::CheckResult> result;
601
602 result = checker->check(this->env(), tasks[0]);
603 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
604
605 result = checker->check(this->env(), tasks[1]);
606 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
607
608 result = checker->check(this->env(), tasks[2]);
609 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
610
611 result = checker->check(this->env(), tasks[3]);
612 EXPECT_NEAR(this->parseNumber("11/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
613 });
614}
615
616TYPED_TEST(DtmcPrctlModelCheckerTest, Crowds) {
617 std::string formulasString = "P=? [F observe0>1]";
618 formulasString += "; P=? [F \"observeIGreater1\"]";
619 formulasString += "; P=? [F observe1>1]";
620
621 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", formulasString);
622 auto model = std::move(modelFormulas.first);
623 auto tasks = this->getTasks(modelFormulas.second);
624 this->execute(model, [&]() {
625 EXPECT_EQ(726ul, model->getNumberOfStates());
626 EXPECT_EQ(1146ul, model->getNumberOfTransitions());
627 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
628 auto checker = this->createModelChecker(model);
629 std::unique_ptr<storm::modelchecker::CheckResult> result;
630
631 result = checker->check(this->env(), tasks[0]);
632 EXPECT_NEAR(this->parseNumber("78686542099694893/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
633
634 result = checker->check(this->env(), tasks[1]);
635 EXPECT_NEAR(this->parseNumber("40300855878315123/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
636
637 result = checker->check(this->env(), tasks[2]);
638 EXPECT_NEAR(this->parseNumber("13433618626105041/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
639 });
640}
641
642TYPED_TEST(DtmcPrctlModelCheckerTest, SynchronousLeader) {
643 std::string formulasString = "P=? [F \"elected\"]";
644 formulasString += "; P=? [F<=5 \"elected\"]";
645 formulasString += "; R=? [F \"elected\"]";
646
647 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
648 auto model = std::move(modelFormulas.first);
649 auto tasks = this->getTasks(modelFormulas.second);
650 this->execute(model, [&]() {
651 EXPECT_EQ(273ul, model->getNumberOfStates());
652 EXPECT_EQ(397ul, model->getNumberOfTransitions());
653 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
654 auto checker = this->createModelChecker(model);
655 std::unique_ptr<storm::modelchecker::CheckResult> result;
656
657 result = checker->check(this->env(), tasks[0]);
658 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
659
660 result = checker->check(this->env(), tasks[1]);
661 EXPECT_NEAR(this->parseNumber("24/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
662
663 result = checker->check(this->env(), tasks[2]);
664 EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
665 });
666}
667
668TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) {
669#ifndef STORM_HAVE_Z3
670 GTEST_SKIP() << "Z3 not available.";
671#endif
672 std::string formulasString = "P=? [F \"one\"]";
673 formulasString += "; P=? [F \"two\"]";
674 formulasString += "; P=? [F \"three\"]";
675
676 storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
677 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
678 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, double>> tasks;
679 for (auto const& f : formulas) {
680 tasks.emplace_back(*f);
681 }
682 auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::Dtmc<double>>();
683 EXPECT_EQ(13ul, model->getNumberOfStates());
684 EXPECT_EQ(20ul, model->getNumberOfTransitions());
685
686 storm::storage::SparseMatrix<double> matrix = model->getTransitionMatrix();
687 storm::storage::BitVector initialStates(13);
688 initialStates.set(0);
689 storm::storage::BitVector phiStates(13);
690 storm::storage::BitVector psiStates(13);
691 psiStates.set(7);
692 psiStates.set(8);
693 psiStates.set(9);
694 psiStates.set(10);
695 psiStates.set(11);
696 psiStates.set(12);
697 storm::Environment env;
698 storm::solver::SolveGoal<double> goal(*model, tasks[0]);
699 std::vector<double> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix,
700 initialStates, phiStates, psiStates);
701
702 EXPECT_NEAR(1.0 / 6, result[7], 1e-6);
703 EXPECT_NEAR(1.0 / 6, result[8], 1e-6);
704 EXPECT_NEAR(1.0 / 6, result[9], 1e-6);
705 EXPECT_NEAR(1.0 / 6, result[10], 1e-6);
706 EXPECT_NEAR(1.0 / 6, result[11], 1e-6);
707 EXPECT_NEAR(1.0 / 6, result[12], 1e-6);
708
709 phiStates.set(6);
710 psiStates.set(1);
711 result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates,
712 psiStates);
713
714 EXPECT_NEAR(1, result[0], 1e-6);
715 EXPECT_NEAR(0.5, result[1], 1e-6);
716 EXPECT_NEAR(0.5, result[2], 1e-6);
717 EXPECT_NEAR(0.25, result[5], 1e-6);
718 EXPECT_NEAR(0, result[7], 1e-6);
719 EXPECT_NEAR(0, result[8], 1e-6);
720 EXPECT_NEAR(0, result[9], 1e-6);
721 EXPECT_NEAR(0.125, result[10], 1e-6);
722 EXPECT_NEAR(0.125, result[11], 1e-6);
723 EXPECT_NEAR(0, result[12], 1e-6);
724}
725
726TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesDie) {
727#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
728 std::string formulasString = "P=? [(X s>0) U (s=7 & d=2)]";
729 formulasString += "; P=? [ X (((s=1) U (s=3)) U (s=7))]";
730 formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]";
731 formulasString += "; P=? [ F (s=3 U (\"three\"))]";
732 formulasString += "; P=? [ F s=3 U (\"three\")]";
733 formulasString += "; P=? [ F (s=6) & X \"done\"]";
734 formulasString += "; P=? [ (F s=6) & (X \"done\")]";
735
736 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
737 auto model = std::move(modelFormulas.first);
738 auto tasks = this->getTasks(modelFormulas.second);
739 this->execute(model, [&]() {
740 EXPECT_EQ(13ul, model->getNumberOfStates());
741 EXPECT_EQ(20ul, model->getNumberOfTransitions());
742 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
743 auto checker = this->createModelChecker(model);
744 std::unique_ptr<storm::modelchecker::CheckResult> result;
745
746 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
747 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
748 result = checker->check(tasks[0]);
749 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
750
751 result = checker->check(tasks[1]);
752 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
753
754 result = checker->check(tasks[2]);
755 EXPECT_NEAR(this->parseNumber("1/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
756
757 result = checker->check(tasks[3]);
758 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
759
760 result = checker->check(tasks[4]);
761 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
762
763 result = checker->check(tasks[5]);
764 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
765
766 result = checker->check(tasks[6]);
767 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
768 } else {
769 EXPECT_FALSE(checker->canHandle(tasks[0]));
770 }
771 });
772#else
773 GTEST_SKIP();
774#endif
775}
776
777TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesSynchronousLeader) {
778#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
779 std::string formulasString = "P=? [X (u1=true U \"elected\")]";
780 formulasString += "; P=? [X !(u1=true U \"elected\")]";
781 formulasString += "; P=? [X v1=2 & X v1=1]";
782 formulasString += "; P=? [(X v1=2) & (X v1=1)]";
783 formulasString += "; P=? [(!X v1=2) & (X v1=1)]";
784
785 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
786 auto model = std::move(modelFormulas.first);
787 auto tasks = this->getTasks(modelFormulas.second);
788 this->execute(model, [&]() {
789 EXPECT_EQ(273ul, model->getNumberOfStates());
790 EXPECT_EQ(397ul, model->getNumberOfTransitions());
791 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
792 auto checker = this->createModelChecker(model);
793 std::unique_ptr<storm::modelchecker::CheckResult> result;
794
795 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
796 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
797 result = checker->check(tasks[0]);
798 EXPECT_NEAR(this->parseNumber("16/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
799
800 result = checker->check(tasks[1]);
801 EXPECT_NEAR(this->parseNumber("9/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
802
803 result = checker->check(tasks[2]);
804 EXPECT_NEAR(this->parseNumber("1/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
805
806 result = checker->check(tasks[3]);
807 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
808
809 result = checker->check(tasks[4]);
810 EXPECT_NEAR(this->parseNumber("1/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
811
812 } else {
813 EXPECT_FALSE(checker->canHandle(tasks[0]));
814 }
815 });
816#else
817 GTEST_SKIP();
818#endif
819}
820
821TYPED_TEST(DtmcPrctlModelCheckerTest, HOAProbabilitiesDie) {
822 // "P=? [(X s>0) U (s=7 & d=2)]"
823 std::string formulasString = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (s=7 & d=2) }]";
824 // "P=? [(X s>0) U (d=4 | d=2)]"
825 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (d=4 | d=2) }]";
826 // "P=? [ (F s=4) & (X \"three\")]"
827 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4), \"p1\" -> \"three\" }]";
828 // "P=? [ (F s=6) & (X \"done\")]"
829 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> \"done\" }]";
830 // "P=? [ (F s=6) & (X !\"done\")]"
831 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> !\"done\" }]";
832 // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]"
833 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]";
834 // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]"
835 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) }]";
836
837 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
838 auto model = std::move(modelFormulas.first);
839 auto tasks = this->getTasks(modelFormulas.second);
840 this->execute(model, [&]() {
841 EXPECT_EQ(13ul, model->getNumberOfStates());
842 EXPECT_EQ(20ul, model->getNumberOfTransitions());
843 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
844 auto checker = this->createModelChecker(model);
845 std::unique_ptr<storm::modelchecker::CheckResult> result;
846
847 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
848 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
849 result = checker->check(tasks[0]);
850 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
851
852 result = checker->check(tasks[1]);
853 EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
854
855 result = checker->check(tasks[2]);
856 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
857
858 result = checker->check(tasks[3]);
859 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
860
861 result = checker->check(tasks[4]);
862 EXPECT_NEAR(this->parseNumber("1/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
863
864 result = checker->check(tasks[5]);
865 EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
866
867 result = checker->check(tasks[6]);
868 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
869 } else {
870 EXPECT_FALSE(checker->canHandle(tasks[0]));
871 }
872 });
873}
874
875} // 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:332
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:13
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:530
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