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/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
289#ifdef STORM_HAVE_Z3_OPTIMIZE
290
291TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) {
292 storm::Environment env;
293 env.solver().setForceExact(true);
294 auto const prec = env.modelchecker().multi().getPrecision();
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_NEAR(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
319
320 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
321 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
322 EXPECT_NEAR(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState],
323 prec);
324
325 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
326 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
327 EXPECT_NEAR(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
328
329 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
330 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
331 std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber>(0.5),
332 storm::utility::convertNumber<storm::RationalNumber>(0.5)};
333 std::vector<storm::RationalNumber> q1 = {storm::utility::convertNumber<storm::RationalNumber>(0.125),
334 storm::utility::convertNumber<storm::RationalNumber>(0.75)};
335 auto expectedAchievableValues =
336 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1, q1}));
337
338 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
339 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
340
341 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula());
342 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
343 std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber>(0.0),
344 storm::utility::convertNumber<storm::RationalNumber>(0.75)};
345 expectedAchievableValues =
346 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2}));
347 std::vector<std::vector<storm::RationalNumber>> transformationMatrix(2,
348 std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
349 transformationMatrix[0][0] = -storm::utility::one<storm::RationalNumber>();
350 transformationMatrix[1][1] = storm::utility::one<storm::RationalNumber>();
351 expectedAchievableValues = expectedAchievableValues->affineTransformation(
352 transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
353 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
354 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
355
356 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula());
357 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
358 std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber>(0.0),
359 storm::utility::convertNumber<storm::RationalNumber>(-0.75)};
360 std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber>(-0.5),
361 storm::utility::convertNumber<storm::RationalNumber>(0.0)};
362 expectedAchievableValues =
363 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3, q3}));
364 transformationMatrix[1][1] = -storm::utility::one<storm::RationalNumber>();
365 expectedAchievableValues = expectedAchievableValues->affineTransformation(
366 transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
367 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
368 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
369}
370
371TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) {
372 if (!storm::test::z3AtLeastVersion(4, 8, 5)) {
373 GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
374 }
375 storm::Environment env;
376 env.solver().setForceExact(true);
377 auto const prec = env.modelchecker().multi().getPrecision();
378
379 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
380 std::string constantsDef = "N=10";
381 std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=5 x=N ]) ";
382 formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )])";
383 formulasAsString += "; \n multi(P>=1/512 [ F{\"r\"}<=5 x=N], Pmax=? [ F{\"l\"}<=10 x=0])";
384
385 // programm, model, formula
386 storm::prism::Program program = storm::api::parseProgram(programFile);
387 program = storm::utility::prism::preprocess(program, constantsDef);
388 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
389 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
390 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
391 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
392 uint_fast64_t const initState = *mdp->getInitialStates().begin();
393
394 std::unique_ptr<storm::modelchecker::CheckResult> result;
395
396 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
397 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
398 storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
399 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
400
401 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
402 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
403 expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
404 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
405
406 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
407 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
408 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("2539/4096");
409 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
410}
411
412TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) {
413 storm::Environment env;
414 env.solver().setForceExact(true);
415 auto const prec = env.modelchecker().multi().getPrecision();
416
417 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm";
418 std::string constantsDef = "";
419 std::string formulasAsString = "multi(Pmax=? [ F{\"a\"}<=3 x=4 ]) "; // 0.2
420 formulasAsString += "; \n multi(Pmin=? [ F{\"a\"}<=3 x=4 ]) "; // 0.0
421 formulasAsString += "; \n multi(Pmin=? [ F{\"a\"}<1 x=1 ]) "; // 0.0
422 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )]) "; // 0.02
423 formulasAsString += "; \n multi(Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )]) "; // 0.0
424 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )]) "; // 0.02
425 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )]) "; // 0.02
426 formulasAsString +=
427 "; \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)
428
429 // programm, model, formula
430 storm::prism::Program program = storm::api::parseProgram(programFile);
431 program = storm::utility::prism::preprocess(program, constantsDef);
432 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
433 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
434 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
435 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
436 uint_fast64_t const initState = *mdp->getInitialStates().begin();
437
438 std::unique_ptr<storm::modelchecker::CheckResult> result;
439
440 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
441 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
442 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/5");
443 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
444
445 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->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[2]->asMultiObjectiveFormula());
451 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
452 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
453 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
454
455 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
456 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
457 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
458 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
459
460 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula());
461 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
462 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("0");
463 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
464
465 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->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[6]->asMultiObjectiveFormula());
471 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
472 expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("1/50");
473 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
474
475 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[7]->asMultiObjectiveFormula());
476 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
477 std::vector<storm::RationalNumber> p = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1/10"),
478 storm::utility::convertNumber<storm::RationalNumber, std::string>("0")};
479 std::vector<storm::RationalNumber> q = {storm::utility::convertNumber<storm::RationalNumber, std::string>("0"),
480 storm::utility::convertNumber<storm::RationalNumber, std::string>("19/100")};
481 auto expectedAchievableValues =
482 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p, q}));
483
484 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
485 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
486}
487
488TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) {
489 storm::Environment env;
490 auto const prec = storm::utility::convertNumber<double>(env.modelchecker().multi().getPrecision());
491
492 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
493 std::string constantsDef = "N=1000,K=2,reset=true";
494 std::string formulasAsString = "multi(Pmin=? [ F{\"t\"}<50 \"ipfound\" ])";
495 formulasAsString += "; \n multi(Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ])";
496
497 // programm, model, formula
498 storm::prism::Program program = storm::api::parseProgram(programFile);
499 program = storm::utility::prism::preprocess(program, constantsDef);
500 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
501 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
502 std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
503 uint_fast64_t const initState = *mdp->getInitialStates().begin();
504
505 std::unique_ptr<storm::modelchecker::CheckResult> result;
506
507 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
508 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
509 EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult<double>()[initState], prec);
510
511 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
512 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
513 EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult<double>()[initState], prec);
514}
515
516TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) {
517 storm::Environment env;
518 env.solver().setForceExact(true);
519 auto const prec = env.modelchecker().multi().getPrecision();
520
521 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm";
522 std::string constantsDef = "";
523 std::string formulasAsString = "multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ])";
524 formulasAsString += "; \n multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ], Pmax=? [ !\"collision_max_backoff\" U \"all_delivered\"] )";
525
526 // programm, model, formula
527 storm::prism::Program program = storm::api::parseProgram(programFile);
528 program = storm::utility::prism::preprocess(program, constantsDef);
529 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
530 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
531 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
532 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
533 uint_fast64_t const initState = *mdp->getInitialStates().begin();
534
535 std::unique_ptr<storm::modelchecker::CheckResult> result;
536
537 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
538 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
539 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832");
540 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
541
542 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
543 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
544 std::vector<storm::RationalNumber> p = {storm::utility::convertNumber<storm::RationalNumber, std::string>("29487882838281/35184372088832"),
545 storm::utility::convertNumber<storm::RationalNumber, std::string>("7/8")};
546 auto expectedAchievableValues =
547 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p}));
548 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
549 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
550}
551
552TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) {
553 storm::Environment env;
554 env.solver().setForceExact(true);
555 auto const prec = env.modelchecker().multi().getPrecision();
556
557 std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm";
558 std::string constantsDef = "";
559 std::string formulasAsString = "multi(Pmax=? [ F{\"a\"}>=1.1 x=1 ])";
560 formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}<=0.2 x=1], Pmax=? [F{\"b\"}>3 x=1 ])";
561 formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}>0.2 x=1 ], Pmax=? [F{\"b\"}>3 x=1 ])";
562 formulasAsString += "; \n multi(Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4)], Pmax=? [F {\"b\"}>3 x = 1])";
563
564 // programm, model, formula
565 storm::prism::Program program = storm::api::parseProgram(programFile);
566 program = storm::utility::prism::preprocess(program, constantsDef);
567 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
568 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
569 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp =
570 storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
571 uint_fast64_t const initState = *mdp->getInitialStates().begin();
572
573 std::unique_ptr<storm::modelchecker::CheckResult> result;
574
575 storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>> mc(*mdp);
576
577 result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
578 ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
579 storm::RationalNumber expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("81/100");
580 EXPECT_NEAR(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState], prec);
581
582 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
583 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
584 std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1"),
585 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
586 auto expectedAchievableValues =
587 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1}));
588 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
589 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
590
591 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
592 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
593 std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("1"),
594 storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640")};
595 std::vector<storm::RationalNumber> q2 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("81/256"),
596 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
597 expectedAchievableValues =
598 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2, q2}));
599 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
600 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
601
602 result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula());
603 ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
604 std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("81/160"),
605 storm::utility::convertNumber<storm::RationalNumber, std::string>("243/640")};
606 std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber, std::string>("2187/10240"),
607 storm::utility::convertNumber<storm::RationalNumber, std::string>("27/64")};
608 expectedAchievableValues =
609 storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3, q3}));
610 EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
611 EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
612}
613
614#endif /* STORM_HAVE_Z3_OPTIMIZE */
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:46
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:179
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:765
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::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::pow
ValueType pow(ValueType const &value, int_fast64_t exponent)
Definition constants.cpp:243
storm_gtest.h