Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DtmcPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-conv/api/storm-conv.h"
5#include "storm-parsers/api/model_descriptions.h"
6#include "storm-parsers/api/properties.h"
7#include "storm-parsers/parser/FormulaParser.h"
8#include "storm-parsers/parser/PrismParser.h"
9#include "storm/api/builder.h"
10#include "storm/api/properties.h"
11#include "storm/environment/solver/EigenSolverEnvironment.h"
12#include "storm/environment/solver/GmmxxSolverEnvironment.h"
13#include "storm/environment/solver/NativeSolverEnvironment.h"
14#include "storm/environment/solver/TopologicalSolverEnvironment.h"
15#include "storm/logic/Formulas.h"
16#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
17#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
18#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
19#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
20#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
21#include "storm/modelchecker/results/QualitativeCheckResult.h"
22#include "storm/modelchecker/results/QuantitativeCheckResult.h"
23#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
24#include "storm/models/sparse/Dtmc.h"
25#include "storm/models/sparse/StandardRewardModel.h"
26#include "storm/models/symbolic/Dtmc.h"
27#include "storm/models/symbolic/StandardRewardModel.h"
28#include "storm/settings/modules/CoreSettings.h"
29#include "storm/solver/EigenLinearEquationSolver.h"
30#include "storm/storage/expressions/ExpressionManager.h"
31
32namespace {
33
34enum class DtmcEngine { PrismSparse, JaniSparse, Hybrid, PrismDd, JaniDd };
35
36class SparseGmmxxGmresIluEnvironment {
37 public:
38 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
39 static const DtmcEngine engine = DtmcEngine::PrismSparse;
40 static const bool isExact = false;
41 typedef double ValueType;
42 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
43 static storm::Environment createEnvironment() {
44 storm::Environment env;
45 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
46 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
47 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
48 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
49 return env;
50 }
51};
52
53class JaniSparseGmmxxGmresIluEnvironment {
54 public:
55 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
56 static const DtmcEngine engine = DtmcEngine::JaniSparse;
57 static const bool isExact = false;
58 typedef double ValueType;
59 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
60 static storm::Environment createEnvironment() {
61 storm::Environment env;
62 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
63 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
64 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
65 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
66 return env;
67 }
68};
69
70class SparseGmmxxGmresDiagEnvironment {
71 public:
72 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
73 static const DtmcEngine engine = DtmcEngine::PrismSparse;
74 static const bool isExact = false;
75 typedef double ValueType;
76 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
77 static storm::Environment createEnvironment() {
78 storm::Environment env;
79 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
80 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
81 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
82 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
83 return env;
84 }
85};
86
87class SparseGmmxxBicgstabIluEnvironment {
88 public:
89 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
90 static const DtmcEngine engine = DtmcEngine::PrismSparse;
91 static const bool isExact = false;
92 typedef double ValueType;
93 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
94 static storm::Environment createEnvironment() {
95 storm::Environment env;
96 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
97 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
98 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
99 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
100 return env;
101 }
102};
103
104class SparseEigenDGmresEnvironment {
105 public:
106 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
107 static const DtmcEngine engine = DtmcEngine::PrismSparse;
108 static const bool isExact = false;
109 typedef double ValueType;
110 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
111 static storm::Environment createEnvironment() {
112 storm::Environment env;
113 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
114 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
115 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
116 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
117 return env;
118 }
119};
120
121class SparseEigenDoubleLUEnvironment {
122 public:
123 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
124 static const DtmcEngine engine = DtmcEngine::PrismSparse;
125 static const bool isExact = false;
126 typedef double ValueType;
127 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
128 static storm::Environment createEnvironment() {
129 storm::Environment env;
130 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
131 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
132 return env;
133 }
134};
135
136class SparseEigenRationalLUEnvironment {
137 public:
138 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
139 static const DtmcEngine engine = DtmcEngine::PrismSparse;
140 static const bool isExact = true;
141 typedef storm::RationalNumber ValueType;
142 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
143 static storm::Environment createEnvironment() {
144 storm::Environment env;
145 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
146 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
147 return env;
148 }
149};
150
151class SparseRationalEliminationEnvironment {
152 public:
153 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
154 static const DtmcEngine engine = DtmcEngine::PrismSparse;
155 static const bool isExact = true;
156 typedef storm::RationalNumber ValueType;
157 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
158 static storm::Environment createEnvironment() {
159 storm::Environment env;
160 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
161 return env;
162 }
163};
164
165class SparseNativeJacobiEnvironment {
166 public:
167 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
168 static const DtmcEngine engine = DtmcEngine::PrismSparse;
169 static const bool isExact = false;
170 typedef double ValueType;
171 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
172 static storm::Environment createEnvironment() {
173 storm::Environment env;
174 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
175 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
176 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
177 return env;
178 }
179};
180
181class SparseNativeWalkerChaeEnvironment {
182 public:
183 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
184 static const DtmcEngine engine = DtmcEngine::PrismSparse;
185 static const bool isExact = false;
186 typedef double ValueType;
187 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
188 static storm::Environment createEnvironment() {
189 storm::Environment env;
190 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
191 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
192 env.solver().native().setMaximalNumberOfIterations(1000000);
193 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-7));
194 return env;
195 }
196};
197
198class SparseNativeSorEnvironment {
199 public:
200 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
201 static const DtmcEngine engine = DtmcEngine::PrismSparse;
202 static const bool isExact = false;
203 typedef double ValueType;
204 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
205 static storm::Environment createEnvironment() {
206 storm::Environment env;
207 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
208 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
209 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
210 return env;
211 }
212};
213
214class SparseNativePowerEnvironment {
215 public:
216 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
217 static const DtmcEngine engine = DtmcEngine::PrismSparse;
218 static const bool isExact = false;
219 typedef double ValueType;
220 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
221 static storm::Environment createEnvironment() {
222 storm::Environment env;
223 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
224 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
225 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
226 return env;
227 }
228};
229
230class SparseNativeSoundValueIterationEnvironment {
231 public:
232 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
233 static const DtmcEngine engine = DtmcEngine::PrismSparse;
234 static const bool isExact = false;
235 typedef double ValueType;
236 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
237 static storm::Environment createEnvironment() {
238 storm::Environment env;
239 env.solver().setForceSoundness(true);
240 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
241 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration);
242 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
243 return env;
244 }
245};
246
247class SparseNativeOptimisticValueIterationEnvironment {
248 public:
249 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
250 static const DtmcEngine engine = DtmcEngine::PrismSparse;
251 static const bool isExact = false;
252 typedef double ValueType;
253 typedef storm::models::sparse::Dtmc<ValueType> ModelType;
254 static storm::Environment createEnvironment() {
255 storm::Environment env;
256 env.solver().setForceSoundness(true);
257 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
258 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration);
259 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
260 return env;
261 }
262};
263
264class 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<
576#ifdef STORM_HAVE_GMM
577 SparseGmmxxGmresIluEnvironment, JaniSparseGmmxxGmresIluEnvironment, SparseGmmxxGmresDiagEnvironment, SparseGmmxxBicgstabIluEnvironment,
578 HybridSylvanGmmxxGmresEnvironment,
579#endif
580 SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment, SparseEigenRationalLUEnvironment, SparseRationalEliminationEnvironment,
581 SparseNativeJacobiEnvironment, SparseNativeWalkerChaeEnvironment, SparseNativeSorEnvironment, SparseNativePowerEnvironment,
582 SparseNativeSoundValueIterationEnvironment, SparseNativeOptimisticValueIterationEnvironment, SparseNativeIntervalIterationEnvironment,
583 SparseNativeRationalSearchEnvironment, SparseTopologicalEigenLUEnvironment, HybridCuddNativeJacobiEnvironment,
584 HybridCuddNativeSoundValueIterationEnvironment, HybridSylvanNativeRationalSearchEnvironment, DdSylvanNativePowerEnvironment,
585 JaniDdSylvanNativePowerEnvironment, DdCuddNativeJacobiEnvironment, DdSylvanRationalSearchEnvironment>
586 TestingTypes;
587
588TYPED_TEST_SUITE(DtmcPrctlModelCheckerTest, TestingTypes, );
589
590TYPED_TEST(DtmcPrctlModelCheckerTest, Die) {
591 std::string formulasString = "P=? [F \"one\"]";
592 formulasString += "; P=? [F \"two\"]";
593 formulasString += "; P=? [F \"three\"]";
594 formulasString += "; R=? [F \"done\"]";
595
596 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
597 auto model = std::move(modelFormulas.first);
598 auto tasks = this->getTasks(modelFormulas.second);
599 this->execute(model, [&]() {
600 EXPECT_EQ(13ul, model->getNumberOfStates());
601 EXPECT_EQ(20ul, model->getNumberOfTransitions());
602 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
603 auto checker = this->createModelChecker(model);
604 std::unique_ptr<storm::modelchecker::CheckResult> result;
605
606 result = checker->check(this->env(), tasks[0]);
607 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
608
609 result = checker->check(this->env(), tasks[1]);
610 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
611
612 result = checker->check(this->env(), tasks[2]);
613 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
614
615 result = checker->check(this->env(), tasks[3]);
616 EXPECT_NEAR(this->parseNumber("11/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
617 });
618}
619
620TYPED_TEST(DtmcPrctlModelCheckerTest, Crowds) {
621 std::string formulasString = "P=? [F observe0>1]";
622 formulasString += "; P=? [F \"observeIGreater1\"]";
623 formulasString += "; P=? [F observe1>1]";
624
625 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", formulasString);
626 auto model = std::move(modelFormulas.first);
627 auto tasks = this->getTasks(modelFormulas.second);
628 this->execute(model, [&]() {
629 EXPECT_EQ(726ul, model->getNumberOfStates());
630 EXPECT_EQ(1146ul, model->getNumberOfTransitions());
631 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
632 auto checker = this->createModelChecker(model);
633 std::unique_ptr<storm::modelchecker::CheckResult> result;
634
635 result = checker->check(this->env(), tasks[0]);
636 EXPECT_NEAR(this->parseNumber("78686542099694893/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
637
638 result = checker->check(this->env(), tasks[1]);
639 EXPECT_NEAR(this->parseNumber("40300855878315123/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
640
641 result = checker->check(this->env(), tasks[2]);
642 EXPECT_NEAR(this->parseNumber("13433618626105041/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
643 });
644}
645
646TYPED_TEST(DtmcPrctlModelCheckerTest, SynchronousLeader) {
647 std::string formulasString = "P=? [F \"elected\"]";
648 formulasString += "; P=? [F<=5 \"elected\"]";
649 formulasString += "; R=? [F \"elected\"]";
650
651 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
652 auto model = std::move(modelFormulas.first);
653 auto tasks = this->getTasks(modelFormulas.second);
654 this->execute(model, [&]() {
655 EXPECT_EQ(273ul, model->getNumberOfStates());
656 EXPECT_EQ(397ul, model->getNumberOfTransitions());
657 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
658 auto checker = this->createModelChecker(model);
659 std::unique_ptr<storm::modelchecker::CheckResult> result;
660
661 result = checker->check(this->env(), tasks[0]);
662 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
663
664 result = checker->check(this->env(), tasks[1]);
665 EXPECT_NEAR(this->parseNumber("24/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
666
667 result = checker->check(this->env(), tasks[2]);
668 EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
669 });
670}
671
672TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) {
673#ifndef STORM_HAVE_Z3
674 GTEST_SKIP() << "Z3 not available.";
675#endif
676 std::string formulasString = "P=? [F \"one\"]";
677 formulasString += "; P=? [F \"two\"]";
678 formulasString += "; P=? [F \"three\"]";
679
680 storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
681 auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
682 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, double>> tasks;
683 for (auto const& f : formulas) {
684 tasks.emplace_back(*f);
685 }
686 auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::Dtmc<double>>();
687 EXPECT_EQ(13ul, model->getNumberOfStates());
688 EXPECT_EQ(20ul, model->getNumberOfTransitions());
689
690 storm::storage::SparseMatrix<double> matrix = model->getTransitionMatrix();
691 storm::storage::BitVector initialStates(13);
692 initialStates.set(0);
693 storm::storage::BitVector phiStates(13);
694 storm::storage::BitVector psiStates(13);
695 psiStates.set(7);
696 psiStates.set(8);
697 psiStates.set(9);
698 psiStates.set(10);
699 psiStates.set(11);
700 psiStates.set(12);
701 storm::Environment env;
702 storm::solver::SolveGoal<double> goal(*model, tasks[0]);
703 std::vector<double> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix,
704 initialStates, phiStates, psiStates);
705
706 EXPECT_NEAR(1.0 / 6, result[7], 1e-6);
707 EXPECT_NEAR(1.0 / 6, result[8], 1e-6);
708 EXPECT_NEAR(1.0 / 6, result[9], 1e-6);
709 EXPECT_NEAR(1.0 / 6, result[10], 1e-6);
710 EXPECT_NEAR(1.0 / 6, result[11], 1e-6);
711 EXPECT_NEAR(1.0 / 6, result[12], 1e-6);
712
713 phiStates.set(6);
714 psiStates.set(1);
715 result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates,
716 psiStates);
717
718 EXPECT_NEAR(1, result[0], 1e-6);
719 EXPECT_NEAR(0.5, result[1], 1e-6);
720 EXPECT_NEAR(0.5, result[2], 1e-6);
721 EXPECT_NEAR(0.25, result[5], 1e-6);
722 EXPECT_NEAR(0, result[7], 1e-6);
723 EXPECT_NEAR(0, result[8], 1e-6);
724 EXPECT_NEAR(0, result[9], 1e-6);
725 EXPECT_NEAR(0.125, result[10], 1e-6);
726 EXPECT_NEAR(0.125, result[11], 1e-6);
727 EXPECT_NEAR(0, result[12], 1e-6);
728}
729
730TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesDie) {
731#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
732 std::string formulasString = "P=? [(X s>0) U (s=7 & d=2)]";
733 formulasString += "; P=? [ X (((s=1) U (s=3)) U (s=7))]";
734 formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]";
735 formulasString += "; P=? [ F (s=3 U (\"three\"))]";
736 formulasString += "; P=? [ F s=3 U (\"three\")]";
737 formulasString += "; P=? [ F (s=6) & X \"done\"]";
738 formulasString += "; P=? [ (F s=6) & (X \"done\")]";
739
740 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
741 auto model = std::move(modelFormulas.first);
742 auto tasks = this->getTasks(modelFormulas.second);
743 this->execute(model, [&]() {
744 EXPECT_EQ(13ul, model->getNumberOfStates());
745 EXPECT_EQ(20ul, model->getNumberOfTransitions());
746 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
747 auto checker = this->createModelChecker(model);
748 std::unique_ptr<storm::modelchecker::CheckResult> result;
749
750 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
751 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
752 result = checker->check(tasks[0]);
753 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
754
755 result = checker->check(tasks[1]);
756 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
757
758 result = checker->check(tasks[2]);
759 EXPECT_NEAR(this->parseNumber("1/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
760
761 result = checker->check(tasks[3]);
762 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
763
764 result = checker->check(tasks[4]);
765 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
766
767 result = checker->check(tasks[5]);
768 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
769
770 result = checker->check(tasks[6]);
771 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
772 } else {
773 EXPECT_FALSE(checker->canHandle(tasks[0]));
774 }
775 });
776#else
777 GTEST_SKIP();
778#endif
779}
780
781TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesSynchronousLeader) {
782#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
783 std::string formulasString = "P=? [X (u1=true U \"elected\")]";
784 formulasString += "; P=? [X !(u1=true U \"elected\")]";
785 formulasString += "; P=? [X v1=2 & X v1=1]";
786 formulasString += "; P=? [(X v1=2) & (X v1=1)]";
787 formulasString += "; P=? [(!X v1=2) & (X v1=1)]";
788
789 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
790 auto model = std::move(modelFormulas.first);
791 auto tasks = this->getTasks(modelFormulas.second);
792 this->execute(model, [&]() {
793 EXPECT_EQ(273ul, model->getNumberOfStates());
794 EXPECT_EQ(397ul, model->getNumberOfTransitions());
795 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
796 auto checker = this->createModelChecker(model);
797 std::unique_ptr<storm::modelchecker::CheckResult> result;
798
799 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
800 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
801 result = checker->check(tasks[0]);
802 EXPECT_NEAR(this->parseNumber("16/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
803
804 result = checker->check(tasks[1]);
805 EXPECT_NEAR(this->parseNumber("9/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
806
807 result = checker->check(tasks[2]);
808 EXPECT_NEAR(this->parseNumber("1/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
809
810 result = checker->check(tasks[3]);
811 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
812
813 result = checker->check(tasks[4]);
814 EXPECT_NEAR(this->parseNumber("1/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
815
816 } else {
817 EXPECT_FALSE(checker->canHandle(tasks[0]));
818 }
819 });
820#else
821 GTEST_SKIP();
822#endif
823}
824
825TYPED_TEST(DtmcPrctlModelCheckerTest, HOAProbabilitiesDie) {
826 // "P=? [(X s>0) U (s=7 & d=2)]"
827 std::string formulasString = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (s=7 & d=2) }]";
828 // "P=? [(X s>0) U (d=4 | d=2)]"
829 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (d=4 | d=2) }]";
830 // "P=? [ (F s=4) & (X \"three\")]"
831 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4), \"p1\" -> \"three\" }]";
832 // "P=? [ (F s=6) & (X \"done\")]"
833 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> \"done\" }]";
834 // "P=? [ (F s=6) & (X !\"done\")]"
835 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> !\"done\" }]";
836 // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]"
837 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]";
838 // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]"
839 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) }]";
840
841 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
842 auto model = std::move(modelFormulas.first);
843 auto tasks = this->getTasks(modelFormulas.second);
844 this->execute(model, [&]() {
845 EXPECT_EQ(13ul, model->getNumberOfStates());
846 EXPECT_EQ(20ul, model->getNumberOfTransitions());
847 ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
848 auto checker = this->createModelChecker(model);
849 std::unique_ptr<storm::modelchecker::CheckResult> result;
850
851 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
852 if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse) {
853 result = checker->check(tasks[0]);
854 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
855
856 result = checker->check(tasks[1]);
857 EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
858
859 result = checker->check(tasks[2]);
860 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
861
862 result = checker->check(tasks[3]);
863 EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
864
865 result = checker->check(tasks[4]);
866 EXPECT_NEAR(this->parseNumber("1/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
867
868 result = checker->check(tasks[5]);
869 EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
870
871 result = checker->check(tasks[6]);
872 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
873 } else {
874 EXPECT_FALSE(checker->canHandle(tasks[0]));
875 }
876 });
877}
878
879} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
getInitialStateFilter
std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model)
Definition RobustMdpPrctlModelCheckerTest.cpp:18
getQuantitativeResultAtInitialState
double getQuantitativeResultAtInitialState(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
Definition RobustMdpPrctlModelCheckerTest.cpp:27
storm::EigenSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition EigenSolverEnvironment.cpp:70
storm::EigenSolverEnvironment::setPreconditioner
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
Definition EigenSolverEnvironment.cpp:46
storm::EigenSolverEnvironment::setMethod
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
Definition EigenSolverEnvironment.cpp:37
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::GmmxxSolverEnvironment::setMethod
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
Definition GmmxxSolverEnvironment.cpp:32
storm::GmmxxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition GmmxxSolverEnvironment.cpp:64
storm::GmmxxSolverEnvironment::setPreconditioner
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
Definition GmmxxSolverEnvironment.cpp:40
storm::NativeSolverEnvironment::setMaximalNumberOfIterations
void setMaximalNumberOfIterations(uint64_t value)
Definition NativeSolverEnvironment.cpp:52
storm::NativeSolverEnvironment::setMethod
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
Definition NativeSolverEnvironment.cpp:43
storm::NativeSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition NativeSolverEnvironment.cpp:60
storm::SolverEnvironment::topological
TopologicalSolverEnvironment & topological()
Definition SolverEnvironment.cpp:91
storm::SolverEnvironment::setLinearEquationSolverType
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
Definition SolverEnvironment.cpp:127
storm::SolverEnvironment::eigen
EigenSolverEnvironment & eigen()
Definition SolverEnvironment.cpp:59
storm::SolverEnvironment::native
NativeSolverEnvironment & native()
Definition SolverEnvironment.cpp:75
storm::SolverEnvironment::gmmxx
GmmxxSolverEnvironment & gmmxx()
Definition SolverEnvironment.cpp:67
storm::TopologicalSolverEnvironment::setUnderlyingEquationSolverType
void setUnderlyingEquationSolverType(storm::solver::EquationSolverType value)
Definition TopologicalSolverEnvironment.cpp:33
storm::modelchecker::helper::SparseDtmcPrctlHelper::computeAllUntilProbabilities
static std::vector< ValueType > computeAllUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition SparseDtmcPrctlHelper.cpp:247
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:15
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:331
model_descriptions.h
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::api::convertPrismToJani
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > convertPrismToJani(storm::prism::Program const &program, storm::converter::PrismToJaniConverterOptions options)
Definition storm-conv.cpp:111
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:53
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
storm::utility::vector::filter
storm::storage::BitVector filter(std::vector< T > const &values, std::function< bool(T const &value)> const &function)
Retrieves a bit vector containing all the indices for which the value at this position makes the give...
Definition vector.h:490
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h