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