Storm 1.12.0.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 SparseRationalLinearProgrammingEnvironment>
125 TestingTypes;
126
127TYPED_TEST_SUITE(LraMdpPrctlModelCheckerTest, TestingTypes, );
128
129TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) {
130 typedef typename TestFixture::ValueType ValueType;
131
132 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
133 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
134
135 // A parser that we use for conveniently constructing the formulas.
136 storm::parser::FormulaParser formulaParser;
137
138 {
139 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
140 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
141 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
142 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
143
144 storm::models::sparse::StateLabeling ap(2);
145 ap.addLabel("a");
146 ap.addLabelToState("a", 1);
147
148 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
149
150 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
151
152 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
153
154 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
155 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
156
157 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
158 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
159
160 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
161
162 result = checker.check(this->env(), *formula);
163 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
164
165 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
166 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
167 }
168 {
169 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
170 matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
171 matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
172 matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
173 matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
174 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
175
176 storm::models::sparse::StateLabeling ap(2);
177 ap.addLabel("a");
178 ap.addLabelToState("a", 1);
179
180 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
181
182 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
183
184 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
185
186 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
187 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
188
189 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
190 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
191
192 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
193
194 result = checker.check(this->env(), *formula);
195 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
196
197 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
198 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
199 }
200 {
201 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
202 matrixBuilder.newRowGroup(0);
203 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
204 matrixBuilder.newRowGroup(1);
205 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
206 matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
207 matrixBuilder.newRowGroup(3);
208 matrixBuilder.addNextValue(3, 0, this->parseNumber("1"));
209 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
210
211 storm::models::sparse::StateLabeling ap(3);
212 ap.addLabel("a");
213 ap.addLabelToState("a", 2);
214 ap.addLabel("b");
215 ap.addLabelToState("b", 0);
216 ap.addLabel("c");
217 ap.addLabelToState("c", 0);
218 ap.addLabelToState("c", 2);
219
220 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
221
222 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
223
224 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
225
226 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
227 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
228
229 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
230 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
231 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
232
233 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
234
235 result = checker.check(this->env(), *formula);
236 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
237
238 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
239 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
240 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
241
242 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
243
244 result = checker.check(this->env(), *formula);
245 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
246
247 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision());
248 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision());
249 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision());
250
251 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
252
253 result = checker.check(this->env(), *formula);
254 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
255
256 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision());
257 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision());
258 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision());
259
260 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
261
262 result = checker.check(this->env(), *formula);
263 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
264
265 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision());
266 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision());
267 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision());
268
269 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
270
271 result = checker.check(this->env(), *formula);
272 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
273
274 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision());
275 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision());
276 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision());
277 }
278}
279
280TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) {
281 typedef typename TestFixture::ValueType ValueType;
282
283 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
284 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
285
286 // A parser that we use for conveniently constructing the formulas.
287 storm::parser::FormulaParser formulaParser;
288
289 {
290 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
291 matrixBuilder.newRowGroup(0);
292 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
293 matrixBuilder.newRowGroup(1);
294 matrixBuilder.addNextValue(1, 1, this->parseNumber("1"));
295 matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
296 matrixBuilder.newRowGroup(3);
297 matrixBuilder.addNextValue(3, 2, this->parseNumber("1"));
298 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
299
300 storm::models::sparse::StateLabeling ap(3);
301 ap.addLabel("a");
302 ap.addLabelToState("a", 0);
303 ap.addLabel("b");
304 ap.addLabelToState("b", 1);
305 ap.addLabel("c");
306 ap.addLabelToState("c", 2);
307
308 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
309
310 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
311
312 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
313
314 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
315 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
316
317 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision());
318 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision());
319 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision());
320
321 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
322
323 result = checker.check(this->env(), *formula);
324 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
325
326 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
327 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
328 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
329
330 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
331
332 result = checker.check(this->env(), *formula);
333 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
334
335 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision());
336 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision());
337 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision());
338
339 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
340
341 result = checker.check(this->env(), *formula);
342 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
343
344 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision());
345 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision());
346 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision());
347
348 formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
349
350 result = checker.check(this->env(), *formula);
351 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
352
353 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision());
354 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision());
355 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision());
356
357 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
358
359 result = checker.check(this->env(), *formula);
360 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
361
362 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision());
363 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision());
364 EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision());
365 }
366 {
367 matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(22, 15, 28, true, true, 15);
368 matrixBuilder.newRowGroup(0);
369 matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
370 matrixBuilder.newRowGroup(1);
371 matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
372 matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
373 matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7"));
374 matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3"));
375 matrixBuilder.newRowGroup(4);
376 matrixBuilder.addNextValue(4, 0, this->parseNumber("1"));
377
378 matrixBuilder.newRowGroup(5);
379 matrixBuilder.addNextValue(5, 4, this->parseNumber("1"));
380 matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8"));
381 matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2"));
382 matrixBuilder.newRowGroup(7);
383 matrixBuilder.addNextValue(7, 3, this->parseNumber("1"));
384 matrixBuilder.addNextValue(8, 5, this->parseNumber("1"));
385 matrixBuilder.newRowGroup(9);
386 matrixBuilder.addNextValue(9, 3, this->parseNumber("1"));
387
388 matrixBuilder.newRowGroup(10);
389 matrixBuilder.addNextValue(10, 7, this->parseNumber("1"));
390 matrixBuilder.newRowGroup(11);
391 matrixBuilder.addNextValue(11, 6, this->parseNumber("1"));
392 matrixBuilder.addNextValue(12, 8, this->parseNumber("1"));
393 matrixBuilder.newRowGroup(13);
394 matrixBuilder.addNextValue(13, 6, this->parseNumber("1"));
395
396 matrixBuilder.newRowGroup(14);
397 matrixBuilder.addNextValue(14, 10, this->parseNumber("1"));
398 matrixBuilder.newRowGroup(15);
399 matrixBuilder.addNextValue(15, 9, this->parseNumber("1"));
400 matrixBuilder.addNextValue(16, 11, this->parseNumber("1"));
401 matrixBuilder.newRowGroup(17);
402 matrixBuilder.addNextValue(17, 9, this->parseNumber("1"));
403
404 matrixBuilder.newRowGroup(18);
405 matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4"));
406 matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3"));
407 matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3"));
408
409 matrixBuilder.newRowGroup(19);
410 matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7"));
411 matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3"));
412
413 matrixBuilder.newRowGroup(20);
414 matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1"));
415 matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9"));
416 matrixBuilder.addNextValue(21, 12, this->parseNumber("1"));
417
418 storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
419
420 storm::models::sparse::StateLabeling ap(15);
421 ap.addLabel("a");
422 ap.addLabelToState("a", 1);
423 ap.addLabelToState("a", 4);
424 ap.addLabelToState("a", 5);
425 ap.addLabelToState("a", 7);
426 ap.addLabelToState("a", 11);
427 ap.addLabelToState("a", 13);
428 ap.addLabelToState("a", 14);
429
430 mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
431
432 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
433
434 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
435
436 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
437 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
438
439 EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision());
440 EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision());
441 EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision());
442 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision());
443 EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision());
444 EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision());
445 EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision());
446
447 formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
448
449 result = checker.check(this->env(), *formula);
450 storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
451
452 EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision());
453 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision());
454 EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision());
455 EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision());
456 EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision());
457 EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision());
458 EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision());
459 }
460}
461
462TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) {
463 typedef typename TestFixture::ValueType ValueType;
464
465 std::string formulasString = "R{\"grants\"}max=? [ MP ]; R{\"grants\"}min=? [ MP ];";
466
467 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
468 auto model = std::move(modelFormulas.first);
469 auto tasks = this->getTasks(modelFormulas.second);
470 EXPECT_EQ(184ul, model->getNumberOfStates());
471 EXPECT_EQ(541ul, model->getNumberOfTransitions());
472 ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
473 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
474 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
475
476 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
477 EXPECT_NEAR(this->parseNumber("333/1000"), result[*mdp->getInitialStates().begin()], this->precision());
478
479 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
480 EXPECT_NEAR(this->parseNumber("0"), result[*mdp->getInitialStates().begin()], this->precision());
481}
482
483} // 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:92
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:134
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:154
storm::storage::SparseMatrixBuilder::newRowGroup
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
Definition SparseMatrix.cpp:251
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:279
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:329
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:55
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:13
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