Storm
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#ifdef STORM_HAVE_CARL
5
6#include "storm/adapters/RationalFunctionAdapter.h"
7
8#include "storm-pars/api/storm-pars.h"
9#include "storm/api/storm.h"
10
11#include "storm-parsers/api/storm-parsers.h"
12
13#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
14#include "storm/environment/solver/MinMaxSolverEnvironment.h"
15#include "storm/solver/stateelimination/NondeterministicModelStateEliminator.h"
16#include "storm/storage/StronglyConnectedComponentDecomposition.h"
17#include "storm/storage/jani/Property.h"
18
19namespace {
20class DoubleViEnvironment {
21 public:
22 typedef double ValueType;
23 static storm::Environment createEnvironment() {
24 storm::Environment env;
25 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
26 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
27 return env;
28 }
29};
30
31class DoubleSVIEnvironment {
32 public:
33 typedef double ValueType;
34 static storm::Environment createEnvironment() {
35 storm::Environment env;
36 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
37 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
38 return env;
39 }
40};
41
42class RationalPiEnvironment {
43 public:
44 typedef storm::RationalNumber ValueType;
45 static storm::Environment createEnvironment() {
46 storm::Environment env;
47 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
48 return env;
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
73typedef ::testing::Types<DoubleViEnvironment, DoubleSVIEnvironment, RationalPiEnvironment> TestingTypes;
74
75TYPED_TEST_SUITE(SparseDtmcParameterLiftingTest, TestingTypes, );
76
77TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
78 typedef typename TestFixture::ValueType ValueType;
79
80 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
81 std::string formulaAsString = "P<=0.84 [F s=5 ]";
82 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
83
84 // Program and formula
85 storm::prism::Program program = storm::api::parseProgram(programFile);
86 program = storm::utility::prism::preprocess(program, constantsAsString);
87 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
88 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
89 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
90 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
91
92 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
93 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
94 modelParameters.insert(rewParameters.begin(), rewParameters.end());
95
96 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
97 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
98
99 // start testing
100 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
101 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
102 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
103
104 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
105 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
106 storm::modelchecker::RegionResult::Unknown, true));
107 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
108 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
109 storm::modelchecker::RegionResult::Unknown, true));
110 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
111 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
112 storm::modelchecker::RegionResult::Unknown, true));
113}
114
115TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_no_simplification) {
116 typedef typename TestFixture::ValueType ValueType;
117
118 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
119 std::string formulaAsString = "P<=0.84 [F s=5 ]";
120 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
121
122 // Program and formula
123 storm::prism::Program program = storm::api::parseProgram(programFile);
124 program = storm::utility::prism::preprocess(program, constantsAsString);
125 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
126 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
127 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
128 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
129
130 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
131 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
132 modelParameters.insert(rewParameters.begin(), rewParameters.end());
133
134 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
135 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), false, false);
136
137 // start testing
138 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
139 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
140 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
141
142 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
143 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
144 storm::modelchecker::RegionResult::Unknown, true));
145 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
146 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
147 storm::modelchecker::RegionResult::Unknown, true));
148 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
149 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
150 storm::modelchecker::RegionResult::Unknown, true));
151}
152
153TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
154 typedef typename TestFixture::ValueType ValueType;
155 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
156 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
157 std::string constantsAsString = "pL=0.9,TOAck=0.5";
158
159 storm::prism::Program program = storm::api::parseProgram(programFile);
160 program = storm::utility::prism::preprocess(program, constantsAsString);
161 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
162 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
163 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
164 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<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 = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
171 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
172
173 // start testing
174 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
175 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
176 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
177
178 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
179 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
180 storm::modelchecker::RegionResult::Unknown, true));
181 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
182 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
183 storm::modelchecker::RegionResult::Unknown, true));
184 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
185 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
186 storm::modelchecker::RegionResult::Unknown, true));
187}
188
189TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
190 typedef typename TestFixture::ValueType ValueType;
191 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
192 std::string formulaAsString = "R>2.5 [ C<=300]";
193 std::string constantsAsString = "pL=0.9,TOAck=0.5";
194
195 storm::prism::Program program = storm::api::parseProgram(programFile);
196 program = storm::utility::prism::preprocess(program, constantsAsString);
197 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
198 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
199 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
200 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
201
202 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
203 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
204 modelParameters.insert(rewParameters.begin(), rewParameters.end());
205
206 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
207 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
208
209 // start testing
210 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
211 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
212 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
213
214 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
215 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
216 storm::modelchecker::RegionResult::Unknown, true));
217 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
218 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
219 storm::modelchecker::RegionResult::Unknown, true));
220 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
221 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
222 storm::modelchecker::RegionResult::Unknown, true));
223}
224
225TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
226 typedef typename TestFixture::ValueType ValueType;
227 if (!std::is_same<ValueType, storm::RationalNumber>::value) {
228 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
229 std::string formulaAsString = "P<=0.84 [F s=5 ]";
230 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
231
232 // Program and formula
233 storm::prism::Program program = storm::api::parseProgram(programFile);
234 program = storm::utility::prism::preprocess(program, constantsAsString);
235 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
236 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
237 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
238 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
239
240 auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, ValueType, storm::RationalNumber>(
241 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
242
243 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
244 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
245 modelParameters.insert(rewParameters.begin(), rewParameters.end());
246
247 // start testing
248 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
249 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
250 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
251
252 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
253 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
254 storm::modelchecker::RegionResult::Unknown, true));
255 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
256 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
257 storm::modelchecker::RegionResult::Unknown, true));
258 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
259 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
260 storm::modelchecker::RegionResult::Unknown, true));
261 }
262}
263
264TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
265 typedef typename TestFixture::ValueType ValueType;
266 if (!std::is_same<ValueType, storm::RationalNumber>::value) {
267 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
268 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
269 std::string constantsAsString = "pL=0.9,TOAck=0.5";
270
271 storm::prism::Program program = storm::api::parseProgram(programFile);
272 program = storm::utility::prism::preprocess(program, 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::initializeValidatingRegionModelChecker<storm::RationalFunction, ValueType, storm::RationalNumber>(
283 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
284
285 // start testing
286 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
287 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
288 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
289
290 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
291 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
292 storm::modelchecker::RegionResult::Unknown, true));
293 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
294 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
295 storm::modelchecker::RegionResult::Unknown, true));
296 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
297 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
298 storm::modelchecker::RegionResult::Unknown, true));
299 }
300}
301
302TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
303 typedef typename TestFixture::ValueType ValueType;
304
305 if (!std::is_same<ValueType, storm::RationalNumber>::value) {
306 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
307 std::string formulaAsString = "R>2.5 [ C<=300]";
308 std::string constantsAsString = "pL=0.9,TOAck=0.5";
309
310 storm::prism::Program program = storm::api::parseProgram(programFile);
311 program = storm::utility::prism::preprocess(program, constantsAsString);
312 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
313 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
314 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
315 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
316
317 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
318 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
319 modelParameters.insert(rewParameters.begin(), rewParameters.end());
320
321 auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, ValueType, storm::RationalNumber>(
322 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
323
324 // start testing
325 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
326 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
327 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
328
329 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
330 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
331 storm::modelchecker::RegionResult::Unknown, true));
332 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
333 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
334 storm::modelchecker::RegionResult::Unknown, true));
335 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
336 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
337 storm::modelchecker::RegionResult::Unknown, true));
338 }
339}
340
341TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
342 typedef typename TestFixture::ValueType ValueType;
343
344 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
345 std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
346 std::string constantsAsString = "";
347 storm::prism::Program program = storm::api::parseProgram(programFile);
348 program = storm::utility::prism::preprocess(program, constantsAsString);
349 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
350 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
351 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
352 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
353
354 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
355 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
356 modelParameters.insert(rewParameters.begin(), rewParameters.end());
357
358 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
359 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
360
361 // start testing
362 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);
363
364 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
365 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
366 storm::modelchecker::RegionResult::Unknown, true));
367}
368
369TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
370 typedef typename TestFixture::ValueType ValueType;
371
372 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
373 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
374 std::string constantsAsString = "";
375 storm::prism::Program program = storm::api::parseProgram(programFile);
376 program = storm::utility::prism::preprocess(program, constantsAsString);
377 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
378 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
379 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
380 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
381
382 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
383 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
384 modelParameters.insert(rewParameters.begin(), rewParameters.end());
385
386 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
387 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
388
389 // start testing
390 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);
391 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);
392 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);
393
394 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
395 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
396 storm::modelchecker::RegionResult::Unknown, true));
397 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
398 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
399 storm::modelchecker::RegionResult::Unknown, true));
400 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
401 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
402 storm::modelchecker::RegionResult::Unknown, true));
403}
404
405TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
406 typedef typename TestFixture::ValueType ValueType;
407
408 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
409 std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
410 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
411
412 storm::prism::Program program = storm::api::parseProgram(programFile);
413 program = storm::utility::prism::preprocess(program, constantsAsString);
414 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
415 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
416 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
417 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
418
419 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
420 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
421 modelParameters.insert(rewParameters.begin(), rewParameters.end());
422
423 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
424 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
425
426 // start testing
427 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
428 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
429 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
430 auto allVioHardRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
431
432 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
433 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
434 storm::modelchecker::RegionResult::Unknown, true));
435 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
436 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
437 storm::modelchecker::RegionResult::Unknown, true));
438 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
439 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
440 storm::modelchecker::RegionResult::Unknown, true));
441 EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated,
442 regionChecker->analyzeRegion(this->env(), allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
443 storm::modelchecker::RegionResult::Unknown, true));
444}
445
446TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
447 typedef typename TestFixture::ValueType ValueType;
448
449 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
450 std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]";
451 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
452
453 storm::prism::Program program = storm::api::parseProgram(programFile);
454 program = storm::utility::prism::preprocess(program, constantsAsString);
455 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
456 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
457 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
458 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
459
460 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
461 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
462 modelParameters.insert(rewParameters.begin(), rewParameters.end());
463
464 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
465 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
466
467 // start testing
468 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
469 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
470 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
471 auto allVioHardRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
472
473 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
474 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
475 storm::modelchecker::RegionResult::Unknown, true));
476 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
477 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
478 storm::modelchecker::RegionResult::Unknown, true));
479 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
480 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
481 storm::modelchecker::RegionResult::Unknown, true));
482 EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated,
483 regionChecker->analyzeRegion(this->env(), allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
484 storm::modelchecker::RegionResult::Unknown, true));
485}
486
487TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
488 typedef typename TestFixture::ValueType ValueType;
489
490 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
491 std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
492 std::string constantsAsString = "badC=0.3"; // e.g. pL=0.9,TOACK=0.5
493
494 storm::prism::Program program = storm::api::parseProgram(programFile);
495 program = storm::utility::prism::preprocess(program, constantsAsString);
496 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
497 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
498 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
499 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
500
501 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
502 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
503 modelParameters.insert(rewParameters.begin(), rewParameters.end());
504
505 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
506 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
507
508 // start testing
509 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.9<=PF<=0.99", modelParameters);
510 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.9", modelParameters);
511 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.01<=PF<=0.8", modelParameters);
512
513 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
514 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
515 storm::modelchecker::RegionResult::Unknown, true));
516 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
517 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
518 storm::modelchecker::RegionResult::Unknown, true));
519 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
520 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
521 storm::modelchecker::RegionResult::Unknown, true));
522}
523
524TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
525 typedef typename TestFixture::ValueType ValueType;
526
527 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
528 std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
529 std::string constantsAsString = "PF=0.9,badC=0.2";
530
531 storm::prism::Program program = storm::api::parseProgram(programFile);
532 program = storm::utility::prism::preprocess(program, constantsAsString);
533 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
534 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
535 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
536 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
537
538 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
539 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
540 modelParameters.insert(rewParameters.begin(), rewParameters.end());
541
542 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
543 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
544
545 // start testing
546 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("", modelParameters);
547
548 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
549 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
550 storm::modelchecker::RegionResult::Unknown, true));
551}
552
553TYPED_TEST(SparseDtmcParameterLiftingTest, ZeroConf) {
554 typedef typename TestFixture::ValueType ValueType;
555
556 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/zeroconf4.pm";
557 std::string formulaAsString = "P>0.5 [F s=5 ]";
558 std::string constantsAsString = " n = 4"; // e.g. pL=0.9,TOACK=0.5
559
560 // Program and formula
561 storm::prism::Program program = storm::api::parseProgram(programFile);
562 program = storm::utility::prism::preprocess(program, constantsAsString);
563 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
564 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
565 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
566 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
567
568 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
569 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
570 modelParameters.insert(rewParameters.begin(), rewParameters.end());
571
572 auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, ValueType>(
573 this->env(), model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
574
575 // start testing
576 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=pL<=0.95,0.8<=pK<=0.95", modelParameters);
577 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pL<=0.9,0.6<=pK<=0.9", modelParameters);
578 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.7,0.1<=pK<=0.7", modelParameters);
579
580 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
581 regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
582 storm::modelchecker::RegionResult::Unknown, true));
583 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
584 regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
585 storm::modelchecker::RegionResult::Unknown, true));
586 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
587 regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,
588 storm::modelchecker::RegionResult::Unknown, true));
589}
590} // namespace
591#endif
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:25
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::MinMaxSolverEnvironment::setMethod
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
Definition MinMaxSolverEnvironment.cpp:43
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:43
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:13
storm::modelchecker::RegionResult::AllSat
@ AllSat
the formula is satisfied for all parameters in the given region
storm::modelchecker::RegionResult::AllViolated
@ AllViolated
the formula is violated for all parameters in the given region
storm::modelchecker::RegionResult::Unknown
@ Unknown
the result is unknown
storm::modelchecker::RegionResult::ExistsBoth
@ ExistsBoth
the formula is satisfied for some parameters but also violated for others
storm::modelchecker::RegionResult::CenterViolated
@ CenterViolated
the formula is violated for the parameter Valuation that corresponds to the center point of the regio...
storm::models::sparse::getRewardParameters
std::set< storm::RationalFunctionVariable > getRewardParameters(Model< storm::RationalFunction > const &model)
Get all parameters occurring in rewards.
Definition Model.cpp:707
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:703
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h