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