Storm
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<SparseGmmxxGmresIluEnvironment, JaniSparseGmmxxGmresIluEnvironment, SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment,
302 SparseNativeSorEnvironment, HybridCuddGmmxxGmresEnvironment, JaniHybridCuddGmmxxGmresEnvironment, HybridSylvanGmmxxGmresEnvironment>
303 TestingTypes;
304
305TYPED_TEST_SUITE(CtmcCslModelCheckerTest, TestingTypes, );
306
307TYPED_TEST(CtmcCslModelCheckerTest, Cluster) {
308 std::string formulasString = "P=? [ F<=100 !\"minimum\"]";
309 formulasString += "; P=? [ F[100,100] !\"minimum\"]";
310 formulasString += "; P=? [ F[100,2000] !\"minimum\"]";
311 formulasString += "; P=? [ \"minimum\" U<=10 \"premium\"]";
312 formulasString += "; P=? [ !\"minimum\" U>=1 \"minimum\"]";
313 formulasString += "; P=? [ \"minimum\" U>=1 !\"minimum\"]";
314 formulasString += "; R=? [C<=100]";
315
316 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", formulasString);
317 auto model = std::move(modelFormulas.first);
318 auto tasks = this->getTasks(modelFormulas.second);
319 this->execute(model, [&]() {
320 EXPECT_EQ(276ul, model->getNumberOfStates());
321 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
322 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
323 auto checker = this->createModelChecker(model);
324 std::unique_ptr<storm::modelchecker::CheckResult> result;
325
326 result = checker->check(this->env(), tasks[0]);
327 EXPECT_NEAR(this->parseNumber("5.5461254704419085E-5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
328
329 result = checker->check(this->env(), tasks[1]);
330 EXPECT_NEAR(this->parseNumber("2.3397873548343415E-6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
331
332 result = checker->check(this->env(), tasks[2]);
333 EXPECT_NEAR(this->parseNumber("0.001105335651670241"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
334
335 result = checker->check(this->env(), tasks[3]);
336 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
337
338 result = checker->check(this->env(), tasks[4]);
339 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
340
341 result = checker->check(this->env(), tasks[5]);
342 EXPECT_NEAR(this->parseNumber("0.9999999033633374"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
343
344 result = checker->check(this->env(), tasks[6]);
345 EXPECT_NEAR(this->parseNumber("0.8602815057967503"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
346 });
347}
348
349TYPED_TEST(CtmcCslModelCheckerTest, Embedded) {
350 std::string formulasString = "P=? [ F<=10000 \"down\"]";
351 formulasString += "; P=? [ !\"down\" U<=10000 \"fail_actuators\"]";
352 formulasString += "; P=? [ !\"down\" U<=10000 \"fail_io\"]";
353 formulasString += "; P=? [ !\"down\" U<=10000 \"fail_sensors\"]";
354 formulasString += "; R{\"up\"}=? [C<=10000]";
355
356 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString);
357 auto model = std::move(modelFormulas.first);
358 auto tasks = this->getTasks(modelFormulas.second);
359 this->execute(model, [&]() {
360 EXPECT_EQ(3478ul, model->getNumberOfStates());
361 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
362 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
363 auto checker = this->createModelChecker(model);
364 std::unique_ptr<storm::modelchecker::CheckResult> result;
365
366 result = checker->check(this->env(), tasks[0]);
367 EXPECT_NEAR(this->parseNumber("0.0019216435246119591"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
368
369 result = checker->check(this->env(), tasks[1]);
370 EXPECT_NEAR(this->parseNumber("3.7079151806696567E-6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
371
372 result = checker->check(this->env(), tasks[2]);
373 EXPECT_NEAR(this->parseNumber("0.001556839327673734"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
374
375 result = checker->check(this->env(), tasks[3]);
376 EXPECT_NEAR(this->parseNumber("4.429620626755424E-5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
377
378 result = checker->check(this->env(), tasks[4]);
379 EXPECT_NEAR(this->parseNumber("2.7745274082080154"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
380 });
381}
382
383TYPED_TEST(CtmcCslModelCheckerTest, Tandem) {
384 std::string formulasString = "P=? [ F<=10 \"network_full\" ]";
385 formulasString += "; P=? [ F<=10 \"first_queue_full\" ]";
386 formulasString += "; P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]";
387 formulasString += "; R=? [I=10]";
388 formulasString += "; R=? [C<=10]";
389 formulasString += "; R=? [F \"first_queue_full\"&\"second_queue_full\"]";
390
391 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", formulasString);
392 auto model = std::move(modelFormulas.first);
393 auto tasks = this->getTasks(modelFormulas.second);
394 this->execute(model, [&]() {
395 EXPECT_EQ(66ul, model->getNumberOfStates());
396 EXPECT_EQ(189ul, model->getNumberOfTransitions());
397 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
398 auto checker = this->createModelChecker(model);
399 std::unique_ptr<storm::modelchecker::CheckResult> result;
400
401 result = checker->check(this->env(), tasks[0]);
402 EXPECT_NEAR(this->parseNumber("0.015446370562428037"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
403
404 result = checker->check(this->env(), tasks[1]);
405 EXPECT_NEAR(this->parseNumber("0.999999837225515"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
406
407 result = checker->check(this->env(), tasks[2]);
408 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
409
410 result = checker->check(this->env(), tasks[3]);
411 EXPECT_NEAR(this->parseNumber("5.679243850315877"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
412
413 result = checker->check(this->env(), tasks[4]);
414 EXPECT_NEAR(this->parseNumber("55.44792186036232"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
415
416 result = checker->check(this->env(), tasks[5]);
417 EXPECT_NEAR(this->parseNumber("262.85103824276308"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
418 });
419}
420
421TYPED_TEST(CtmcCslModelCheckerTest, simple1) {
422 std::string formulasString = "P=? [ F<=0.5 x=1 ]";
423 formulasString += "; R=? [ C<=0.1 ]";
424 formulasString += "; R=? [ C<=1 ]";
425 formulasString += "; R=? [ C<=10 ]";
426
427 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/simple1.sm", formulasString);
428 auto model = std::move(modelFormulas.first);
429 auto tasks = this->getTasks(modelFormulas.second);
430 this->execute(model, [&]() {
431 EXPECT_EQ(2ul, model->getNumberOfStates());
432 EXPECT_EQ(2ul, model->getNumberOfTransitions());
433 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
434 auto checker = this->createModelChecker(model);
435 std::unique_ptr<storm::modelchecker::CheckResult> result;
436
437 uint64_t propertyIndex = 0;
438 auto expected = this->parseNumber("0.9502129316"); // integrate 6* e^(-6*t) dt from 0 to 0.5 = 1 - 1/(e^3)
439 result = checker->check(this->env(), tasks[propertyIndex++]);
440 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
441
442 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)
443 result = checker->check(this->env(), tasks[propertyIndex++]);
444 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
445
446 expected = this->parseNumber("0.1662535413"); // = 1/6 - 1/(6*e^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.16666666667"); // = 1/6 - 1/(6*e^60)
451 result = checker->check(this->env(), tasks[propertyIndex++]);
452 EXPECT_NEAR(expected, this->getQuantitativeResultAtInitialState(model, result), this->precision());
453 });
454}
455
456TYPED_TEST(CtmcCslModelCheckerTest, simple2) {
457 std::string formulasString = "R{\"rew1\"}=? [ C ]";
458 formulasString += "; R{\"rew2\"}=? [ C ]";
459
460 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/simple2.sm", formulasString);
461 auto model = std::move(modelFormulas.first);
462 auto tasks = this->getTasks(modelFormulas.second);
463 EXPECT_EQ(5ul, model->getNumberOfStates());
464 EXPECT_EQ(8ul, model->getNumberOfTransitions());
465 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
466 auto checker = this->createModelChecker(model);
467 std::unique_ptr<storm::modelchecker::CheckResult> result;
468
469 // Total reward formulas are currently not supported for non-sparse models.
470 if (this->isSparseModel()) {
471 result = checker->check(this->env(), tasks[0]);
472 EXPECT_NEAR(this->parseNumber("23/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
473
474 result = checker->check(this->env(), tasks[1]);
475 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
476 } else {
477 EXPECT_FALSE(checker->canHandle(tasks[0]));
478 }
479}
480
481TEST(CtmcCslModelCheckerTest, TransientProbabilities) {
482 // Example from lecture
483 storm::storage::SparseMatrixBuilder<double> matrixBuilder;
484 matrixBuilder.addNextValue(0, 1, 3.0);
485 matrixBuilder.addNextValue(1, 0, 2.0);
486 storm::storage::SparseMatrix<double> matrix = matrixBuilder.build();
487
488 std::vector<double> exitRates = {3, 2};
489 storm::storage::BitVector initialStates(2);
490 initialStates.set(0);
491 storm::storage::BitVector phiStates(2);
492 storm::storage::BitVector psiStates(2);
493 storm::Environment env;
494 std::vector<double> result =
495 storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, matrix, initialStates, phiStates, psiStates, exitRates, 1);
496
497 EXPECT_NEAR(0.404043, result[0], 1e-6);
498 EXPECT_NEAR(0.595957, result[1], 1e-6);
499}
500
501TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesEmbedded) {
502#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
503 std::string formulasString = "P=? [ X F (!\"down\" U \"fail_sensors\") ]";
504 formulasString += "; P=? [ (! \"down\" U ( F \"fail_actuators\" U \"fail_io\")) ]";
505 formulasString += "; P=? [ F \"down\" & X G \"fail_sensors\" ]"; // F ("down" & (X (G "fail_sensors")) )
506 formulasString += "; P<1 [ F \"down\" & X G \"fail_sensors\" ]"; // F ("down" & (X (G "fail_sensors")) )
507 formulasString += "; P>0.9 [ F \"down\" & X G \"fail_sensors\" ]"; // F ("down" & (X (G "fail_sensors")) )
508 formulasString += "; P=? [ ( X X X X X X !\"down\") ]";
509
510 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", formulasString);
511 auto model = std::move(modelFormulas.first);
512 auto tasks = this->getTasks(modelFormulas.second);
513 EXPECT_EQ(3478ul, model->getNumberOfStates());
514 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
515 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
516
517 auto checker = this->createModelChecker(model);
518 std::unique_ptr<storm::modelchecker::CheckResult> result;
519 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
520 result = checker->check(this->env(), tasks[0]);
521
522 EXPECT_NEAR(this->parseNumber("6201111489217/6635130141055"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
523
524 result = checker->check(this->env(), tasks[1]);
525 EXPECT_NEAR(this->parseNumber(
526 "18202096756782580932452575931626387221032158256811408997544247061630654697057679936888914805428640014003923523854237983369404268771063"
527 "94069377761908861354080901656982334306495936806479819524633477460248734957778578143867737103318041699906745291007545836953677741618755"
528 "07044994661278270139591275881461260070117701448841596602041739425021618556458197240253807881255308059191194657575523127649292873946401"
529 "60070574497678932806876628747257457080365284815733250063282059801375609508589060775771365121570763916254686586313389233475877585811662"
530 "0357147078085971884542677483086820336410289852315689173054718889915988181632722920483222289764504589120520736097022590652379/"
531 "20728856609142464902872005939672257918093593973189631748243740034008572994831983832074458796252899535111673563261006250198416596416082"
532 "47438209685029840433936315271626219407003724379672398699027456844707912472180250116299363836831808191736954813578721274144593836954580"
533 "34829702750095798077157671737142972112983783526417917830063407814131534204102733837172200651731758231462705370319722286895248244604663"
534 "52533471344327110886363060826404895467465893956592712512371350202090241564215213495275079722307576230931018615138366081056985311311073"
535 "6677679624520398243456708277522978182665363672039087497825748539279661186260492946647251487454498033763681938956076478285935"),
536 this->getQuantitativeResultAtInitialState(model, result), this->precision());
537
538 result = checker->check(this->env(), tasks[2]);
539 EXPECT_NEAR(this->parseNumber("6201111489217/6635130141055"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
540
541 result = checker->check(this->env(), tasks[3]);
542 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
543
544 result = checker->check(this->env(), tasks[4]);
545 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
546
547 result = checker->check(this->env(), tasks[5]);
548 EXPECT_NEAR(
549 this->parseNumber("12029468814241604838132837548112161585296814078767944885625781581320425536116175992062768102403002605220660026092168995568067825"
550 "92159369214025808794108439870476812421358247413140536419394633974952856222783873484713998841710951907938016323396243234904692402"
551 "52961677855027461283258094829047603758584033514598048083454101721311299129841296115907033485846297142252703801497367159453680266"
552 "24792167429109658151655487647994259314643886424142766790442953987818429468012101992798588110824350651761547347356873144826620057"
553 "74077569191240855183945543277103593833128730289929192543135438680962528094118605758445585995100073617/"
554 "12029720509287104832319318812972923934077469133245668896466828391759984671516390780365666074295318137833660807349293929200056244"
555 "56488274509559191073647430577878963431232759904608946782891839010213213206349818700590576273106941528872428420715245020013732520"
556 "85567053299253798937031071047697289051751242127258744937438520681995840650837777808189738580512102669860241858552660166073849086"
557 "67980634152813607901785527175246314720373131268228013598128613517599905951566964079825880226357974174647948493893065216449623389"
558 "15119549986021747121828809226061546105390273235103310319147341214480736689719855550298904337697187500"),
559 this->getQuantitativeResultAtInitialState(model, result), this->precision());
560
561 } else {
562 EXPECT_FALSE(checker->canHandle(tasks[0]));
563 }
564#else
565 GTEST_SKIP();
566#endif
567}
568
569TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesPolling) {
570#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
571 std::string formulasString = "P=? [ X X !(s=1 & a=1) U (s=2 & a=1) ]"; // (X X a) U b
572 formulasString += "; P=? [ X (( !(s=1) U (a=1)) U (s=1)) ]";
573
574 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString);
575 auto model = std::move(modelFormulas.first);
576 auto tasks = this->getTasks(modelFormulas.second);
577 EXPECT_EQ(12ul, model->getNumberOfStates());
578 EXPECT_EQ(22ul, model->getNumberOfTransitions());
579 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
580
581 auto checker = this->createModelChecker(model);
582 std::unique_ptr<storm::modelchecker::CheckResult> result;
583 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
584 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
585 result = checker->check(this->env(), tasks[0]);
586 EXPECT_NEAR(this->parseNumber("80400/160801"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
587
588 result = checker->check(this->env(), tasks[1]);
589 EXPECT_NEAR(this->parseNumber("601/80601"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
590
591 } else {
592 EXPECT_FALSE(checker->canHandle(tasks[0]));
593 }
594#else
595 GTEST_SKIP();
596#endif
597}
598
599TYPED_TEST(CtmcCslModelCheckerTest, HOAProbabilitiesPolling) {
600 // "P=? [ F "target" & (X s=1)]"
601 std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"target\", \"p1\" -> (s=1) }]";
602 // "P=? [!(s=1) U (s=1)]"
603 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s=1) , \"p1\" -> \"target\" }]";
604
605 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", formulasString);
606 auto model = std::move(modelFormulas.first);
607 auto tasks = this->getTasks(modelFormulas.second);
608 EXPECT_EQ(12ul, model->getNumberOfStates());
609 EXPECT_EQ(22ul, model->getNumberOfTransitions());
610 ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
611 auto checker = this->createModelChecker(model);
612 std::unique_ptr<storm::modelchecker::CheckResult> result;
613
614 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
615 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
616 result = checker->check(tasks[0]);
617 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
618
619 result = checker->check(tasks[1]);
620 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
621 } else {
622 EXPECT_FALSE(checker->canHandle(tasks[0]));
623 }
624}
625} // 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:137
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:332
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
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