Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/api/storm-parsers.h"
5#include "storm/api/storm.h"
6#include "storm/environment/Environment.h"
7#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
8#include "storm/environment/solver/MinMaxSolverEnvironment.h"
9#include "storm/modelchecker/multiobjective/MultiObjectiveModelChecking.h"
10#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
11#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
12#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
13#include "storm/models/sparse/Mdp.h"
14#include "storm/storage/jani/Property.h"
15#include "storm/utility/constants.h"
16
17class SparseMdpMultiDimensionalRewardUnfoldingTest : public ::testing::Test {
18 protected:
19 void SetUp() override {
20#ifndef STORM_HAVE_Z3
21 GTEST_SKIP() << "Z3 not available.";
22#endif
23 }
24};
25
26TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small) {
27 storm::Environment env;
28 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
29 std::string constantsDef = "N=2";
30 std::string formulasAsString = "Pmax=? [ F{\"r\"}<=1 x=N ] ";
31 formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]";
32 formulasAsString += "; \n Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]";
33 formulasAsString += "; \n Pmax=? [ F{\"r\"}>=1 x=N ] ";
34 formulasAsString += "; \n Pmax=? [ F{\"r\"}>=3 x=N ] ";
35 formulasAsString += "; \n Pmin=? [ F{\"r\"}>=2 x=N ] ";
36 formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}>=1 x=N, F{\"l\"}>=2 x=0 )]";
37
38 // programm, model, formula
39 storm::prism::Program program = storm::api::parseProgram(programFile);
40 program = storm::utility::prism::preprocess(program, constantsDef);
41 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
42 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
43 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
44 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
45 uint_fast64_t const initState = *mdp->getInitialStates().begin();
46 std::unique_ptr<storm::modelchecker::CheckResult> result;
47
48 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
49 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
50 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
51
52 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
53 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
54 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
55
56 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
57 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
58 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
59
60 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
61 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
62 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
63
64 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
65 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
66 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
67
68 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
69 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
70 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
71
72 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
73 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
74 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
75}
76
77TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) {
78 storm::Environment env;
79
80 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
81 std::string constantsDef = "N=10";
82 std::string formulasAsString = "Pmax=? [ F{\"r\"}<=5 x=N ] ";
83 formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )]";
84
85 // programm, model, formula
86 storm::prism::Program program = storm::api::parseProgram(programFile);
87 program = storm::utility::prism::preprocess(program, constantsDef);
88 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
89 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
90 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
91 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
92 uint_fast64_t const initState = *mdp->getInitialStates().begin();
93
94 std::unique_ptr<storm::modelchecker::CheckResult> result;
95
96 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
97
98 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
99 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
100 storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
101 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
102
103 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
104 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
105 expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
106 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
107}
108
109TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) {
110 storm::Environment env;
111
112 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm";
113 std::string constantsDef = "";
114 std::string formulasAsString = "Pmax=? [ F{\"a\"}<=3 x=4 ] "; // 0.2
115 formulasAsString += "; \n Pmin=? [ F{\"a\"}<=3 x=4 ] "; // 0.0
116 formulasAsString += "; \n Pmin=? [ F{\"a\"}<1 x=1 ] "; // 0.0
117 formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.02
118 formulasAsString += "; \n Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.0
119 formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )] "; // 0.02
120 formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )] "; // 0.02
121
122 // programm, model, formula
123 storm::prism::Program program = storm::api::parseProgram(programFile);
124 program = storm::utility::prism::preprocess(program, constantsDef);
125 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
126 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
127 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
128 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
129 uint_fast64_t const initState = *mdp->getInitialStates().begin();
130
131 std::unique_ptr<storm::modelchecker::CheckResult> result;
132
133 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
134
135 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
136 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
137 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/5");
138 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
139
140 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
141 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
142 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
143 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
144
145 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
146 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
147 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
148 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
149
150 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
151 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
152 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
153 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
154
155 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
156 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
157 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
158 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
159
160 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
161 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
162 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
163 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
164
165 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
166 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
167 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
168 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
169}
170
171TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) {
172 storm::Environment env;
173 auto const prec = storm::utility::convertNumber<double>(env.modelchecker().multi().getPrecision());
174
175 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
176 std::string constantsDef = "N=1000,K=2,reset=true";
177 std::string formulasAsString = "Pmin=? [ F{\"t\"}<50 \"ipfound\" ]";
178 formulasAsString += "; \n Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ]";
179
180 // programm, model, formula
181 storm::prism::Program program = storm::api::parseProgram(programFile);
182 program = storm::utility::prism::preprocess(program, constantsDef);
183 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
184 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
185 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
186 uint_fast64_t const initState = *mdp->getInitialStates().begin();
187
188 std::unique_ptr<storm::modelchecker::CheckResult> result;
189
190 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp);
191
192 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<double>(formulas[0], true));
193 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
194 EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult<double>()[initState], prec);
195
196 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<double>(formulas[1], true));
197 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
198 EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult<double>()[initState], prec);
199}
200
201TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) {
202 storm::Environment env;
203
204 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm";
205 std::string constantsDef = "";
206 std::string formulasAsString = "Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ]";
207
208 // programm, model, formula
209 storm::prism::Program program = storm::api::parseProgram(programFile);
210 program = storm::utility::prism::preprocess(program, constantsDef);
211 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
212 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
213 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
214 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
215 uint_fast64_t const initState = *mdp->getInitialStates().begin();
216
217 std::unique_ptr<storm::modelchecker::CheckResult> result;
218
219 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
220
221 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
222 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
223 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832");
224 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
225}
226
227TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) {
228 storm::Environment env;
229
230 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm";
231 std::string constantsDef = "";
232 std::string formulasAsString = "Pmax=? [ F{\"a\"}>=1.1 x=1 ]";
233 formulasAsString += "; \n Pmin=? [ F{\"a\"}>=1.1 x=1 ]";
234 formulasAsString += "; \n Pmax=? [ F{\"b\"}>3 x=1 ]";
235 formulasAsString += "; \n Pmax=? [ F{\"b\"}>=2 x=0 ]";
236 formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}<=0.2 x=1, F{\"b\"}>3 x=1) ]";
237 formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>0.2 x=1, F{\"b\"}>3 x=1) ]";
238 formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4) ]";
239
240 // programm, model, formula
241 storm::prism::Program program = storm::api::parseProgram(programFile);
242 program = storm::utility::prism::preprocess(program, constantsDef);
243 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
244 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
245 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
246 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
247 uint_fast64_t const initState = *mdp->getInitialStates().begin();
248
249 std::unique_ptr<storm::modelchecker::CheckResult> result;
250
251 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
252
253 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
254 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
255 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/100");
256 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
257
258 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
259 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
260 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
261 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
262
263 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
264 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
265 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64");
266 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
267
268 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
269 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
270 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("9/16");
271 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
272
273 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
274 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
275 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64");
276 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
277
278 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
279 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
280 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640");
281 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
282
283 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
284 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
285 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/160");
286 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
287}
288
289TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) {
290 storm::Environment env;
291 env.solver().setForceExact(true);
292 auto const prec = env.modelchecker().multi().getPrecision();
293
294 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
295 std::string constantsDef = "N=2";
296 std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=1 x=N ]) ";
297 formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])";
298 formulasAsString += "; \n multi(Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])";
299 formulasAsString += "; \n multi(Pmax=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])";
300 formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])";
301 formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmin=? [ F{\"l\"}<=2 x=0])";
302
303 // programm, model, formula
304 storm::prism::Program program = storm::api::parseProgram(programFile);
305 program = storm::utility::prism::preprocess(program, constantsDef);
306 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
307 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
308 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
309 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
310 uint_fast64_t const initState = *mdp->getInitialStates().begin();
311
312 std::unique_ptr<storm::modelchecker::CheckResult> result;
313
314 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
315 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
316 EXPECT_NEAR(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
317
318 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
319 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
320 EXPECT_NEAR(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState],
321 prec);
322
323 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
324 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
325 EXPECT_NEAR(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
326
327 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
328 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
329 std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber>(0.5),
330 storm::utility::convertNumber<storm::RationalNumber>(0.5)};
331 std::vector<storm::RationalNumber> q1 = {storm::utility::convertNumber<storm::RationalNumber>(0.125),
332 storm::utility::convertNumber<storm::RationalNumber>(0.75)};
333 auto expectedAchievableValues =
334 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1, q1}));
335
336 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
337 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
338
339 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula());
340 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
341 std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber>(0.0),
342 storm::utility::convertNumber<storm::RationalNumber>(0.75)};
343 expectedAchievableValues =
344 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2}));
345 std::vector<std::vector<storm::RationalNumber>> transformationMatrix(2,
346 std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
347 transformationMatrix[0][0] = -storm::utility::one<storm::RationalNumber>();
348 transformationMatrix[1][1] = storm::utility::one<storm::RationalNumber>();
349 expectedAchievableValues = expectedAchievableValues->affineTransformation(
350 transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
351 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
352 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
353
354 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula());
355 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
356 std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber>(0.0),
357 storm::utility::convertNumber<storm::RationalNumber>(-0.75)};
358 std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber>(-0.5),
359 storm::utility::convertNumber<storm::RationalNumber>(0.0)};
360 expectedAchievableValues =
361 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3, q3}));
362 transformationMatrix[1][1] = -storm::utility::one<storm::RationalNumber>();
363 expectedAchievableValues = expectedAchievableValues->affineTransformation(
364 transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
365 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
366 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
367}
368
369TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) {
370 storm::Environment env;
371 env.solver().setForceExact(true);
372 auto const prec = env.modelchecker().multi().getPrecision();
373
374 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
375 std::string constantsDef = "N=10";
376 std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=5 x=N ]) ";
377 formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )])";
378 formulasAsString += "; \n multi(P>=1/512 [ F{\"r\"}<=5 x=N], Pmax=? [ F{\"l\"}<=10 x=0])";
379
380 // programm, model, formula
381 storm::prism::Program program = storm::api::parseProgram(programFile);
382 program = storm::utility::prism::preprocess(program, constantsDef);
383 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
384 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
385 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
386 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
387 uint_fast64_t const initState = *mdp->getInitialStates().begin();
388
389 std::unique_ptr<storm::modelchecker::CheckResult> result;
390
391 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
392 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
393 storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
394 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
395
396 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
397 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
398 expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
399 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
400
401 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
402 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
403 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("2539/4096");
404 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
405}
406
407TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) {
408 storm::Environment env;
409 env.solver().setForceExact(true);
410 auto const prec = env.modelchecker().multi().getPrecision();
411
412 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm";
413 std::string constantsDef = "";
414 std::string formulasAsString = "multi(Pmax=? [ F{\"a\"}<=3 x=4 ]) "; // 0.2
415 formulasAsString += "; \n multi(Pmin=? [ F{\"a\"}<=3 x=4 ]) "; // 0.0
416 formulasAsString += "; \n multi(Pmin=? [ F{\"a\"}<1 x=1 ]) "; // 0.0
417 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )]) "; // 0.02
418 formulasAsString += "; \n multi(Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )]) "; // 0.0
419 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )]) "; // 0.02
420 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )]) "; // 0.02
421 formulasAsString +=
422 "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"c\"}<1/2 x=5 )], Pmax=? [multi( F{\"b\"}<=0 x=3, F{\"c\"}<=4/5 x=5 )]) "; // (0.1, 0) , (0, 0.19)
423
424 // programm, model, formula
425 storm::prism::Program program = storm::api::parseProgram(programFile);
426 program = storm::utility::prism::preprocess(program, constantsDef);
427 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
428 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
429 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
430 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
431 uint_fast64_t const initState = *mdp->getInitialStates().begin();
432
433 std::unique_ptr<storm::modelchecker::CheckResult> result;
434
435 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
436 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
437 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/5");
438 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
439
440 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
441 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
442 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
443 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
444
445 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
446 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
447 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
448 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
449
450 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
451 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
452 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
453 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
454
455 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula());
456 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
457 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
458 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
459
460 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula());
461 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
462 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
463 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
464
465 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[6]->asMultiObjectiveFormula());
466 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
467 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
468 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
469
470 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[7]->asMultiObjectiveFormula());
471 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
472 std::vector<storm::RationalNumber> p = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1/10"),
473 storm::utility::convertNumber<storm::RationalNumber, std::string>("0")};
474 std::vector<storm::RationalNumber> q = {storm::utility::convertNumber<storm::RationalNumber, std::string>("0"),
475 storm::utility::convertNumber<storm::RationalNumber, std::string>("19/100")};
476 auto expectedAchievableValues =
477 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p, q}));
478
479 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
480 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
481}
482
483TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) {
484 storm::Environment env;
485 auto const prec = storm::utility::convertNumber<double>(env.modelchecker().multi().getPrecision());
486
487 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
488 std::string constantsDef = "N=1000,K=2,reset=true";
489 std::string formulasAsString = "multi(Pmin=? [ F{\"t\"}<50 \"ipfound\" ])";
490 formulasAsString += "; \n multi(Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ])";
491
492 // programm, model, formula
493 storm::prism::Program program = storm::api::parseProgram(programFile);
494 program = storm::utility::prism::preprocess(program, constantsDef);
495 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
496 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
497 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
498 uint_fast64_t const initState = *mdp->getInitialStates().begin();
499
500 std::unique_ptr<storm::modelchecker::CheckResult> result;
501
502 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
503 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
504 EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult<double>()[initState], prec);
505
506 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
507 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
508 EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult<double>()[initState], prec);
509}
510
511TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) {
512 storm::Environment env;
513 env.solver().setForceExact(true);
514 auto const prec = env.modelchecker().multi().getPrecision();
515
516 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm";
517 std::string constantsDef = "";
518 std::string formulasAsString = "multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ])";
519 formulasAsString += "; \n multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ], Pmax=? [ !\"collision_max_backoff\" U \"all_delivered\"] )";
520
521 // programm, model, formula
522 storm::prism::Program program = storm::api::parseProgram(programFile);
523 program = storm::utility::prism::preprocess(program, constantsDef);
524 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
525 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
526 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
527 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
528 uint_fast64_t const initState = *mdp->getInitialStates().begin();
529
530 std::unique_ptr<storm::modelchecker::CheckResult> result;
531
532 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
533 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
534 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832");
535 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
536
537 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
538 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
539 std::vector<storm::RationalNumber> p = {storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832"),
540 storm::utility::convertNumber<storm::RationalNumber, std::string>("7/8")};
541 auto expectedAchievableValues =
542 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p}));
543 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
544 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
545}
546
547TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) {
548 storm::Environment env;
549 env.solver().setForceExact(true);
550 auto const prec = env.modelchecker().multi().getPrecision();
551
552 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm";
553 std::string constantsDef = "";
554 std::string formulasAsString = "multi(Pmax=? [ F{\"a\"}>=1.1 x=1 ])";
555 formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}<=0.2 x=1], Pmax=? [F{\"b\"}>3 x=1 ])";
556 formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}>0.2 x=1 ], Pmax=? [F{\"b\"}>3 x=1 ])";
557 formulasAsString += "; \n multi(Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4)], Pmax=? [F {\"b\"}>3 x = 1])";
558
559 // programm, model, formula
560 storm::prism::Program program = storm::api::parseProgram(programFile);
561 program = storm::utility::prism::preprocess(program, constantsDef);
562 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
563 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
564 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
565 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
566 uint_fast64_t const initState = *mdp->getInitialStates().begin();
567
568 std::unique_ptr<storm::modelchecker::CheckResult> result;
569
570 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
571
572 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
573 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
574 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/100");
575 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
576
577 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
578 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
579 std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1"),
580 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
581 auto expectedAchievableValues =
582 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1}));
583 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
584 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
585
586 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
587 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
588 std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1"),
589 storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640")};
590 std::vector<storm::RationalNumber> q2 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("81/256"),
591 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
592 expectedAchievableValues =
593 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2, q2}));
594 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
595 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
596
597 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
598 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
599 std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("81/160"),
600 storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640")};
601 std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("2187/10240"),
602 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
603 expectedAchievableValues =
604 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3, q3}));
605 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
606 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
607}
TEST_F
TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small)
Definition SparseMdpMultiDimensionalRewardUnfoldingTest.cpp:26
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::Environment::modelchecker
ModelCheckerEnvironment & modelchecker()
Definition Environment.cpp:33
storm::ModelCheckerEnvironment::multi
MultiObjectiveModelCheckerEnvironment & multi()
Definition ModelCheckerEnvironment.cpp:45
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::models::sparse::Model::getInitialStates
storm::storage::BitVector const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:178
storm::storage::BitVector::begin
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
Definition BitVector.cpp:769
storm::storage::geometry::Polytope::createDownwardClosure
static std::shared_ptr< Polytope< ValueType > > createDownwardClosure(std::vector< Point > const &points)
Creates the downward closure of the given points (i.e., the set { x | ex.
Definition Polytope.cpp:40
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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
storm::api::createTask
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > createTask(std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)
Definition verification.h:46
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::api::verifyWithSparseEngine
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
Definition verification.h:105
storm::modelchecker::multiobjective::performMultiObjectiveModelChecking
std::unique_ptr< CheckResult > performMultiObjectiveModelChecking(Environment const &env, SparseModelType const &model, storm::logic::MultiObjectiveFormula const &formula, bool produceScheduler)
Definition MultiObjectiveModelChecking.cpp:28
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
storm::utility::zero
ValueType zero()
Definition constants.cpp:24
storm::utility::pow
ValueType pow(ValueType const &value, int_fast64_t exponent)
Definition constants.cpp:243
storm::utility::one
ValueType one()
Definition constants.cpp:19
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:135
storm_gtest.h