Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LraMdpPrctlModelCheckerTest.cpp
Go to the documentation of this file.
1#include "test/storm_gtest.h"
2
3#include "test/storm_gtest.h"
4
5#include "storm-config.h"
6
7#include "storm-conv/api/storm-conv.h"
8#include "storm-parsers/api/model_descriptions.h"
9#include "storm-parsers/api/properties.h"
10#include "storm/api/builder.h"
11#include "storm/api/properties.h"
12
13#include "storm-parsers/parser/FormulaParser.h"
14#include "storm/logic/Formulas.h"
15#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
16#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
17#include "storm/models/sparse/StandardRewardModel.h"
18#include "storm/settings/SettingsManager.h"
19#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
20
21#include "storm/settings/modules/GeneralSettings.h"
22
23#include "storm-parsers/parser/AutoParser.h"
24#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
25#include "storm/settings/modules/NativeEquationSolverSettings.h"
26
27namespace {
28
29class SparseValueTypeValueIterationEnvironment {
30 public:
31 static const bool isExact = false;
32 typedef double ValueType;
33 typedef storm::models::sparse::Mdp<ValueType> ModelType;
34 static storm::Environment createEnvironment() {
35 storm::Environment env;
36 env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration);
37 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
38 return env;
39 }
40};
41
42class SparseValueTypeLinearProgrammingEnvironment {
43 public:
44 static const bool isExact = false;
45 typedef double ValueType;
46 typedef storm::models::sparse::Mdp<ValueType> ModelType;
47 static storm::Environment createEnvironment() {
48 storm::Environment env;
49 env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::LinearProgramming);
50 env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
51 return env;
52 }
53};
54
55class SparseSoundEnvironment {
56 public:
57 static const bool isExact = false;
58 typedef double ValueType;
59 typedef storm::models::sparse::Mdp<ValueType> ModelType;
60 static storm::Environment createEnvironment() {
61 storm::Environment env;
62 env.solver().setForceSoundness(true);
63 return env;
64 }
65};
66
67class SparseRationalLinearProgrammingEnvironment {
68 public:
69 static const bool isExact = true;
70 typedef storm::RationalNumber ValueType;
71 typedef storm::models::sparse::Mdp<ValueType> ModelType;
72 static storm::Environment createEnvironment() {
73 storm::Environment env;
74 env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::LinearProgramming);
75 return env;
76 }
77};
78
79template<typename TestType>
80class LraMdpPrctlModelCheckerTest : public ::testing::Test {
81 public:
82 typedef typename TestType::ValueType ValueType;
83 typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
84
85 LraMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
86
87 void SetUp() override {
88#ifndef STORM_HAVE_Z3
89 GTEST_SKIP() << "Z3 not available.";
90#endif
91 }
92
93 storm::Environment const& env() const {
94 return _environment;
95 }
96 ValueType parseNumber(std::string const& input) const {
97 return storm::utility::convertNumber<ValueType>(input);
98 }
99 ValueType precision() const {
100 return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");
101 }
102 bool isSparseModel() const {
103 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
104 }
105
106 std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(
107 std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
108 std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
109 storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
110 program = storm::utility::prism::preprocess(program, constantDefinitionString);
111 result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
112 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<SparseModelType>();
113 return result;
114 }
115
116 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
117 std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
118 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
119 for (auto const& f : formulas) {
120 result.emplace_back(*f);
121 }
122 return result;
123 }
124
125 private:
126 storm::Environment _environment;
127};
128
129typedef ::testing::Types<SparseValueTypeValueIterationEnvironment, SparseValueTypeLinearProgrammingEnvironment, SparseSoundEnvironment
130#ifdef STORM_HAVE_Z3_OPTIMIZE
131 ,
132 SparseRationalLinearProgrammingEnvironment
133#endif
134 >
135 TestingTypes;
136
137TYPED_TEST_SUITE(LraMdpPrctlModelCheckerTest, TestingTypes, );
138
139TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) {
140 typedef typename TestFixture::ValueType ValueType;
141
142 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
143 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
144
145 // A parser that we use for conveniently constructing the formulas.
146 storm::parser::FormulaParser formulaParser;
147
148 {
149 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
150 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
151 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
152 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
153
154 storm::models::sparse::StateLabeling ap(2);
155 ap.addLabel("a");
156 ap.addLabelToState("a", 1);
157
158 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
159
160 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
161
162 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
163
164 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
165 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
166
167 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
168 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
169
170 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
171
172 result = checker.check(this->env(), *formula);
173 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
174
175 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
176 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
177 }
178 {
179 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
180 matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
181 matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
182 matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
183 matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
184 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
185
186 storm::models::sparse::StateLabeling ap(2);
187 ap.addLabel("a");
188 ap.addLabelToState("a", 1);
189
190 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
191
192 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
193
194 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
195
196 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
197 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
198
199 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
200 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
201
202 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
203
204 result = checker.check(this->env(), *formula);
205 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
206
207 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
208 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
209 }
210 {
211 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
212 matrixBuilder.newRowGroup(0);
213 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
214 matrixBuilder.newRowGroup(1);
215 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
216 matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
217 matrixBuilder.newRowGroup(3);
218 matrixBuilder.addNextValue(3, 0, this->parseNumber("1"));
219 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
220
221 storm::models::sparse::StateLabeling ap(3);
222 ap.addLabel("a");
223 ap.addLabelToState("a", 2);
224 ap.addLabel("b");
225 ap.addLabelToState("b", 0);
226 ap.addLabel("c");
227 ap.addLabelToState("c", 0);
228 ap.addLabelToState("c", 2);
229
230 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
231
232 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
233
234 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
235
236 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
237 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
238
239 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
240 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
241 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
242
243 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
244
245 result = checker.check(this->env(), *formula);
246 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
247
248 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
249 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
250 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
251
252 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
253
254 result = checker.check(this->env(), *formula);
255 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
256
257 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision());
258 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision());
259 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision());
260
261 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
262
263 result = checker.check(this->env(), *formula);
264 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
265
266 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision());
267 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision());
268 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision());
269
270 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
271
272 result = checker.check(this->env(), *formula);
273 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
274
275 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision());
276 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision());
277 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision());
278
279 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
280
281 result = checker.check(this->env(), *formula);
282 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
283
284 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision());
285 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision());
286 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision());
287 }
288}
289
290TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) {
291 typedef typename TestFixture::ValueType ValueType;
292
293 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
294 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
295
296 // A parser that we use for conveniently constructing the formulas.
297 storm::parser::FormulaParser formulaParser;
298
299 {
300 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
301 matrixBuilder.newRowGroup(0);
302 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
303 matrixBuilder.newRowGroup(1);
304 matrixBuilder.addNextValue(1, 1, this->parseNumber("1"));
305 matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
306 matrixBuilder.newRowGroup(3);
307 matrixBuilder.addNextValue(3, 2, this->parseNumber("1"));
308 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
309
310 storm::models::sparse::StateLabeling ap(3);
311 ap.addLabel("a");
312 ap.addLabelToState("a", 0);
313 ap.addLabel("b");
314 ap.addLabelToState("b", 1);
315 ap.addLabel("c");
316 ap.addLabelToState("c", 2);
317
318 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
319
320 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
321
322 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
323
324 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
325 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
326
327 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision());
328 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision());
329 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision());
330
331 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
332
333 result = checker.check(this->env(), *formula);
334 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
335
336 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
337 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
338 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
339
340 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
341
342 result = checker.check(this->env(), *formula);
343 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
344
345 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision());
346 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision());
347 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision());
348
349 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
350
351 result = checker.check(this->env(), *formula);
352 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
353
354 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision());
355 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision());
356 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision());
357
358 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
359
360 result = checker.check(this->env(), *formula);
361 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
362
363 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision());
364 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision());
365 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision());
366
367 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
368
369 result = checker.check(this->env(), *formula);
370 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
371
372 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision());
373 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision());
374 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision());
375 }
376 {
377 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(22, 15, 28, true, true, 15);
378 matrixBuilder.newRowGroup(0);
379 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
380 matrixBuilder.newRowGroup(1);
381 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
382 matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
383 matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7"));
384 matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3"));
385 matrixBuilder.newRowGroup(4);
386 matrixBuilder.addNextValue(4, 0, this->parseNumber("1"));
387
388 matrixBuilder.newRowGroup(5);
389 matrixBuilder.addNextValue(5, 4, this->parseNumber("1"));
390 matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8"));
391 matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2"));
392 matrixBuilder.newRowGroup(7);
393 matrixBuilder.addNextValue(7, 3, this->parseNumber("1"));
394 matrixBuilder.addNextValue(8, 5, this->parseNumber("1"));
395 matrixBuilder.newRowGroup(9);
396 matrixBuilder.addNextValue(9, 3, this->parseNumber("1"));
397
398 matrixBuilder.newRowGroup(10);
399 matrixBuilder.addNextValue(10, 7, this->parseNumber("1"));
400 matrixBuilder.newRowGroup(11);
401 matrixBuilder.addNextValue(11, 6, this->parseNumber("1"));
402 matrixBuilder.addNextValue(12, 8, this->parseNumber("1"));
403 matrixBuilder.newRowGroup(13);
404 matrixBuilder.addNextValue(13, 6, this->parseNumber("1"));
405
406 matrixBuilder.newRowGroup(14);
407 matrixBuilder.addNextValue(14, 10, this->parseNumber("1"));
408 matrixBuilder.newRowGroup(15);
409 matrixBuilder.addNextValue(15, 9, this->parseNumber("1"));
410 matrixBuilder.addNextValue(16, 11, this->parseNumber("1"));
411 matrixBuilder.newRowGroup(17);
412 matrixBuilder.addNextValue(17, 9, this->parseNumber("1"));
413
414 matrixBuilder.newRowGroup(18);
415 matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4"));
416 matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3"));
417 matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3"));
418
419 matrixBuilder.newRowGroup(19);
420 matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7"));
421 matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3"));
422
423 matrixBuilder.newRowGroup(20);
424 matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1"));
425 matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9"));
426 matrixBuilder.addNextValue(21, 12, this->parseNumber("1"));
427
428 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
429
430 storm::models::sparse::StateLabeling ap(15);
431 ap.addLabel("a");
432 ap.addLabelToState("a", 1);
433 ap.addLabelToState("a", 4);
434 ap.addLabelToState("a", 5);
435 ap.addLabelToState("a", 7);
436 ap.addLabelToState("a", 11);
437 ap.addLabelToState("a", 13);
438 ap.addLabelToState("a", 14);
439
440 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
441
442 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
443
444 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
445
446 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
447 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
448
449 EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision());
450 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision());
451 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision());
452 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision());
453 EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision());
454 EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision());
455 EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision());
456
457 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
458
459 result = checker.check(this->env(), *formula);
460 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
461
462 EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision());
463 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision());
464 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision());
465 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision());
466 EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision());
467 EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision());
468 EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision());
469 }
470}
471
472TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) {
473 typedef typename TestFixture::ValueType ValueType;
474
475 std::string formulasString = "R{\"grants\"}max=? [ MP ]; R{\"grants\"}min=? [ MP ];";
476
477 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
478 auto model = std::move(modelFormulas.first);
479 auto tasks = this->getTasks(modelFormulas.second);
480 EXPECT_EQ(184ul, model->getNumberOfStates());
481 EXPECT_EQ(541ul, model->getNumberOfTransitions());
482 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
483 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
484 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
485
486 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
487 EXPECT_NEAR(this->parseNumber("333/1000"), result[*mdp->getInitialStates().begin()], this->precision());
488
489 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
490 EXPECT_NEAR(this->parseNumber("0"), result[*mdp->getInitialStates().begin()], this->precision());
491}
492
493} // namespace
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::LongRunAverageSolverEnvironment::setNondetLraMethod
void setNondetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault=false)
Definition LongRunAverageSolverEnvironment.cpp:49
storm::SolverEnvironment::lra
LongRunAverageSolverEnvironment & lra()
Definition SolverEnvironment.cpp:27
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:94
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
storm::models::sparse::StateLabeling
This class manages the labeling of the state space with a number of (atomic) labels.
Definition StateLabeling.h:19
storm::parser::FormulaParser::parseSingleFormulaFromString
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
Definition FormulaParser.cpp:55
storm::storage::SparseMatrixBuilder
A class that can be used to build a sparse matrix by adding value by value.
Definition SparseMatrix.h:137
storm::storage::SparseMatrixBuilder::addNextValue
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
Definition SparseMatrix.cpp:156
storm::storage::SparseMatrixBuilder::newRowGroup
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
Definition SparseMatrix.cpp:253
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:281
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:332
model_descriptions.h
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:13
storm::parser::parseNumber
NumberType parseNumber(std::string const &value)
Parse number from string.
Definition ValueParser.cpp:53
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
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