Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDtmcParameterLiftingTest.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};
27
28class DoubleSVIEnvironment {
29 public:
30 typedef double ValueType;
31 static storm::modelchecker::RegionCheckEngine const regionEngine = storm::modelchecker::RegionCheckEngine::ParameterLifting;
32 static storm::Environment createEnvironment() {
33 storm::Environment env;
34 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
35 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
36 return env;
37 }
38};
39
40class RationalPiEnvironment {
41 public:
42 typedef storm::RationalNumber ValueType;
43 static storm::modelchecker::RegionCheckEngine const regionEngine = storm::modelchecker::RegionCheckEngine::ExactParameterLifting;
44 static storm::Environment createEnvironment() {
45 storm::Environment env;
46 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
47 return env;
48 }
49};
50
51template<typename TestType>
52class SparseDtmcParameterLiftingTest : public ::testing::Test {
53 public:
54 typedef typename TestType::ValueType ValueType;
55 SparseDtmcParameterLiftingTest() : _environment(TestType::createEnvironment()) {}
56 storm::Environment const& env() const {
57 return _environment;
58 }
59 virtual void SetUp() {
60#ifndef STORM_HAVE_Z3
61 GTEST_SKIP() << "Z3 not available.";
62#endif
63 carl::VariablePool::getInstance().clear();
64 }
65 virtual void TearDown() {
66 carl::VariablePool::getInstance().clear();
67 }
68
69 private:
70 storm::Environment _environment;
71};
72
73void checkBrpProb(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine, bool allowSimplify) {
74 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
75 std::string formulaAsString = "P<=0.84 [F s=5 ]";
76 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
77
78 // Program and formula
79 storm::prism::Program program = storm::api::parseProgram(programFile);
80 program = program.preprocess(constantsAsString);
81 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
82 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
83 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
84 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
85
86 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
87 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
88 modelParameters.insert(rewParameters.begin(), rewParameters.end());
89
90 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
91 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, allowSimplify);
92
93 // start testing
94 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
95 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
96 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
97
98 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
99 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
100 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
101 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
102 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
103 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
104}
105
106void checkBrpProbValidation(storm::Environment const& env) {
107 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
108 std::string formulaAsString = "P<=0.84 [F s=5 ]";
109 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
110
111 // Program and formula
112 storm::prism::Program program = storm::api::parseProgram(programFile);
113 program = program.preprocess(constantsAsString);
114 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
115 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
116 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
117 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
118
119 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
120 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting);
121
122 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
123 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
124 modelParameters.insert(rewParameters.begin(), rewParameters.end());
125
126 // start testing
127 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
128 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
129 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
130
131 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
132 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
133 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
134 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
135 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
136 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
137}
138
139void checkBrpRew(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine, bool allowSimplify) {
140 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
141 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
142 std::string constantsAsString = "pL=0.9,TOAck=0.5";
143
144 storm::prism::Program program = storm::api::parseProgram(programFile);
145 program = program.preprocess(constantsAsString);
146 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
147 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
148 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
149 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
150
151 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
152 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
153 modelParameters.insert(rewParameters.begin(), rewParameters.end());
154
155 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
156 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, allowSimplify);
157
158 // start testing
159 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
160 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
161 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
162
163 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
164 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
165 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
166 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
167 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
168 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
169}
170
171void checkBrpRewValidation(storm::Environment const& env) {
172 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
173 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
174 std::string constantsAsString = "pL=0.9,TOAck=0.5";
175
176 storm::prism::Program program = storm::api::parseProgram(programFile);
177 program = program.preprocess(constantsAsString);
178 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
179 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
180 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
181 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
182
183 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
184 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting);
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 // start testing
191 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
192 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
193 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
194
195 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
196 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
197 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
198 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
199 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
200 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
201}
202
203void checkBrpRewBounded(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine, bool allowSimplify) {
204 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
205 std::string formulaAsString = "R>2.5 [ C<=300]";
206 std::string constantsAsString = "pL=0.9,TOAck=0.5";
207
208 storm::prism::Program program = storm::api::parseProgram(programFile);
209 program = program.preprocess(constantsAsString);
210 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
211 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
212 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
213 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
214
215 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
216 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
217 modelParameters.insert(rewParameters.begin(), rewParameters.end());
218
219 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
220 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, allowSimplify);
221
222 // start testing
223 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
224 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
225 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
226
227 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
228 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
229 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
230 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
231 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
232 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
233}
234
235void checkBrpRewBoundedValidation(storm::Environment const& env) {
236 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
237 std::string formulaAsString = "R>2.5 [ C<=300]";
238 std::string constantsAsString = "pL=0.9,TOAck=0.5";
239
240 storm::prism::Program program = storm::api::parseProgram(programFile);
241 program = program.preprocess(constantsAsString);
242 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
243 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
244 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
245 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
246
247 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
248 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting);
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 // start testing
255 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
256 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
257 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
258
259 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
260 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
261 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
262 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
263 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
264 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
265}
266
267void checkBrpRewInfty(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
268 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
269 std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
270 std::string constantsAsString = "";
271 storm::prism::Program program = storm::api::parseProgram(programFile);
272 program = program.preprocess(constantsAsString);
273 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
274 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
275 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
276 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
277
278 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
279 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
280 modelParameters.insert(rewParameters.begin(), rewParameters.end());
281
282 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
283 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
284
285 // start testing
286 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);
287
288 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
289 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
290}
291
292void checkBrpRew4Par(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
293 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
294 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
295 std::string constantsAsString = "";
296 storm::prism::Program program = storm::api::parseProgram(programFile);
297 program = program.preprocess(constantsAsString);
298 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
299 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
300 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
301 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
302
303 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
304 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
305 modelParameters.insert(rewParameters.begin(), rewParameters.end());
306
307 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
308 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
309
310 // start testing
311 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);
312 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);
313 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);
314
315 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
316 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
317 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
318 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
319 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
320 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
321}
322
323void checkCrowdsProb(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
324 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
325 std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
326 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
327
328 storm::prism::Program program = storm::api::parseProgram(programFile);
329 program = program.preprocess(constantsAsString);
330 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
331 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
332 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
333 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
334
335 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
336 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
337 modelParameters.insert(rewParameters.begin(), rewParameters.end());
338
339 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
340 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
341
342 // start testing
343 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
344 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
345 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
346 auto allVioHardRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
347
348 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
349 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
350 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
351 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
352 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
353 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
354 EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated,
355 regionChecker->analyzeRegion(env, allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
356}
357
358void checkCrowdsProbStepBounded(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
359 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
360 std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]";
361 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
362
363 storm::prism::Program program = storm::api::parseProgram(programFile);
364 program = program.preprocess(constantsAsString);
365 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
366 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
367 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
368 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
369
370 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
371 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
372 modelParameters.insert(rewParameters.begin(), rewParameters.end());
373
374 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
375 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
376
377 // start testing
378 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
379 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
380 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
381 auto allVioHardRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
382
383 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
384 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
385 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
386 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
387 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
388 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
389 EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated,
390 regionChecker->analyzeRegion(env, allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
391}
392
393void checkCrowdsProb1Par(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
394 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
395 std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
396 std::string constantsAsString = "badC=0.3"; // e.g. pL=0.9,TOACK=0.5
397
398 storm::prism::Program program = storm::api::parseProgram(programFile);
399 program = program.preprocess(constantsAsString);
400 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
401 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
402 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
403 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
404
405 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
406 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
407 modelParameters.insert(rewParameters.begin(), rewParameters.end());
408
409 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
410 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
411
412 // start testing
413 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.9<=PF<=0.99", modelParameters);
414 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.9", modelParameters);
415 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.01<=PF<=0.8", modelParameters);
416
417 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
418 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
419 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
420 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
421 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
422 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
423}
424
425void checkCrowdsProbConst(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
426 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
427 std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
428 std::string constantsAsString = "PF=0.9,badC=0.2";
429
430 storm::prism::Program program = storm::api::parseProgram(programFile);
431 program = program.preprocess(constantsAsString);
432 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
433 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
434 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
435 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
436
437 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
438 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
439 modelParameters.insert(rewParameters.begin(), rewParameters.end());
440
441 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
442 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
443
444 // start testing
445 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("", modelParameters);
446
447 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
448 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
449}
450
451void checkZeroConf(storm::Environment const& env, storm::modelchecker::RegionCheckEngine regionEngine) {
452 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/zeroconf4.pm";
453 std::string formulaAsString = "P>0.5 [F s=5 ]";
454 std::string constantsAsString = " n = 4"; // e.g. pL=0.9,TOACK=0.5
455
456 // Program and formula
457 storm::prism::Program program = storm::api::parseProgram(programFile);
458 program = program.preprocess(constantsAsString);
459 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
460 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
461 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
462 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
463
464 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
465 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
466 modelParameters.insert(rewParameters.begin(), rewParameters.end());
467
468 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
469 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), regionEngine, true);
470
471 // start testing
472 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=pL<=0.95,0.8<=pK<=0.95", modelParameters);
473 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pL<=0.9,0.6<=pK<=0.9", modelParameters);
474 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.7,0.1<=pK<=0.7", modelParameters);
475
476 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
477 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
478 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
479 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
480 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
481 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
482}
483
484typedef ::testing::Types<DoubleViEnvironment, DoubleSVIEnvironment, RationalPiEnvironment> TestingTypes;
485
486TYPED_TEST_SUITE(SparseDtmcParameterLiftingTest, TestingTypes, );
487
488TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
489 checkBrpProb(this->env(), TypeParam::regionEngine, true);
490}
491
492TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_no_simplification) {
493 checkBrpProb(this->env(), TypeParam::regionEngine, false);
494}
495
496TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
497 checkBrpRew(this->env(), TypeParam::regionEngine, true);
498}
499
500TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
501 checkBrpRewBounded(this->env(), TypeParam::regionEngine, true);
502}
503
504TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
505 typedef typename TestFixture::ValueType ValueType;
506 if (std::is_same<ValueType, storm::RationalNumber>::value) {
507 return;
508 }
509 checkBrpProbValidation(this->env());
510}
511
512TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
513 typedef typename TestFixture::ValueType ValueType;
514 if (std::is_same<ValueType, storm::RationalNumber>::value) {
515 return;
516 }
517 checkBrpRewValidation(this->env());
518}
519
520TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
521 typedef typename TestFixture::ValueType ValueType;
522 if (std::is_same<ValueType, storm::RationalNumber>::value) {
523 return;
524 }
525 checkBrpRewBoundedValidation(this->env());
526}
527
528TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
529 checkBrpRewInfty(this->env(), TypeParam::regionEngine);
530}
531
532TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
533 checkBrpRew4Par(this->env(), TypeParam::regionEngine);
534}
535
536TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
537 checkCrowdsProb(this->env(), TypeParam::regionEngine);
538}
539
540TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
541 checkCrowdsProbStepBounded(this->env(), TypeParam::regionEngine);
542}
543
544TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
545 checkCrowdsProb1Par(this->env(), TypeParam::regionEngine);
546}
547
548TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
549 checkCrowdsProbConst(this->env(), TypeParam::regionEngine);
550}
551
552TYPED_TEST(SparseDtmcParameterLiftingTest, ZeroConf) {
553 checkZeroConf(this->env(), TypeParam::regionEngine);
554}
555} // 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::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.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::RegionResult::CenterViolated
@ CenterViolated
the formula is violated for the parameter Valuation that corresponds to the center point of the regio...
Definition RegionResult.h:16
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