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