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