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