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