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