Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
CtmcCslModelCheckerTest.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/api/builder.h"
8#include "storm/api/properties.h"
9#include "storm/environment/solver/EigenSolverEnvironment.h"
10#include "storm/environment/solver/GmmxxSolverEnvironment.h"
11#include "storm/environment/solver/NativeSolverEnvironment.h"
12#include "storm/logic/Formulas.h"
13#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h"
14#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
15#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
16#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
17#include "storm/modelchecker/results/QualitativeCheckResult.h"
18#include "storm/modelchecker/results/QuantitativeCheckResult.h"
19#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
20#include "storm/models/sparse/Ctmc.h"
21#include "storm/models/sparse/StandardRewardModel.h"
22#include "storm/models/symbolic/Ctmc.h"
23#include "storm/models/symbolic/StandardRewardModel.h"
24#include "storm/settings/modules/CoreSettings.h"
25#include "storm/solver/EigenLinearEquationSolver.h"
26#include "storm/storage/dd/DdManager.h"
27#include "storm/storage/expressions/ExpressionManager.h"
28
29namespace {
30
31enum class CtmcEngine { PrismSparse, JaniSparse, PrismHybrid, JaniHybrid };
32
33class SparseGmmxxGmresIluEnvironment {
34 public:
35 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
36 static const CtmcEngine engine = CtmcEngine::PrismSparse;
37 static const bool isExact = false;
38 typedef double ValueType;
39 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
40 static storm::Environment createEnvironment() {
41 storm::Environment env;
42 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
43 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
44 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
45 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
46 return env;
47 }
48};
49
50class JaniSparseGmmxxGmresIluEnvironment {
51 public:
52 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
53 static const CtmcEngine engine = CtmcEngine::JaniSparse;
54 static const bool isExact = false;
55 typedef double ValueType;
56 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
57 static storm::Environment createEnvironment() {
58 storm::Environment env;
59 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
60 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
61 env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
62 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
63 return env;
64 }
65};
66
67class SparseEigenDGmresEnvironment {
68 public:
69 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
70 static const CtmcEngine engine = CtmcEngine::PrismSparse;
71 static const bool isExact = false;
72 typedef double ValueType;
73 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
74 static storm::Environment createEnvironment() {
75 storm::Environment env;
76 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
77 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
78 env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
79 env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
80 return env;
81 }
82};
83
84class SparseEigenDoubleLUEnvironment {
85 public:
86 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
87 static const CtmcEngine engine = CtmcEngine::PrismSparse;
88 static const bool isExact = false;
89 typedef double ValueType;
90 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
91 static storm::Environment createEnvironment() {
92 storm::Environment env;
93 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
94 env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
95 return env;
96 }
97};
98
99class SparseNativeSorEnvironment {
100 public:
101 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
102 static const CtmcEngine engine = CtmcEngine::PrismSparse;
103 static const bool isExact = false;
104 typedef double ValueType;
105 typedef storm::models::sparse::Ctmc<ValueType> ModelType;
106 static storm::Environment createEnvironment() {
107 storm::Environment env;
108 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
109 env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
110 env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-9));
111 env.solver().native().setRelativeTerminationCriterion(false);
112 env.solver().native().setMaximalNumberOfIterations(5000000);
113 return env;
114 }
115};
116
117class HybridCuddGmmxxGmresEnvironment {
118 public:
119 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
120 static const CtmcEngine engine = CtmcEngine::PrismHybrid;
121 static const bool isExact = false;
122 typedef double ValueType;
123 typedef storm::models::symbolic::Ctmc<ddType, ValueType> ModelType;
124 static storm::Environment createEnvironment() {
125 storm::Environment env;
126 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
127 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
128 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
129 return env;
130 }
131};
132
133class JaniHybridCuddGmmxxGmresEnvironment {
134 public:
135 static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
136 static const CtmcEngine engine = CtmcEngine::JaniHybrid;
137 static const bool isExact = false;
138 typedef double ValueType;
139 typedef storm::models::symbolic::Ctmc<ddType, ValueType> ModelType;
140 static storm::Environment createEnvironment() {
141 storm::Environment env;
142 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
143 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
144 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
145 return env;
146 }
147};
148
149class HybridSylvanGmmxxGmresEnvironment {
150 public:
151 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
152 static const CtmcEngine engine = CtmcEngine::PrismHybrid;
153 static const bool isExact = false;
154 typedef double ValueType;
155 typedef storm::models::symbolic::Ctmc<ddType, ValueType> ModelType;
156 static storm::Environment createEnvironment() {
157 storm::Environment env;
158 env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
159 env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
160 env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
161 return env;
162 }
163};
164
165template<typename TestType>
166class CtmcCslModelCheckerTest : public ::testing::Test {
167 public:
168 typedef typename TestType::ValueType ValueType;
169 typedef typename storm::models::sparse::Ctmc<ValueType> SparseModelType;
170 typedef typename storm::models::symbolic::Ctmc<TestType::ddType, ValueType> SymbolicModelType;
171
172 CtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
173
174 void SetUp() override {
175#ifndef STORM_HAVE_Z3
176 GTEST_SKIP() << "Z3 not available.";
177#endif
178 }
179
180 storm::Environment const& env() const {
181 return _environment;
182 }
183 ValueType parseNumber(std::string const& input) const {
184 return storm::utility::convertNumber<ValueType>(input);
185 }
186 ValueType precision() const {
187 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
188 }
189 bool isSparseModel() const {
190 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
191 }
192 bool isSymbolicModel() const {
193 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
194 }
195 CtmcEngine getEngine() const {
196 return TestType::engine;
197 }
198
199 template<typename MT = typename TestType::ModelType>
200 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
201 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
202 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
203 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
204 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true);
205 program = storm::utility::prism::preprocess(program, constantDefinitionString);
206 if (TestType::engine == CtmcEngine::PrismSparse) {
207 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
208 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
209 } else if (TestType::engine == CtmcEngine::JaniSparse) {
210 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
211 janiData.first.substituteFunctions();
212 result.second = storm::api::extractFormulasFromProperties(janiData.second);
213 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
214 }
215 return result;
216 }
217
218 template<typename MT = typename TestType::ModelType>
219 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
220 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
221 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
222 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
223 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true);
224 program = storm::utility::prism::preprocess(program, constantDefinitionString);
225 if (TestType::engine == CtmcEngine::PrismHybrid) {
226 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
227 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
228 } else if (TestType::engine == CtmcEngine::JaniHybrid) {
229 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
230 janiData.first.substituteFunctions();
231 result.second = storm::api::extractFormulasFromProperties(janiData.second);
232 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
233 }
234 return result;
235 }
236
237 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
238 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
239 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
240 for (auto const& f : formulas) {
241 result.emplace_back(*f);
242 }
243 return result;
244 }
245
246 template<typename MT = typename TestType::ModelType>
247 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
248 std::shared_ptr<MT> const& model) const {
249 if (TestType::engine == CtmcEngine::PrismSparse || TestType::engine == CtmcEngine::JaniSparse) {
250 return std::make_shared<storm::modelchecker::SparseCtmcCslModelChecker<SparseModelType>>(*model);
251 }
252 }
253
254 template<typename MT = typename TestType::ModelType>
255 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
256 createModelChecker(std::shared_ptr<MT> const& model) const {
257 if (TestType::engine == CtmcEngine::PrismHybrid || TestType::engine == CtmcEngine::JaniHybrid) {
258 return std::make_shared<storm::modelchecker::HybridCtmcCslModelChecker<SymbolicModelType>>(*model);
259 }
260 }
261
262 template<typename MT = typename TestType::ModelType>
263 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
264 std::function<void()> const& f) const {
265 f();
266 }
267
268 template<typename MT = typename TestType::ModelType>
269 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
270 std::function<void()> const& f) const {
271 model->getManager().execute(f);
272 }
273
274 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
275 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
276 auto filter = getInitialStateFilter(model);
277 result->filter(*filter);
278 return result->asQualitativeCheckResult().forallTrue();
279 }
280
281 ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
282 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
283 auto filter = getInitialStateFilter(model);
284 result->filter(*filter);
285 return result->asQuantitativeCheckResult<ValueType>().getMin();
286 }
287
288 private:
289 storm::Environment _environment;
290
291 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
292 if (isSparseModel()) {
293 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
294 } else {
295 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
296 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
297 }
298 }
299};
300
301typedef ::testing::Types<
302#ifdef STORM_HAVE_GMM
303 SparseGmmxxGmresIluEnvironment, JaniSparseGmmxxGmresIluEnvironment, HybridCuddGmmxxGmresEnvironment, JaniHybridCuddGmmxxGmresEnvironment,
304 HybridSylvanGmmxxGmresEnvironment,
305#endif
306 SparseNativeSorEnvironment, SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment>
307 TestingTypes;
308
309TYPED_TEST_SUITE(CtmcCslModelCheckerTest, TestingTypes, );
310
311TYPED_TEST(CtmcCslModelCheckerTest, Cluster) {
312 std::string formulasString = "P=? [ F<=100 !\"minimum\"]";
313 formulasString += "; P=? [ F[100,100] !\"minimum\"]";
314 formulasString += "; P=? [ F[100,2000] !\"minimum\"]";
315 formulasString += "; P=? [ \"minimum\" U<=10 \"premium\"]";
316 formulasString += "; P=? [ !\"minimum\" U>=1 \"minimum\"]";
317 formulasString += "; P=? [ \"minimum\" U>=1 !\"minimum\"]";
318 formulasString += "; R=? [C<=100]";
319
320 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", formulasString);
321 auto model = std::move(modelFormulas.first);
322 auto tasks = this->getTasks(modelFormulas.second);
323 this->execute(model, [&]() {
324 EXPECT_EQ(276ul, model->getNumberOfStates());
325 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
326 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
327 auto checker = this->createModelChecker(model);
328 std::unique_ptr<storm::modelchecker::CheckResult> result;
329
330 result = checker->check(this->env(), tasks[0]);
331 EXPECT_NEAR(this->parseNumber("5.5461254704419085E-5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
332
333 result = checker->check(this->env(), tasks[1]);
334 EXPECT_NEAR(this->parseNumber("2.3397873548343415E-6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
335
336 result = checker->check(this->env(), tasks[2]);
337 EXPECT_NEAR(this->parseNumber("0.001105335651670241"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
338
339 result = checker->check(this->env(), tasks[3]);
340 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
341
342 result = checker->check(this->env(), tasks[4]);
343 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
344
345 result = checker->check(this->env(), tasks[5]);
346 EXPECT_NEAR(this->parseNumber("0.9999999033633374"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
347
348 result = checker->check(this->env(), tasks[6]);
349 EXPECT_NEAR(this->parseNumber("0.8602815057967503"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
350 });
351}
352
353TYPED_TEST(CtmcCslModelCheckerTest, Embedded) {
354 std::string formulasString = "P=? [ F<=10000 \"down\"]";
355 formulasString += "; P=? [ !\"down\" U<=10000 \"fail_actuators\"]";
356 formulasString += "; P=? [ !\"down\" U<=10000 \"fail_io\"]";
357 formulasString += "; P=? [ !\"down\" U<=10000 \"fail_sensors\"]";
358 formulasString += "; R{\"up\"}=? [C<=10000]";
359
360 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString);
361 auto model = std::move(modelFormulas.first);
362 auto tasks = this->getTasks(modelFormulas.second);
363 this->execute(model, [&]() {
364 EXPECT_EQ(3478ul, model->getNumberOfStates());
365 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
366 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
367 auto checker = this->createModelChecker(model);
368 std::unique_ptr<storm::modelchecker::CheckResult> result;
369
370 result = checker->check(this->env(), tasks[0]);
371 EXPECT_NEAR(this->parseNumber("0.0019216435246119591"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
372
373 result = checker->check(this->env(), tasks[1]);
374 EXPECT_NEAR(this->parseNumber("3.7079151806696567E-6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
375
376 result = checker->check(this->env(), tasks[2]);
377 EXPECT_NEAR(this->parseNumber("0.001556839327673734"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
378
379 result = checker->check(this->env(), tasks[3]);
380 EXPECT_NEAR(this->parseNumber("4.429620626755424E-5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
381
382 result = checker->check(this->env(), tasks[4]);
383 EXPECT_NEAR(this->parseNumber("2.7745274082080154"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
384 });
385}
386
387TYPED_TEST(CtmcCslModelCheckerTest, Tandem) {
388 std::string formulasString = "P=? [ F<=10 \"network_full\" ]";
389 formulasString += "; P=? [ F<=10 \"first_queue_full\" ]";
390 formulasString += "; P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]";
391 formulasString += "; R=? [I=10]";
392 formulasString += "; R=? [C<=10]";
393 formulasString += "; R=? [F \"first_queue_full\"&\"second_queue_full\"]";
394
395 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", formulasString);
396 auto model = std::move(modelFormulas.first);
397 auto tasks = this->getTasks(modelFormulas.second);
398 this->execute(model, [&]() {
399 EXPECT_EQ(66ul, model->getNumberOfStates());
400 EXPECT_EQ(189ul, model->getNumberOfTransitions());
401 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
402 auto checker = this->createModelChecker(model);
403 std::unique_ptr<storm::modelchecker::CheckResult> result;
404
405 result = checker->check(this->env(), tasks[0]);
406 EXPECT_NEAR(this->parseNumber("0.015446370562428037"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
407
408 result = checker->check(this->env(), tasks[1]);
409 EXPECT_NEAR(this->parseNumber("0.999999837225515"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
410
411 result = checker->check(this->env(), tasks[2]);
412 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
413
414 result = checker->check(this->env(), tasks[3]);
415 EXPECT_NEAR(this->parseNumber("5.679243850315877"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
416
417 result = checker->check(this->env(), tasks[4]);
418 EXPECT_NEAR(this->parseNumber("55.44792186036232"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
419
420 result = checker->check(this->env(), tasks[5]);
421 EXPECT_NEAR(this->parseNumber("262.85103824276308"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
422 });
423}
424
425TYPED_TEST(CtmcCslModelCheckerTest, simple1) {
426 std::string formulasString = "P=? [ F<=0.5 x=1 ]";
427 formulasString += "; R=? [ C<=0.1 ]";
428 formulasString += "; R=? [ C<=1 ]";
429 formulasString += "; R=? [ C<=10 ]";
430
431 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/simple1.sm", formulasString);
432 auto model = std::move(modelFormulas.first);
433 auto tasks = this->getTasks(modelFormulas.second);
434 this->execute(model, [&]() {
435 EXPECT_EQ(2ul, model->getNumberOfStates());
436 EXPECT_EQ(2ul, model->getNumberOfTransitions());
437 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
438 auto checker = this->createModelChecker(model);
439 std::unique_ptr<storm::modelchecker::CheckResult> result;
440
441 uint64_t propertyIndex = 0;
442 auto expected = this->parseNumber("0.9502129316"); // integrate 6* e^(-6*t) dt from 0 to 0.5 = 1 - 1/(e^3)
443 result = checker->check(this->env(), tasks[propertyIndex++]);
444 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
445
446 expected = this->parseNumber("0.075198060651"); // integrate min(t,0.1) * 6* e^(-6*t) dt from 0 to infty = 1/6 - 1/(6*e^0.6)
447 result = checker->check(this->env(), tasks[propertyIndex++]);
448 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
449
450 expected = this->parseNumber("0.1662535413"); // = 1/6 - 1/(6*e^6)
451 result = checker->check(this->env(), tasks[propertyIndex++]);
452 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
453
454 expected = this->parseNumber("0.16666666667"); // = 1/6 - 1/(6*e^60)
455 result = checker->check(this->env(), tasks[propertyIndex++]);
456 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
457 });
458}
459
460TYPED_TEST(CtmcCslModelCheckerTest, simple2) {
461 std::string formulasString = "R{\"rew1\"}=? [ C ]";
462 formulasString += "; R{\"rew2\"}=? [ C ]";
463
464 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/simple2.sm", formulasString);
465 auto model = std::move(modelFormulas.first);
466 auto tasks = this->getTasks(modelFormulas.second);
467 EXPECT_EQ(5ul, model->getNumberOfStates());
468 EXPECT_EQ(8ul, model->getNumberOfTransitions());
469 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
470 auto checker = this->createModelChecker(model);
471 std::unique_ptr<storm::modelchecker::CheckResult> result;
472
473 // Total reward formulas are currently not supported for non-sparse models.
474 if (this->isSparseModel()) {
475 result = checker->check(this->env(), tasks[0]);
476 EXPECT_NEAR(this->parseNumber("23/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
477
478 result = checker->check(this->env(), tasks[1]);
479 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
480 } else {
481 EXPECT_FALSE(checker->canHandle(tasks[0]));
482 }
483}
484
485TEST(CtmcCslModelCheckerTest, TransientProbabilities) {
486 // Example from lecture
487 storm::storage::SparseMatrixBuilder<double> matrixBuilder;
488 matrixBuilder.addNextValue(0, 1, 3.0);
489 matrixBuilder.addNextValue(1, 0, 2.0);
490 storm::storage::SparseMatrix<double> matrix = matrixBuilder.build();
491
492 std::vector<double> exitRates = {3, 2};
493 storm::storage::BitVector initialStates(2);
494 initialStates.set(0);
495 storm::storage::BitVector phiStates(2);
496 storm::storage::BitVector psiStates(2);
497 storm::Environment env;
498 std::vector<double> result =
499 storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, matrix, initialStates, phiStates, psiStates, exitRates, 1);
500
501 EXPECT_NEAR(0.404043, result[0], 1e-6);
502 EXPECT_NEAR(0.595957, result[1], 1e-6);
503}
504
505TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesEmbedded) {
506#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
507 std::string formulasString = "P=? [ X F (!\"down\" U \"fail_sensors\") ]";
508 formulasString += "; P=? [ (! \"down\" U ( F \"fail_actuators\" U \"fail_io\")) ]";
509 formulasString += "; P=? [ F \"down\" & X G \"fail_sensors\" ]"; // F ("down" & (X (G "fail_sensors")) )
510 formulasString += "; P<1 [ F \"down\" & X G \"fail_sensors\" ]"; // F ("down" & (X (G "fail_sensors")) )
511 formulasString += "; P>0.9 [ F \"down\" & X G \"fail_sensors\" ]"; // F ("down" & (X (G "fail_sensors")) )
512 formulasString += "; P=? [ ( X X X X X X !\"down\") ]";
513
514 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString);
515 auto model = std::move(modelFormulas.first);
516 auto tasks = this->getTasks(modelFormulas.second);
517 EXPECT_EQ(3478ul, model->getNumberOfStates());
518 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
519 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
520
521 auto checker = this->createModelChecker(model);
522 std::unique_ptr<storm::modelchecker::CheckResult> result;
523 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
524 result = checker->check(this->env(), tasks[0]);
525
526 EXPECT_NEAR(this->parseNumber("6201111489217/6635130141055"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
527
528 result = checker->check(this->env(), tasks[1]);
529 EXPECT_NEAR(this->parseNumber(
530 "18202096756782580932452575931626387221032158256811408997544247061630654697057679936888914805428640014003923523854237983369404268771063"
531 "94069377761908861354080901656982334306495936806479819524633477460248734957778578143867737103318041699906745291007545836953677741618755"
532 "07044994661278270139591275881461260070117701448841596602041739425021618556458197240253807881255308059191194657575523127649292873946401"
533 "60070574497678932806876628747257457080365284815733250063282059801375609508589060775771365121570763916254686586313389233475877585811662"
534 "0357147078085971884542677483086820336410289852315689173054718889915988181632722920483222289764504589120520736097022590652379/"
535 "20728856609142464902872005939672257918093593973189631748243740034008572994831983832074458796252899535111673563261006250198416596416082"
536 "47438209685029840433936315271626219407003724379672398699027456844707912472180250116299363836831808191736954813578721274144593836954580"
537 "34829702750095798077157671737142972112983783526417917830063407814131534204102733837172200651731758231462705370319722286895248244604663"
538 "52533471344327110886363060826404895467465893956592712512371350202090241564215213495275079722307576230931018615138366081056985311311073"
539 "6677679624520398243456708277522978182665363672039087497825748539279661186260492946647251487454498033763681938956076478285935"),
540 this->getQuantitativeResultAtInitialState(model, result), this->precision());
541
542 result = checker->check(this->env(), tasks[2]);
543 EXPECT_NEAR(this->parseNumber("6201111489217/6635130141055"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
544
545 result = checker->check(this->env(), tasks[3]);
546 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
547
548 result = checker->check(this->env(), tasks[4]);
549 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
550
551 result = checker->check(this->env(), tasks[5]);
552 EXPECT_NEAR(
553 this->parseNumber("12029468814241604838132837548112161585296814078767944885625781581320425536116175992062768102403002605220660026092168995568067825"
554 "92159369214025808794108439870476812421358247413140536419394633974952856222783873484713998841710951907938016323396243234904692402"
555 "52961677855027461283258094829047603758584033514598048083454101721311299129841296115907033485846297142252703801497367159453680266"
556 "24792167429109658151655487647994259314643886424142766790442953987818429468012101992798588110824350651761547347356873144826620057"
557 "74077569191240855183945543277103593833128730289929192543135438680962528094118605758445585995100073617/"
558 "12029720509287104832319318812972923934077469133245668896466828391759984671516390780365666074295318137833660807349293929200056244"
559 "56488274509559191073647430577878963431232759904608946782891839010213213206349818700590576273106941528872428420715245020013732520"
560 "85567053299253798937031071047697289051751242127258744937438520681995840650837777808189738580512102669860241858552660166073849086"
561 "67980634152813607901785527175246314720373131268228013598128613517599905951566964079825880226357974174647948493893065216449623389"
562 "15119549986021747121828809226061546105390273235103310319147341214480736689719855550298904337697187500"),
563 this->getQuantitativeResultAtInitialState(model, result), this->precision());
564
565 } else {
566 EXPECT_FALSE(checker->canHandle(tasks[0]));
567 }
568#else
569 GTEST_SKIP();
570#endif
571}
572
573TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesPolling) {
574#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
575 std::string formulasString = "P=? [ X X !(s=1 & a=1) U (s=2 & a=1) ]"; // (X X a) U b
576 formulasString += "; P=? [ X (( !(s=1) U (a=1)) U (s=1)) ]";
577
578 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString);
579 auto model = std::move(modelFormulas.first);
580 auto tasks = this->getTasks(modelFormulas.second);
581 EXPECT_EQ(12ul, model->getNumberOfStates());
582 EXPECT_EQ(22ul, model->getNumberOfTransitions());
583 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
584
585 auto checker = this->createModelChecker(model);
586 std::unique_ptr<storm::modelchecker::CheckResult> result;
587 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
588 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
589 result = checker->check(this->env(), tasks[0]);
590 EXPECT_NEAR(this->parseNumber("80400/160801"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
591
592 result = checker->check(this->env(), tasks[1]);
593 EXPECT_NEAR(this->parseNumber("601/80601"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
594
595 } else {
596 EXPECT_FALSE(checker->canHandle(tasks[0]));
597 }
598#else
599 GTEST_SKIP();
600#endif
601}
602
603TYPED_TEST(CtmcCslModelCheckerTest, HOAProbabilitiesPolling) {
604 // "P=? [ F "target" & (X s=1)]"
605 std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"target\", \"p1\" -> (s=1) }]";
606 // "P=? [!(s=1) U (s=1)]"
607 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s=1) , \"p1\" -> \"target\" }]";
608
609 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString);
610 auto model = std::move(modelFormulas.first);
611 auto tasks = this->getTasks(modelFormulas.second);
612 EXPECT_EQ(12ul, model->getNumberOfStates());
613 EXPECT_EQ(22ul, model->getNumberOfTransitions());
614 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
615 auto checker = this->createModelChecker(model);
616 std::unique_ptr<storm::modelchecker::CheckResult> result;
617
618 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
619 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
620 result = checker->check(tasks[0]);
621 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
622
623 result = checker->check(tasks[1]);
624 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
625 } else {
626 EXPECT_FALSE(checker->canHandle(tasks[0]));
627 }
628}
629} // 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::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::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities
static std::vector< ValueType > computeAllTransientProbabilities(Environment const &env, storm::storage::SparseMatrix< ValueType > const &rateMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, std::vector< ValueType > const &exitRates, double timeBound)
Definition SparseCtmcCslHelper.cpp:546
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
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
storm::storage::SparseMatrixBuilder
A class that can be used to build a sparse matrix by adding value by value.
Definition SparseMatrix.h:136
storm::storage::SparseMatrixBuilder::addNextValue
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
Definition SparseMatrix.cpp:156
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:281
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
storm::utility::isInfinity
bool isInfinity(ValueType const &a)
Definition constants.cpp:71
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