Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LraCtmcCslModelCheckerTest.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/LongRunAverageSolverEnvironment.h"
14#include "storm/environment/solver/NativeSolverEnvironment.h"
15#include "storm/logic/Formulas.h"
16#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h"
17#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
18#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
19#include "storm/modelchecker/results/QualitativeCheckResult.h"
20#include "storm/modelchecker/results/QuantitativeCheckResult.h"
21#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
22#include "storm/models/sparse/Ctmc.h"
23#include "storm/models/sparse/StandardRewardModel.h"
24#include "storm/models/symbolic/Ctmc.h"
25#include "storm/models/symbolic/StandardRewardModel.h"
26#include "storm/settings/modules/CoreSettings.h"
27#include "storm/storage/dd/DdManager.h"
28#include "storm/storage/expressions/ExpressionManager.h"
29
30namespace {
31
32enum class CtmcEngine { PrismSparse, JaniSparse, JaniHybrid };
33
34#ifdef STORM_HAVE_GMM
35class GBSparseGmmxxGmresIluEnvironment {
36 public:
37 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
38 static const CtmcEngine engine = CtmcEngine::PrismSparse;
39 static const bool isExact = false;
40 typedef double ValueType;
41 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
42 static storm::Environment createEnvironment() {
43 storm::Environment env;
44 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
45 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
46 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
47 env.solver().gmmxx().setPrecision(
48 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
49 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
50 env.solver().lra().setPrecision(
51 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
52 return env;
53 }
54};
55
56class GBJaniSparseGmmxxGmresIluEnvironment {
57 public:
58 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
59 static const CtmcEngine engine = CtmcEngine::JaniSparse;
60 static const bool isExact = false;
61 typedef double ValueType;
62 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
63 static storm::Environment createEnvironment() {
64 storm::Environment env;
65 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
66 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
67 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
68 env.solver().gmmxx().setPrecision(
69 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
70 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
71 env.solver().lra().setPrecision(
72 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
73 return env;
74 }
75};
76
77class GBJaniHybridCuddGmmxxGmresEnvironment {
78 public:
79 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
80 static const CtmcEngine engine = CtmcEngine::JaniHybrid;
81 static const bool isExact = false;
82 typedef double ValueType;
83 typedef storm::models::symbolic::Ctmc<ddType, ValueType> ModelType;
84 static storm::Environment createEnvironment() {
85 storm::Environment env;
86 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
87 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
88 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
89 env.solver().gmmxx().setPrecision(
90 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
91 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
92 env.solver().lra().setPrecision(
93 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
94 return env;
95 }
96};
97
98class GBJaniHybridSylvanGmmxxGmresEnvironment {
99 public:
100 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
101 static const CtmcEngine engine = CtmcEngine::JaniHybrid;
102 static const bool isExact = false;
103 typedef double ValueType;
104 typedef storm::models::symbolic::Ctmc<ddType, ValueType> ModelType;
105 static storm::Environment createEnvironment() {
106 storm::Environment env;
107 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
108 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
109 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
110 env.solver().gmmxx().setPrecision(
111 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
112 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
113 env.solver().lra().setPrecision(
114 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
115 return env;
116 }
117};
118#endif
119
120class GBSparseEigenDGmresEnvironment {
121 public:
122 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
123 static const CtmcEngine engine = CtmcEngine::PrismSparse;
124 static const bool isExact = false;
125 typedef double ValueType;
126 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
127 static storm::Environment createEnvironment() {
128 storm::Environment env;
129 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
130 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
131 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
132 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
133 return env;
134 }
135};
136
137class GBSparseEigenDoubleLUEnvironment {
138 public:
139 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
140 static const CtmcEngine engine = CtmcEngine::PrismSparse;
141 static const bool isExact = false;
142 typedef double ValueType;
143 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
144 static storm::Environment createEnvironment() {
145 storm::Environment env;
146 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
147 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
148 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
149 return env;
150 }
151};
152
153class GBSparseNativeSorEnvironment {
154 public:
155 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
156 static const CtmcEngine engine = CtmcEngine::PrismSparse;
157 static const bool isExact = false;
158 typedef double ValueType;
159 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
160 static storm::Environment createEnvironment() {
161 storm::Environment env;
162 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
163 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
164 env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.7)); // LRA computation fails for 0.9
165 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
166 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-9));
167 return env;
168 }
169};
170
171#ifdef STORM_HAVE_GMM
172class DistrSparseGmmxxGmresIluEnvironment {
173 public:
174 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
175 static const CtmcEngine engine = CtmcEngine::PrismSparse;
176 static const bool isExact = false;
177 typedef double ValueType;
178 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
179 static storm::Environment createEnvironment() {
180 storm::Environment env;
181 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
182 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
183 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
184 env.solver().gmmxx().setPrecision(
185 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
186 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations);
187 env.solver().lra().setPrecision(
188 storm::utility::convertNumber<storm::RationalNumber>(1e-8)); // Need to increase precision because eq sys yields incorrect results
189 return env;
190 }
191};
192#endif
193
194class DistrSparseEigenDoubleLUEnvironment {
195 public:
196 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
197 static const CtmcEngine engine = CtmcEngine::PrismSparse;
198 static const bool isExact = false;
199 typedef double ValueType;
200 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
201 static storm::Environment createEnvironment() {
202 storm::Environment env;
203 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
204 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
205 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
206 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
207 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations);
208 return env;
209 }
210};
211
212class ValueIterationSparseEnvironment {
213 public:
214 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
215 static const CtmcEngine engine = CtmcEngine::PrismSparse;
216 static const bool isExact = false;
217 typedef double ValueType;
218 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
219 static storm::Environment createEnvironment() {
220 storm::Environment env;
221 env.solver().lra().setDetLraMethod(storm::solver::LraMethod::ValueIteration);
222 return env;
223 }
224};
225
226class SoundEnvironment {
227 public:
228 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
229 static const CtmcEngine engine = CtmcEngine::PrismSparse;
230 static const bool isExact = false;
231 typedef double ValueType;
232 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
233 static storm::Environment createEnvironment() {
234 storm::Environment env;
235 env.solver().setForceSoundness(true);
236 return env;
237 }
238};
239
240template<typename TestType>
241class LraCtmcCslModelCheckerTest : public ::testing::Test {
242 public:
243 typedef typename TestType::ValueType ValueType;
244 typedef typename storm::models::sparse::Ctmc<ValueType> SparseModelType;
245 typedef typename storm::models::symbolic::Ctmc<TestType::ddType, ValueType> SymbolicModelType;
246
247 LraCtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
248
249 void SetUp() override {
250#ifndef STORM_HAVE_Z3
251 GTEST_SKIP() << "Z3 not available.";
252#endif
253 }
254
255 storm::Environment const& env() const {
256 return _environment;
257 }
258 ValueType parseNumber(std::string const& input) const {
259 return storm::utility::convertNumber<ValueType>(input);
260 }
261 ValueType precision() const {
262 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
263 }
264 bool isSparseModel() const {
265 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
266 }
267 bool isSymbolicModel() const {
268 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
269 }
270 CtmcEngine getEngine() const {
271 return TestType::engine;
272 }
273
274 template<typename MT = typename TestType::ModelType>
275 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
276 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
277 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
278 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
279 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true);
280 program = storm::utility::prism::preprocess(program, constantDefinitionString);
281 if (TestType::engine == CtmcEngine::PrismSparse) {
282 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
283 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
284 } else if (TestType::engine == CtmcEngine::JaniSparse) {
285 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
286 janiData.first.substituteFunctions();
287 result.second = storm::api::extractFormulasFromProperties(janiData.second);
288 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
289 }
290 return result;
291 }
292
293 template<typename MT = typename TestType::ModelType>
294 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
295 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
296 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
297 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
298 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true);
299 program = storm::utility::prism::preprocess(program, constantDefinitionString);
300 if (TestType::engine == CtmcEngine::JaniHybrid) {
301 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
302 janiData.first.substituteFunctions();
303 result.second = storm::api::extractFormulasFromProperties(janiData.second);
304 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
305 }
306 return result;
307 }
308
309 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
310 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
311 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
312 for (auto const& f : formulas) {
313 result.emplace_back(*f);
314 }
315 return result;
316 }
317
318 template<typename MT = typename TestType::ModelType>
319 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
320 std::shared_ptr<MT> const& model) const {
321 if (TestType::engine == CtmcEngine::PrismSparse || TestType::engine == CtmcEngine::JaniSparse) {
322 return std::make_shared<storm::modelchecker::SparseCtmcCslModelChecker<SparseModelType>>(*model);
323 }
324 return nullptr;
325 }
326
327 template<typename MT = typename TestType::ModelType>
328 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
329 createModelChecker(std::shared_ptr<MT> const& model) const {
330 if (TestType::engine == CtmcEngine::JaniHybrid) {
331 return std::make_shared<storm::modelchecker::HybridCtmcCslModelChecker<SymbolicModelType>>(*model);
332 }
333 return nullptr;
334 }
335
336 template<typename MT = typename TestType::ModelType>
337 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
338 std::function<void()> const& f) const {
339 f();
340 }
341
342 template<typename MT = typename TestType::ModelType>
343 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
344 std::function<void()> const& f) const {
345 model->getManager().execute(f);
346 }
347
348 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
349 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
350 auto filter = getInitialStateFilter(model);
351 result->filter(*filter);
352 return result->asQualitativeCheckResult().forallTrue();
353 }
354
355 ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
356 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
357 auto filter = getInitialStateFilter(model);
358 result->filter(*filter);
359 return result->asQuantitativeCheckResult<ValueType>().getMin();
360 }
361
362 private:
363 storm::Environment _environment;
364
365 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
366 if (isSparseModel()) {
367 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
368 } else {
369 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
370 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
371 }
372 }
373};
374
375typedef ::testing::Types<
376#ifdef STORM_HAVE_GMM
377 GBSparseGmmxxGmresIluEnvironment, GBJaniSparseGmmxxGmresIluEnvironment, GBJaniHybridCuddGmmxxGmresEnvironment, GBJaniHybridSylvanGmmxxGmresEnvironment,
378 DistrSparseGmmxxGmresIluEnvironment,
379#endif
380 GBSparseEigenDGmresEnvironment, GBSparseEigenDoubleLUEnvironment, GBSparseNativeSorEnvironment, DistrSparseEigenDoubleLUEnvironment,
381 ValueIterationSparseEnvironment, SoundEnvironment>
382 TestingTypes;
383
384TYPED_TEST_SUITE(LraCtmcCslModelCheckerTest, TestingTypes, );
385
386TYPED_TEST(LraCtmcCslModelCheckerTest, Cluster) {
387 std::string formulasString = "LRA=? [\"minimum\"]";
388
389 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", formulasString);
390 auto model = std::move(modelFormulas.first);
391 auto tasks = this->getTasks(modelFormulas.second);
392 this->execute(model, [&]() {
393 EXPECT_EQ(276ul, model->getNumberOfStates());
394 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
395 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
396 auto checker = this->createModelChecker(model);
397 std::unique_ptr<storm::modelchecker::CheckResult> result;
398
399 result = checker->check(this->env(), tasks[0]);
400 EXPECT_NEAR(this->parseNumber("0.99999766034263426"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
401 });
402}
403
404TYPED_TEST(LraCtmcCslModelCheckerTest, Embedded) {
405 std::string formulasString = "LRA=? [\"fail_sensors\"]";
406
407 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString);
408 auto model = std::move(modelFormulas.first);
409 auto tasks = this->getTasks(modelFormulas.second);
410 this->execute(model, [&]() {
411 EXPECT_EQ(3478ul, model->getNumberOfStates());
412 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
413 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
414 auto checker = this->createModelChecker(model);
415 std::unique_ptr<storm::modelchecker::CheckResult> result;
416
417 result = checker->check(this->env(), tasks[0]);
418 EXPECT_NEAR(this->parseNumber("6201111489217/6635130141055"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
419 });
420}
421
422TYPED_TEST(LraCtmcCslModelCheckerTest, Polling) {
423 std::string formulasString = "LRA=?[\"target\"]";
424
425 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString);
426 auto model = std::move(modelFormulas.first);
427 auto tasks = this->getTasks(modelFormulas.second);
428 this->execute(model, [&]() {
429 EXPECT_EQ(12ul, model->getNumberOfStates());
430 EXPECT_EQ(22ul, model->getNumberOfTransitions());
431 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
432 auto checker = this->createModelChecker(model);
433 std::unique_ptr<storm::modelchecker::CheckResult> result;
434
435 result = checker->check(this->env(), tasks[0]);
436 EXPECT_NEAR(this->parseNumber("0.20079750055570736"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
437 });
438}
439
440TYPED_TEST(LraCtmcCslModelCheckerTest, Tandem) {
441 std::string formulasString = "LRA=? [\"first_queue_full\"]";
442
443 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", formulasString);
444 auto model = std::move(modelFormulas.first);
445 auto tasks = this->getTasks(modelFormulas.second);
446 this->execute(model, [&]() {
447 EXPECT_EQ(66ul, model->getNumberOfStates());
448 EXPECT_EQ(189ul, model->getNumberOfTransitions());
449 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
450 auto checker = this->createModelChecker(model);
451 std::unique_ptr<storm::modelchecker::CheckResult> result;
452
453 result = checker->check(this->env(), tasks[0]);
454 EXPECT_NEAR(this->parseNumber("0.9100373532"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
455 });
456}
457
458TYPED_TEST(LraCtmcCslModelCheckerTest, Rewards) {
459 std::string formulasString = "R=? [ LRA ]";
460
461 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/lrarewards.sm", formulasString);
462 auto model = std::move(modelFormulas.first);
463 auto tasks = this->getTasks(modelFormulas.second);
464 this->execute(model, [&]() {
465 EXPECT_EQ(4ul, model->getNumberOfStates());
466 EXPECT_EQ(6ul, model->getNumberOfTransitions());
467 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
468 auto checker = this->createModelChecker(model);
469 std::unique_ptr<storm::modelchecker::CheckResult> result;
470
471 result = checker->check(this->env(), tasks[0]);
472 EXPECT_NEAR(this->parseNumber("11/15"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
473 });
474}
475
476TYPED_TEST(LraCtmcCslModelCheckerTest, kanban) {
477 std::string formulasString = "R{\"throughput\"}=? [ LRA ]";
478
479 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/kanban.prism", formulasString);
480 auto model = std::move(modelFormulas.first);
481 auto tasks = this->getTasks(modelFormulas.second);
482 this->execute(model, [&]() {
483 EXPECT_EQ(160ul, model->getNumberOfStates());
484 EXPECT_EQ(616ul, model->getNumberOfTransitions());
485 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
486 auto checker = this->createModelChecker(model);
487 std::unique_ptr<storm::modelchecker::CheckResult> result;
488
489 result = checker->check(this->env(), tasks[0]);
490 EXPECT_NEAR(
491 this->parseNumber("1132372552133951639536770152429724263999896896549676426094918302160613340902023133969841067385167041200690481843915870926707"
492 "11590526535239899047608853509681914074220789038015289373871985431257486278/"
493 "1223067474012215838745994023624181143448435715858923491568712969277184634645504346456117443333632535902774869182827010789201"
494 "972713368729205674432492059242349591780604188152950845769793378621446766887"),
495 this->getQuantitativeResultAtInitialState(model, result), this->precision());
496 });
497}
498
499} // namespace
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::LongRunAverageSolverEnvironment::setDetLraMethod
void setDetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault=false)
Definition LongRunAverageSolverEnvironment.cpp:36
storm::NativeSolverEnvironment::setSorOmega
void setSorOmega(storm::RationalNumber const &value)
Definition NativeSolverEnvironment.cpp:84
storm::NativeSolverEnvironment::setMethod
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
Definition NativeSolverEnvironment.cpp:43
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::SolverEnvironment::lra
LongRunAverageSolverEnvironment & lra()
Definition SolverEnvironment.cpp:27
storm::models::sparse::Ctmc
This class represents a continuous-time Markov chain.
Definition Ctmc.h:14
storm::models::symbolic::Ctmc
This class represents a continuous-time Markov chain.
Definition Ctmc.h:14
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