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