Storm 1.11.1.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/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 std::unique_ptr<storm::modelchecker::CheckResult> result;
48
49 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
50 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
51 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
52
53 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
54 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
55 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
56
57 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
58 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
59 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
60
61 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
62 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
63 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
64
65 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
66 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
67 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
68
69 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
70 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
71 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
72
73 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
74 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
75 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
76}
77
78TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) {
79 storm::Environment env;
80
81 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
82 std::string constantsDef = "N=10";
83 std::string formulasAsString = "Pmax=? [ F{\"r\"}<=5 x=N ] ";
84 formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )]";
85
86 // programm, model, formula
87 storm::prism::Program program = storm::api::parseProgram(programFile);
88 program = storm::utility::prism::preprocess(program, constantsDef);
89 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
90 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
91 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
92 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
93 uint_fast64_t const initState = *mdp->getInitialStates().begin();
94
95 std::unique_ptr<storm::modelchecker::CheckResult> result;
96
97 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
98
99 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
100 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
101 storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
102 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
103
104 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
105 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
106 expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
107 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
108}
109
110TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) {
111 storm::Environment env;
112
113 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm";
114 std::string constantsDef = "";
115 std::string formulasAsString = "Pmax=? [ F{\"a\"}<=3 x=4 ] "; // 0.2
116 formulasAsString += "; \n Pmin=? [ F{\"a\"}<=3 x=4 ] "; // 0.0
117 formulasAsString += "; \n Pmin=? [ F{\"a\"}<1 x=1 ] "; // 0.0
118 formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.02
119 formulasAsString += "; \n Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.0
120 formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )] "; // 0.02
121 formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )] "; // 0.02
122
123 // programm, model, formula
124 storm::prism::Program program = storm::api::parseProgram(programFile);
125 program = storm::utility::prism::preprocess(program, constantsDef);
126 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
127 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
128 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
129 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
130 uint_fast64_t const initState = *mdp->getInitialStates().begin();
131
132 std::unique_ptr<storm::modelchecker::CheckResult> result;
133
134 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
135
136 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
137 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
138 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/5");
139 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
140
141 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
142 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
143 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
144 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
145
146 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
147 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
148 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
149 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
150
151 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
152 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
153 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
154 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
155
156 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
157 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
158 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
159 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
160
161 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
162 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
163 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
164 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
165
166 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
167 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
168 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
169 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
170}
171
172TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) {
173 storm::Environment env;
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],
195 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
196
197 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<double>(formulas[1], true));
198 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
199 EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult<double>()[initState],
200 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
201}
202
203TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) {
204 storm::Environment env;
205
206 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm";
207 std::string constantsDef = "";
208 std::string formulasAsString = "Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ]";
209
210 // programm, model, formula
211 storm::prism::Program program = storm::api::parseProgram(programFile);
212 program = storm::utility::prism::preprocess(program, constantsDef);
213 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
214 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
215 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
216 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
217 uint_fast64_t const initState = *mdp->getInitialStates().begin();
218
219 std::unique_ptr<storm::modelchecker::CheckResult> result;
220
221 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
222
223 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
224 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
225 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832");
226 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
227}
228
229TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) {
230 storm::Environment env;
231
232 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm";
233 std::string constantsDef = "";
234 std::string formulasAsString = "Pmax=? [ F{\"a\"}>=1.1 x=1 ]";
235 formulasAsString += "; \n Pmin=? [ F{\"a\"}>=1.1 x=1 ]";
236 formulasAsString += "; \n Pmax=? [ F{\"b\"}>3 x=1 ]";
237 formulasAsString += "; \n Pmax=? [ F{\"b\"}>=2 x=0 ]";
238 formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}<=0.2 x=1, F{\"b\"}>3 x=1) ]";
239 formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>0.2 x=1, F{\"b\"}>3 x=1) ]";
240 formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4) ]";
241
242 // programm, model, formula
243 storm::prism::Program program = storm::api::parseProgram(programFile);
244 program = storm::utility::prism::preprocess(program, constantsDef);
245 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
246 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
247 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
248 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
249 uint_fast64_t const initState = *mdp->getInitialStates().begin();
250
251 std::unique_ptr<storm::modelchecker::CheckResult> result;
252
253 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
254
255 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
256 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
257 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/100");
258 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
259
260 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
261 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
262 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
263 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
264
265 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
266 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
267 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64");
268 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
269
270 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
271 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
272 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("9/16");
273 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
274
275 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
276 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
277 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64");
278 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
279
280 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
281 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
282 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640");
283 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
284
285 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
286 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
287 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/160");
288 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
289}
290
291#ifdef STORM_HAVE_Z3_OPTIMIZE
292
293TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) {
294 storm::Environment env;
295
296 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
297 std::string constantsDef = "N=2";
298 std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=1 x=N ]) ";
299 formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])";
300 formulasAsString += "; \n multi(Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])";
301 formulasAsString += "; \n multi(Pmax=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])";
302 formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])";
303 formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmin=? [ F{\"l\"}<=2 x=0])";
304
305 // programm, model, formula
306 storm::prism::Program program = storm::api::parseProgram(programFile);
307 program = storm::utility::prism::preprocess(program, constantsDef);
308 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
309 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
310 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
311 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
312 uint_fast64_t const initState = *mdp->getInitialStates().begin();
313
314 std::unique_ptr<storm::modelchecker::CheckResult> result;
315
316 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
317 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
318 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
319
320 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
321 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
322 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
323
324 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
325 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
326 EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
327
328 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
329 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
330 std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber>(0.5),
331 storm::utility::convertNumber<storm::RationalNumber>(0.5)};
332 std::vector<storm::RationalNumber> q1 = {storm::utility::convertNumber<storm::RationalNumber>(0.125),
333 storm::utility::convertNumber<storm::RationalNumber>(0.75)};
334 auto expectedAchievableValues =
335 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1, q1}));
336
337 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
338 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
339
340 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula());
341 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
342 std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber>(0.0),
343 storm::utility::convertNumber<storm::RationalNumber>(0.75)};
344 expectedAchievableValues =
345 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2}));
346 std::vector<std::vector<storm::RationalNumber>> transformationMatrix(2,
347 std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
348 transformationMatrix[0][0] = -storm::utility::one<storm::RationalNumber>();
349 transformationMatrix[1][1] = storm::utility::one<storm::RationalNumber>();
350 expectedAchievableValues = expectedAchievableValues->affineTransformation(
351 transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
352 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
353 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
354
355 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula());
356 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
357 std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber>(0.0),
358 storm::utility::convertNumber<storm::RationalNumber>(-0.75)};
359 std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber>(-0.5),
360 storm::utility::convertNumber<storm::RationalNumber>(0.0)};
361 expectedAchievableValues =
362 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3, q3}));
363 transformationMatrix[1][1] = -storm::utility::one<storm::RationalNumber>();
364 expectedAchievableValues = expectedAchievableValues->affineTransformation(
365 transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
366 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
367 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
368}
369
370TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) {
371 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
372 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
373 }
374 storm::Environment env;
375
376 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
377 std::string constantsDef = "N=10";
378 std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=5 x=N ]) ";
379 formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )])";
380 formulasAsString += "; \n multi(P>=1/512 [ F{\"r\"}<=5 x=N], Pmax=? [ F{\"l\"}<=10 x=0])";
381
382 // programm, model, formula
383 storm::prism::Program program = storm::api::parseProgram(programFile);
384 program = storm::utility::prism::preprocess(program, constantsDef);
385 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
386 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
387 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
388 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
389 uint_fast64_t const initState = *mdp->getInitialStates().begin();
390
391 std::unique_ptr<storm::modelchecker::CheckResult> result;
392
393 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
394 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
395 storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
396 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
397
398 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
399 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
400 expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
401 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
402
403 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
404 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
405 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("2539/4096");
406 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
407}
408
409TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) {
410 storm::Environment env;
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
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
486 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
487 std::string constantsDef = "N=1000,K=2,reset=true";
488 std::string formulasAsString = "multi(Pmin=? [ F{\"t\"}<50 \"ipfound\" ])";
489 formulasAsString += "; \n multi(Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ])";
490
491 // programm, model, formula
492 storm::prism::Program program = storm::api::parseProgram(programFile);
493 program = storm::utility::prism::preprocess(program, constantsDef);
494 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
495 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
496 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
497 uint_fast64_t const initState = *mdp->getInitialStates().begin();
498
499 std::unique_ptr<storm::modelchecker::CheckResult> result;
500
501 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
502 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
503 EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult<double>()[initState],
504 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
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],
509 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
510}
511
512TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) {
513 storm::Environment env;
514
515 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm";
516 std::string constantsDef = "";
517 std::string formulasAsString = "multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ])";
518 formulasAsString += "; \n multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ], Pmax=? [ !\"collision_max_backoff\" U \"all_delivered\"] )";
519
520 // programm, model, formula
521 storm::prism::Program program = storm::api::parseProgram(programFile);
522 program = storm::utility::prism::preprocess(program, constantsDef);
523 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
524 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
525 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
526 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
527 uint_fast64_t const initState = *mdp->getInitialStates().begin();
528
529 std::unique_ptr<storm::modelchecker::CheckResult> result;
530
531 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
532 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
533 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832");
534 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
535
536 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
537 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
538 std::vector<storm::RationalNumber> p = {storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832"),
539 storm::utility::convertNumber<storm::RationalNumber, std::string>("7/8")};
540 auto expectedAchievableValues =
541 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p}));
542 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
543 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
544}
545
546TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) {
547 storm::Environment env;
548
549 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm";
550 std::string constantsDef = "";
551 std::string formulasAsString = "multi(Pmax=? [ F{\"a\"}>=1.1 x=1 ])";
552 formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}<=0.2 x=1], Pmax=? [F{\"b\"}>3 x=1 ])";
553 formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}>0.2 x=1 ], Pmax=? [F{\"b\"}>3 x=1 ])";
554 formulasAsString += "; \n multi(Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4)], Pmax=? [F {\"b\"}>3 x = 1])";
555
556 // programm, model, formula
557 storm::prism::Program program = storm::api::parseProgram(programFile);
558 program = storm::utility::prism::preprocess(program, constantsDef);
559 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
560 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
561 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
562 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
563 uint_fast64_t const initState = *mdp->getInitialStates().begin();
564
565 std::unique_ptr<storm::modelchecker::CheckResult> result;
566
567 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
568
569 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
570 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
571 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/100");
572 EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
573
574 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
575 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
576 std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1"),
577 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
578 auto expectedAchievableValues =
579 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1}));
580 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
581 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
582
583 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
584 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
585 std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1"),
586 storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640")};
587 std::vector<storm::RationalNumber> q2 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("81/256"),
588 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
589 expectedAchievableValues =
590 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2, q2}));
591 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
592 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
593
594 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
595 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
596 std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("81/160"),
597 storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640")};
598 std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("2187/10240"),
599 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
600 expectedAchievableValues =
601 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3, q3}));
602 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
603 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
604}
605
606#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:13
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:739
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:93
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:30
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:242
storm_gtest.h