Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMdpParameterLiftingTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#ifdef STORM_HAVE_CARL
5
6#include "storm/adapters/RationalFunctionAdapter.h"
7
8#include "storm-pars/api/storm-pars.h"
9#include "storm/api/storm.h"
10
11#include "storm-parsers/api/storm-parsers.h"
12
13#include "storm/environment/solver/MinMaxSolverEnvironment.h"
14#include "storm/storage/jani/Property.h"
15
16namespace {
17class DoubleViEnvironment {
18 public:
19 typedef double ValueType;
20 static storm::Environment createEnvironment() {
21 storm::Environment env;
22 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
23 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
24 return env;
25 }
26};
27class RationalPIEnvironment {
28 public:
29 typedef storm::RationalNumber ValueType;
30 static storm::Environment createEnvironment() {
31 storm::Environment env;
32 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
33 return env;
34 }
35};
36template<typename TestType>
37class SparseMdpParameterLiftingTest : public ::testing::Test {
38 public:
39 typedef typename TestType::ValueType ValueType;
40 SparseMdpParameterLiftingTest() : _environment(TestType::createEnvironment()) {}
41 storm::Environment const& env() const {
42 return _environment;
43 }
44 virtual void SetUp() {
45#ifndef STORM_HAVE_Z3
46 GTEST_SKIP() << "Z3 not available.";
47#endif
48 carl::VariablePool::getInstance().clear();
49 }
50 virtual void TearDown() {
51 carl::VariablePool::getInstance().clear();
52 }
53
54 private:
55 storm::Environment _environment;
56};
57
58typedef ::testing::Types<DoubleViEnvironment, RationalPIEnvironment> TestingTypes;
59
60TYPED_TEST_SUITE(SparseMdpParameterLiftingTest, TestingTypes, );
61
62TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
63 typedef typename TestFixture::ValueType ValueType;
64
65 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
66 std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
67
68 storm::prism::Program program = storm::api::parseProgram(programFile);
69 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
70 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
71 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
72 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
73
74 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
75 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
76 modelParameters.insert(rewParameters.begin(), rewParameters.end());
77
78 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
79 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
80
81 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
82 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
83 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
84
85 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
86 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
87 storm::modelchecker::RegionResult::Unknown, true));
88 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
89 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
90 storm::modelchecker::RegionResult::Unknown, true));
91 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
92 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
93 storm::modelchecker::RegionResult::Unknown, true));
94}
95
96TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
97 typedef typename TestFixture::ValueType ValueType;
98
99 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
100 std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
101
102 storm::prism::Program program = storm::api::parseProgram(programFile);
103 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
104 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
105 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
106 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
107
108 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
109 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
110 modelParameters.insert(rewParameters.begin(), rewParameters.end());
111
112 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
113 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
114
115 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
116 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
117 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
118
119 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
120 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
121 storm::modelchecker::RegionResult::Unknown, true));
122 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
123 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
124 storm::modelchecker::RegionResult::Unknown, true));
125 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
126 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
127 storm::modelchecker::RegionResult::Unknown, true));
128}
129
130TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
131 typedef typename TestFixture::ValueType ValueType;
132 if (!std::is_same<ValueType, storm::RationalNumber>::value) {
133 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
134 std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
135
136 storm::prism::Program program = storm::api::parseProgram(programFile);
137 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
138 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
139 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
140 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
141
142 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
143 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
144 modelParameters.insert(rewParameters.begin(), rewParameters.end());
145
146 auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, ValueType, storm::RationalNumber>(
147 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
148
149 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
150 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
151 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
152
153 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
154 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
155 storm::modelchecker::RegionResult::Unknown, true));
156 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
157 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
158 storm::modelchecker::RegionResult::Unknown, true));
159 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
160 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
161 storm::modelchecker::RegionResult::Unknown, true));
162 }
163}
164
165TYPED_TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
166 typedef typename TestFixture::ValueType ValueType;
167 if (!std::is_same<ValueType, storm::RationalNumber>::value) {
168 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
169 std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
170
171 storm::prism::Program program = storm::api::parseProgram(programFile);
172 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
173 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
174 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
175 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
176
177 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
178 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
179 modelParameters.insert(rewParameters.begin(), rewParameters.end());
180
181 auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, ValueType, storm::RationalNumber>(
182 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
183
184 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
185 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
186 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
187
188 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
189 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
190 storm::modelchecker::RegionResult::Unknown, true));
191 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
192 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
193 storm::modelchecker::RegionResult::Unknown, true));
194 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
195 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
196 storm::modelchecker::RegionResult::Unknown, true));
197 }
198}
199
200TYPED_TEST(SparseMdpParameterLiftingTest, coin_Prob) {
201 typedef typename TestFixture::ValueType ValueType;
202
203 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm";
204 std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
205
206 storm::prism::Program program = storm::api::parseProgram(programFile);
207 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
208 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
209 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
210 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
211
212 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
213 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
214 modelParameters.insert(rewParameters.begin(), rewParameters.end());
215
216 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
217 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
218
219 // start testing
220 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);
221 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
222 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.5<=p2<=0.6", modelParameters);
223
224 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
225 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
226 storm::modelchecker::RegionResult::Unknown, true));
227 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
228 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
229 storm::modelchecker::RegionResult::Unknown, true));
230 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
231 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
232 storm::modelchecker::RegionResult::Unknown, true));
233}
234
235TYPED_TEST(SparseMdpParameterLiftingTest, brp_Prop) {
236 typedef typename TestFixture::ValueType ValueType;
237
238 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
239 std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]";
240 std::string constantsAsString = "TOMsg=0.0,TOAck=0.0";
241
242 storm::prism::Program program = storm::api::parseProgram(programFile);
243 program = storm::utility::prism::preprocess(program, constantsAsString);
244 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
245 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
246 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
247 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
248
249 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
250 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
251 modelParameters.insert(rewParameters.begin(), rewParameters.end());
252
253 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
254 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
255
256 // start testing
257 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
258 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
259 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
260
261 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
262 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
263 storm::modelchecker::RegionResult::Unknown, true));
264 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
265 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
266 storm::modelchecker::RegionResult::Unknown, true));
267 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
268 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
269 storm::modelchecker::RegionResult::Unknown, true));
270}
271
272TYPED_TEST(SparseMdpParameterLiftingTest, brp_Rew) {
273 typedef typename TestFixture::ValueType ValueType;
274
275 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
276 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
277 std::string constantsAsString = "pL=0.9,TOAck=0.5";
278
279 storm::prism::Program program = storm::api::parseProgram(programFile);
280 program = storm::utility::prism::preprocess(program, constantsAsString);
281 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
282 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
283 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
284 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
285
286 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
287 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
288 modelParameters.insert(rewParameters.begin(), rewParameters.end());
289
290 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
291 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
292
293 // start testing
294 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
295 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
296 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
297
298 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
299 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
300 storm::modelchecker::RegionResult::Unknown, true));
301 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
302 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
303 storm::modelchecker::RegionResult::Unknown, true));
304 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
305 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
306 storm::modelchecker::RegionResult::Unknown, true));
307}
308
309TYPED_TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
310 typedef typename TestFixture::ValueType ValueType;
311
312 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
313 std::string formulaAsString = "R>2.5 [ C<=300 ]";
314 std::string constantsAsString = "pL=0.9,TOAck=0.5";
315
316 storm::prism::Program program = storm::api::parseProgram(programFile);
317 program = storm::utility::prism::preprocess(program, constantsAsString);
318 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
319 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
320 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
321 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
322
323 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
324 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
325 modelParameters.insert(rewParameters.begin(), rewParameters.end());
326
327 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
328 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
329
330 // start testing
331 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
332 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
333 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
334
335 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
336 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
337 storm::modelchecker::RegionResult::Unknown, true));
338 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
339 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
340 storm::modelchecker::RegionResult::Unknown, true));
341 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
342 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
343 storm::modelchecker::RegionResult::Unknown, true));
344}
345
346TYPED_TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
347 typedef typename TestFixture::ValueType ValueType;
348
349 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
350 std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
351 std::string constantsAsString = "";
352 storm::prism::Program program = storm::api::parseProgram(programFile);
353 program = storm::utility::prism::preprocess(program, constantsAsString);
354 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
355 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
356 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
357 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
358
359 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
360 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
361 modelParameters.insert(rewParameters.begin(), rewParameters.end());
362
363 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
364 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
365
366 // start testing
367 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
368
369 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
370 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
371 storm::modelchecker::RegionResult::Unknown, true));
372}
373
374TYPED_TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
375 typedef typename TestFixture::ValueType ValueType;
376
377 std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
378 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
379 std::string constantsAsString = "";
380 storm::prism::Program program = storm::api::parseProgram(programFile);
381 program = storm::utility::prism::preprocess(program, constantsAsString);
382 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
383 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
384 std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model =
385 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
386
387 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
388 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
389 modelParameters.insert(rewParameters.begin(), rewParameters.end());
390
391 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
392 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
393
394 // start testing
395 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
396 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
397 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
398
399 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
400 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
401 storm::modelchecker::RegionResult::Unknown, true));
402 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
403 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
404 storm::modelchecker::RegionResult::Unknown, true));
405 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
406 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
407 storm::modelchecker::RegionResult::Unknown, true));
408}
409
410} // namespace
411
412#endif
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::MinMaxSolverEnvironment::setMethod
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
Definition MinMaxSolverEnvironment.cpp:43
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:43
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:13
storm::modelchecker::RegionResult::AllSat
@ AllSat
the formula is satisfied for all parameters in the given region
storm::modelchecker::RegionResult::AllViolated
@ AllViolated
the formula is violated for all parameters in the given region
storm::modelchecker::RegionResult::Unknown
@ Unknown
the result is unknown
storm::modelchecker::RegionResult::ExistsBoth
@ ExistsBoth
the formula is satisfied for some parameters but also violated for others
storm::models::sparse::getRewardParameters
std::set< storm::RationalFunctionVariable > getRewardParameters(Model< storm::RationalFunction > const &model)
Get all parameters occurring in rewards.
Definition Model.cpp:707
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:703
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
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h