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