Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MarkovAutomatonCslModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
7#include "storm/api/builder.h"
26
27namespace {
28
29enum class MaEngine { PrismSparse, JaniSparse, JaniHybrid };
30
31class SparseDoubleValueIterationEnvironment {
32 public:
33 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
34 static const MaEngine engine = MaEngine::PrismSparse;
35 static const bool isExact = false;
36 typedef double ValueType;
38 static storm::Environment createEnvironment() {
40 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
41 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
42 return env;
43 }
44};
45class JaniSparseDoubleValueIterationEnvironment {
46 public:
47 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
48 static const MaEngine engine = MaEngine::JaniSparse;
49 static const bool isExact = false;
50 typedef double ValueType;
52 static storm::Environment createEnvironment() {
54 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
55 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
56 return env;
57 }
58};
59class JaniHybridDoubleValueIterationEnvironment {
60 public:
61 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
62 static const MaEngine engine = MaEngine::JaniHybrid;
63 static const bool isExact = false;
64 typedef double ValueType;
66 static storm::Environment createEnvironment() {
68 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, true);
69 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
70 return env;
71 }
72};
73class SparseDoubleIntervalIterationEnvironment {
74 public:
75 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
76 static const MaEngine engine = MaEngine::PrismSparse;
77 static const bool isExact = false;
78 typedef double ValueType;
80 static storm::Environment createEnvironment() {
82 env.solver().setForceSoundness(true);
83 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration, true);
84 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
86 return env;
87 }
88};
89class SparseRationalPolicyIterationEnvironment {
90 public:
91 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
92 static const MaEngine engine = MaEngine::PrismSparse;
93 static const bool isExact = true;
94 typedef storm::RationalNumber ValueType;
96 static storm::Environment createEnvironment() {
98 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration, true);
99 return env;
100 }
101};
102class SparseRationalRationalSearchEnvironment {
103 public:
104 static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
105 static const MaEngine engine = MaEngine::PrismSparse;
106 static const bool isExact = true;
107 typedef storm::RationalNumber ValueType;
109 static storm::Environment createEnvironment() {
111 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch, true);
112 return env;
113 }
114};
115
116template<typename TestType>
117class MarkovAutomatonCslModelCheckerTest : public ::testing::Test {
118 public:
119 typedef typename TestType::ValueType ValueType;
120 typedef typename storm::models::sparse::MarkovAutomaton<ValueType> SparseModelType;
122
123 MarkovAutomatonCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
124
125 void SetUp() override {
126#ifndef STORM_HAVE_Z3
127 GTEST_SKIP() << "Z3 not available.";
128#endif
129 }
130
131 storm::Environment const& env() const {
132 return _environment;
133 }
134 ValueType parseNumber(std::string const& input) const {
135 return storm::utility::convertNumber<ValueType>(input);
136 }
137 ValueType precision() const {
138 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
139 }
140 bool isSparseModel() const {
141 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
142 }
143 bool isSymbolicModel() const {
144 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
145 }
146
147 template<typename MT = typename TestType::ModelType>
148 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
149 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
150 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
151 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
152 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
153 program = storm::utility::prism::preprocess(program, constantDefinitionString);
154 if (TestType::engine == MaEngine::PrismSparse) {
156 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
157 } else if (TestType::engine == MaEngine::JaniSparse) {
158 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
159 result.second = storm::api::extractFormulasFromProperties(janiData.second);
160 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
161 }
162 return result;
163 }
164
165 template<typename MT = typename TestType::ModelType>
166 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
167 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
168 buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
169 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
170 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
171 program = storm::utility::prism::preprocess(program, constantDefinitionString);
172 auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
173 result.second = storm::api::extractFormulasFromProperties(janiData.second);
174 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
175 return result;
176 }
177
178 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
179 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
180 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
181 for (auto const& f : formulas) {
182 result.emplace_back(*f);
183 }
184 return result;
185 }
186
187 template<typename MT = typename TestType::ModelType>
188 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
189 std::shared_ptr<MT> const& model) const {
190 if (TestType::engine == MaEngine::PrismSparse || TestType::engine == MaEngine::JaniSparse) {
191 return std::make_shared<storm::modelchecker::SparseMarkovAutomatonCslModelChecker<SparseModelType>>(*model);
192 }
193 return nullptr;
194 }
195
196 template<typename MT = typename TestType::ModelType>
197 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
198 createModelChecker(std::shared_ptr<MT> const& model) const {
199 if (TestType::engine == MaEngine::JaniHybrid) {
200 return std::make_shared<storm::modelchecker::HybridMarkovAutomatonCslModelChecker<SymbolicModelType>>(*model);
201 // } else if (TestType::engine == MaEngine::Dd) {
202 // return std::make_shared<storm::modelchecker::SymbolicMarkovAutomatonCslModelChecker<SymbolicModelType>>(*model);
203 }
204 return nullptr;
205 }
206
207 template<typename MT = typename TestType::ModelType>
208 typename std::enable_if<std::is_same<MT, SparseModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
209 std::function<void()> const& f) const {
210 f();
211 }
212
213 template<typename MT = typename TestType::ModelType>
214 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, void>::type execute(std::shared_ptr<MT> const& model,
215 std::function<void()> const& f) const {
216 model->getManager().execute(f);
217 }
218
219 bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model,
220 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
221 auto filter = getInitialStateFilter(model);
222 result->filter(*filter);
223 return result->asQualitativeCheckResult().forallTrue();
224 }
225
227 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
228 auto filter = getInitialStateFilter(model);
229 result->filter(*filter);
230 return result->asQuantitativeCheckResult<ValueType>().getMin();
231 }
232
233 private:
234 storm::Environment _environment;
235
236 std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
237 if (isSparseModel()) {
238 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
239 } else {
240 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
241 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
242 }
243 }
244};
245
246typedef ::testing::Types<SparseDoubleValueIterationEnvironment, JaniSparseDoubleValueIterationEnvironment, JaniHybridDoubleValueIterationEnvironment,
247 SparseDoubleIntervalIterationEnvironment, SparseRationalPolicyIterationEnvironment, SparseRationalRationalSearchEnvironment>
249
250TYPED_TEST_SUITE(MarkovAutomatonCslModelCheckerTest, TestingTypes, );
251
252TYPED_TEST(MarkovAutomatonCslModelCheckerTest, server) {
253 std::string formulasString = "Tmax=? [F \"error\"]";
254 formulasString += "; Pmax=? [F \"processB\"]";
255 formulasString += "; Pmax=? [F<1 \"error\"]";
256
257 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/server.ma", formulasString);
258 auto model = std::move(modelFormulas.first);
259 auto tasks = this->getTasks(modelFormulas.second);
260 this->execute(model, [&]() {
261 EXPECT_EQ(6ul, model->getNumberOfStates());
262 EXPECT_EQ(10ul, model->getNumberOfTransitions());
263 ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton);
264 auto checker = this->createModelChecker(model);
265 std::unique_ptr<storm::modelchecker::CheckResult> result;
266
267 result = checker->check(this->env(), tasks[0]);
268 EXPECT_NEAR(this->parseNumber("11/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
269
270 result = checker->check(this->env(), tasks[1]);
271 EXPECT_NEAR(this->parseNumber("2/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
272
273 if (!storm::utility::isZero(this->precision())) {
274 result = checker->check(this->env(), tasks[2]);
275 EXPECT_NEAR(this->parseNumber("0.455504"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
276 }
277 });
278}
279
280TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple) {
281 std::string formulasString = "Pmin=? [F<1 s>2]";
282 formulasString += "; Pmax=? [F<1.3 s=3]";
283
284 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString);
285 auto model = std::move(modelFormulas.first);
286 auto tasks = this->getTasks(modelFormulas.second);
287 this->execute(model, [&]() {
288 EXPECT_EQ(5ul, model->getNumberOfStates());
289 EXPECT_EQ(8ul, model->getNumberOfTransitions());
290 ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton);
291 auto checker = this->createModelChecker(model);
292 std::unique_ptr<storm::modelchecker::CheckResult> result;
293
294 if (!storm::utility::isZero(this->precision())) {
295 result = checker->check(this->env(), tasks[0]);
296 EXPECT_NEAR(this->parseNumber("0.6321205588"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
297
298 result = checker->check(this->env(), tasks[1]);
299 EXPECT_NEAR(this->parseNumber("0.727468207"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
300 }
301 });
302}
303
304TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple2) {
305 std::string formulasString = "R{\"rew0\"}max=? [C]";
306 formulasString += "; R{\"rew0\"}min=? [C]";
307 formulasString += "; R{\"rew1\"}max=? [C]";
308 formulasString += "; R{\"rew1\"}min=? [C]";
309 formulasString += "; R{\"rew2\"}max=? [C]";
310 formulasString += "; R{\"rew2\"}min=? [C]";
311 formulasString += "; R{\"rew3\"}min=? [C]";
312 formulasString += "; LRAmin=? [s=0 | s=3]"; // 0
313 formulasString += "; R{\"rew3\"}max=?[ LRA ]"; // 407
314 formulasString += "; R{\"rew3\"}min=?[ LRA ]"; // 27
315
316 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple2.ma", formulasString);
317 auto model = std::move(modelFormulas.first);
318 auto tasks = this->getTasks(modelFormulas.second);
319 EXPECT_EQ(6ul, model->getNumberOfStates());
320 EXPECT_EQ(11ul, model->getNumberOfTransitions());
321 ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton);
322 auto checker = this->createModelChecker(model);
323 std::unique_ptr<storm::modelchecker::CheckResult> result;
324
325 if (TypeParam::engine != MaEngine::JaniHybrid) {
326 // Total Reward Formulas are not supported in the hybrid engine (for now).
327
328 result = checker->check(this->env(), tasks[0]);
329 EXPECT_NEAR(this->parseNumber("2"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
330
331 result = checker->check(this->env(), tasks[1]);
332 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
333
334 result = checker->check(this->env(), tasks[2]);
335 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
336
337 result = checker->check(this->env(), tasks[3]);
338 EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
339
340 result = checker->check(this->env(), tasks[4]);
341 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
342
343 result = checker->check(this->env(), tasks[5]);
344 EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
345
346 result = checker->check(this->env(), tasks[6]);
347 EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
348 }
349
350#ifndef STORM_HAVE_Z3_OPTIMIZE
351 if (!storm::utility::isZero(this->precision())) {
352#endif
353 // Checking LRA properties exactly requires an exact LP solver.
354 result = checker->check(this->env(), tasks[7]);
355 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
356
357 result = checker->check(this->env(), tasks[8]);
358 EXPECT_NEAR(this->parseNumber("407"), this->getQuantitativeResultAtInitialState(model, result),
359 this->precision() * this->parseNumber("407")); // use relative precision!
360
361 result = checker->check(this->env(), tasks[9]);
362 EXPECT_NEAR(this->parseNumber("27"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
363#ifndef STORM_HAVE_Z3_OPTIMIZE
364 }
365#endif
366}
367
368TYPED_TEST(MarkovAutomatonCslModelCheckerTest, LtlSimple) {
369#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
370 std::string formulasString = "Pmax=? [X X s=3]";
371 formulasString += "; Pmax=? [X X G s>2]";
372 formulasString += "; Pmin=? [X X G s>2]";
373 formulasString += "; Pmax=? [F ((s=0) U X(s=0) & X(s=2))]";
374
375 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString);
376 auto model = std::move(modelFormulas.first);
377 auto tasks = this->getTasks(modelFormulas.second);
378 EXPECT_EQ(5ul, model->getNumberOfStates());
379 EXPECT_EQ(8ul, model->getNumberOfTransitions());
380 ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton);
381 auto checker = this->createModelChecker(model);
382 std::unique_ptr<storm::modelchecker::CheckResult> result;
383
384 // LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
385 if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse) {
386 result = checker->check(this->env(), tasks[0]);
387 EXPECT_NEAR(this->parseNumber("1/10"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
388
389 result = checker->check(this->env(), tasks[1]);
390 EXPECT_NEAR(this->parseNumber("1/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
391
392 result = checker->check(this->env(), tasks[2]);
393 EXPECT_NEAR(this->parseNumber("1/10"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
394
395 result = checker->check(this->env(), tasks[3]);
396 EXPECT_NEAR(this->parseNumber("9/10"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
397
398 } else {
399 EXPECT_FALSE(checker->canHandle(tasks[0]));
400 }
401#else
402 GTEST_SKIP();
403#endif
404}
405
406TYPED_TEST(MarkovAutomatonCslModelCheckerTest, HOASimple) {
407 // "P=? [ F (s=3) & (X s=1)]"
408 std::string formulasString = "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s>1), \"p1\" -> !(s=1) }]";
409 // "P=? [ (s=2) U (s=1)]"
410 formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s=2), \"p1\" -> (s=1) }]";
411
412 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString);
413 auto model = std::move(modelFormulas.first);
414 auto tasks = this->getTasks(modelFormulas.second);
415 EXPECT_EQ(5ul, model->getNumberOfStates());
416 EXPECT_EQ(8ul, model->getNumberOfTransitions());
417 ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton);
418 auto checker = this->createModelChecker(model);
419 std::unique_ptr<storm::modelchecker::CheckResult> result;
420
421 // Not supported in all engines (Hybrid, PrismDd, JaniDd)
422 if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse) {
423 result = checker->check(tasks[0]);
424 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
425
426 result = checker->check(tasks[1]);
427 EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
428 } else {
429 EXPECT_FALSE(checker->canHandle(tasks[0]));
430 }
431}
432} // namespace
std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model)
double getQuantitativeResultAtInitialState(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
SolverEnvironment & solver()
void setPrecision(storm::RationalNumber value)
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
MinMaxSolverEnvironment & minMax()
This class represents a Markov automaton.
This class represents a discrete-time Markov decision process.
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > convertPrismToJani(storm::prism::Program const &program, storm::converter::PrismToJaniConverterOptions options)
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
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
bool isZero(ValueType const &a)
Definition constants.cpp:41
bool isInfinity(ValueType const &a)
Definition constants.cpp:71
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46