Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseDtmcParameterLiftingMonotonicityTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h"
5#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
6#include "storm-parsers/api/storm-parsers.h"
7#include "storm/adapters/RationalFunctionAdapter.h"
8#include "storm/api/storm.h"
9#include "storm/environment/solver/MinMaxSolverEnvironment.h"
10#include "storm/storage/StronglyConnectedComponentDecomposition.h"
11
12namespace {
13class DoubleSVIEnvironment {
14 public:
15 typedef double ValueType;
16 static storm::modelchecker::RegionCheckEngine const regionEngine = storm::modelchecker::RegionCheckEngine::ParameterLifting;
17 static storm::Environment createEnvironment() {
18 storm::Environment env;
19 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
20 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
21 return env;
22 }
23};
24
25class RationalPiEnvironment {
26 public:
27 typedef storm::RationalNumber ValueType;
28 static storm::modelchecker::RegionCheckEngine const regionEngine = storm::modelchecker::RegionCheckEngine::ExactParameterLifting;
29 static storm::Environment createEnvironment() {
30 storm::Environment env;
31 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
32 return env;
33 }
34};
35template<typename TestType>
36class SparseDtmcParameterLiftingMonotonicityTest : public ::testing::Test {
37 public:
38 typedef typename TestType::ValueType ValueType;
39 SparseDtmcParameterLiftingMonotonicityTest() : _environment(TestType::createEnvironment()) {}
40 storm::Environment const& env() const {
41 return _environment;
42 }
43 std::unique_ptr<storm::modelchecker::RegionModelChecker<storm::RationalFunction>> initializeRegionModelChecker(
44 std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> formula,
45 bool useMonotonicity) {
46 return storm::api::initializeRegionModelChecker(env(), model, storm::api::createTask<storm::RationalFunction>(formula, true), TestType::regionEngine,
47 true, true, false, storm::api::MonotonicitySetting(useMonotonicity));
48 }
49
50 virtual void SetUp() {
51#ifndef STORM_HAVE_Z3
52 GTEST_SKIP() << "Z3 not available.";
53#endif
54 carl::VariablePool::getInstance().clear();
55 }
56 virtual void TearDown() {
57 carl::VariablePool::getInstance().clear();
58 }
59
60 private:
61 storm::Environment _environment;
62};
63
64typedef ::testing::Types<DoubleSVIEnvironment, RationalPiEnvironment> TestingTypes;
65
66TYPED_TEST_SUITE(SparseDtmcParameterLiftingMonotonicityTest, TestingTypes, );
67
68TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_LEQ) {
69 typedef typename TestFixture::ValueType ValueType;
70
71 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
72 std::string formulaAsString = "P<=0.84 [F s=5 ]";
73 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
74
75 // Program and formula
76 storm::prism::Program program = storm::api::parseProgram(programFile);
77 program = storm::utility::prism::preprocess(program, constantsAsString);
78 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
79 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
80 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
81 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
82
83 // Simplify model
84 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
85 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
86 model = simplifier.getSimplifiedModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
87 formulas[0] = simplifier.getSimplifiedFormula();
88
89 // Apply bisimulation
90 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
91 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
92 bisimType = storm::storage::BisimulationType::Weak;
93 }
94 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
95 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
96
97 // Model parameters
98 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
99 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
100 modelParameters.insert(rewParameters.begin(), rewParameters.end());
101
102 // Reachability order, as it is already done building we don't need to recreate the order for each region
103 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
104 auto monRes = monHelper->checkMonotonicityInBuild(std::cout);
105 auto order = monRes.begin()->first;
106 ASSERT_EQ(order->getNumberOfAddedStates(), model->getTransitionMatrix().getColumnCount());
107 ASSERT_TRUE(order->getDoneBuilding());
108 auto localMonRes =
109 std::make_shared<storm::analysis::LocalMonotonicityResult<storm::RationalFunctionVariable>>(monRes.begin()->second.first, order->getNumberOfStates());
110
111 // Modelcheckers
112 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
113 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
114
115 // start testing
116 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
117 auto expectedResult = regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
118 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
119
120 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
121 expectedResult = regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
122 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
123
124 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
125 expectedResult = regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
126 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
127}
128
129TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_GEQ) {
130 typedef typename TestFixture::ValueType ValueType;
131
132 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
133 std::string formulaAsString = "P>=0.84 [F s=5 ]";
134 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
135
136 // Program and formula
137 storm::prism::Program program = storm::api::parseProgram(programFile);
138 program = storm::utility::prism::preprocess(program, constantsAsString);
139 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
140 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
141 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
142 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
143
144 // Simplify model
145 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
146 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
147 model = simplifier.getSimplifiedModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
148 formulas[0] = simplifier.getSimplifiedFormula();
149
150 // Apply bisimulation
151 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
152 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
153 bisimType = storm::storage::BisimulationType::Weak;
154 }
155 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
156 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
157
158 // Model parameters
159 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
160 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
161 modelParameters.insert(rewParameters.begin(), rewParameters.end());
162
163 // Reachability order, as it is already done building we don't need to recreate the order for each region
164 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
165 auto monRes = monHelper->checkMonotonicityInBuild(std::cout);
166 auto order = monRes.begin()->first;
167 ASSERT_EQ(order->getNumberOfAddedStates(), model->getTransitionMatrix().getColumnCount());
168 ASSERT_TRUE(order->getDoneBuilding());
169 auto localMonRes =
170 std::make_shared<storm::analysis::LocalMonotonicityResult<storm::RationalFunctionVariable>>(monRes.begin()->second.first, order->getNumberOfStates());
171
172 // Modelcheckers
173 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
174 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
175
176 // start testing
177 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
178 auto expectedResult = regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
179 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
180
181 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
182 expectedResult = regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
183 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
184
185 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
186 expectedResult = regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
187 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
188}
189
190TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_LEQ_Incr) {
191 typedef typename TestFixture::ValueType ValueType;
192
193 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2_mon_incr.pm";
194 std::string formulaAsString = "P<=0.84 [F s=5 ]";
195 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
196
197 // Program and formula
198 storm::prism::Program program = storm::api::parseProgram(programFile);
199 program = storm::utility::prism::preprocess(program, constantsAsString);
200 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
201 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
202 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
203 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
204
205 // Simplify model
206 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
207 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
208 model = simplifier.getSimplifiedModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
209 formulas[0] = simplifier.getSimplifiedFormula();
210
211 // Apply bisimulation
212 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
213 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
214 bisimType = storm::storage::BisimulationType::Weak;
215 }
216 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
217 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
218
219 // Model parameters
220 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
221 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
222 modelParameters.insert(rewParameters.begin(), rewParameters.end());
223
224 // Reachability order, as it is already done building we don't need to recreate the order for each region
225 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
226 auto monRes = monHelper->checkMonotonicityInBuild(std::cout);
227 auto order = monRes.begin()->first;
228 ASSERT_EQ(order->getNumberOfAddedStates(), model->getTransitionMatrix().getColumnCount());
229 ASSERT_TRUE(order->getDoneBuilding());
230 auto localMonRes =
231 std::make_shared<storm::analysis::LocalMonotonicityResult<storm::RationalFunctionVariable>>(monRes.begin()->second.first, order->getNumberOfStates());
232
233 // Modelcheckers
234 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
235 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
236
237 // start testing
238 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
239 auto expectedResult = regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
240 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
241
242 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
243 expectedResult = regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
244 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
245
246 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
247 expectedResult = regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
248 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
249}
250
251TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_GEQ_Incr) {
252 typedef typename TestFixture::ValueType ValueType;
253
254 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2_mon_incr.pm";
255 std::string formulaAsString = "P>=0.84 [F s=5 ]";
256 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
257
258 // Program and formula
259 storm::prism::Program program = storm::api::parseProgram(programFile);
260 program = storm::utility::prism::preprocess(program, constantsAsString);
261 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
262 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
263 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
264 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
265
266 // Simplify model
267 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
268 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
269 model = simplifier.getSimplifiedModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
270 formulas[0] = simplifier.getSimplifiedFormula();
271
272 // Apply bisimulation
273 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
274 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
275 bisimType = storm::storage::BisimulationType::Weak;
276 }
277 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
278 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
279
280 // Model parameters
281 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
282 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
283 modelParameters.insert(rewParameters.begin(), rewParameters.end());
284
285 // Reachability order, as it is already done building we don't need to recreate the order for each region
286 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
287 auto monRes = monHelper->checkMonotonicityInBuild(std::cout);
288 auto order = monRes.begin()->first;
289 ASSERT_EQ(order->getNumberOfAddedStates(), model->getTransitionMatrix().getColumnCount());
290 ASSERT_TRUE(order->getDoneBuilding());
291 auto localMonRes =
292 std::make_shared<storm::analysis::LocalMonotonicityResult<storm::RationalFunctionVariable>>(monRes.begin()->second.first, order->getNumberOfStates());
293
294 // Modelcheckers
295 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
296 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
297
298 // start testing
299 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
300 auto expectedResult = regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
301 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
302
303 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
304 expectedResult = regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
305 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
306
307 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
308 expectedResult = regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true);
309 EXPECT_EQ(expectedResult, regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
310}
311
312TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Parametric_Die_Mon) {
313 typedef typename TestFixture::ValueType ValueType;
314
315 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die_2.pm";
316 std::string formulaAsString = "P <=0.5 [F s=7 & d=2 ]";
317 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
318
319 // Program and formula
320 storm::prism::Program program = storm::api::parseProgram(programFile);
321 program = storm::utility::prism::preprocess(program, constantsAsString);
322 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
323 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
324 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
325 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
326
327 // Model parameters
328 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
329 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
330 modelParameters.insert(rewParameters.begin(), rewParameters.end());
331
332 // Simplify model
333 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
334 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
335 model = simplifier.getSimplifiedModel()->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
336 formulas[0] = simplifier.getSimplifiedFormula();
337
338 // Apply bisimulation
339 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
340 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
341 bisimType = storm::storage::BisimulationType::Weak;
342 }
343 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
344 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
345
346 // Modelcheckers
347 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
348 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
349
350 // Start testing, localMonRes will remain the same
351 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.2,0.8<=q<=0.9", modelParameters);
352 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
353 auto order = monHelper->checkMonotonicityInBuild(std::cout).begin()->first;
354 auto monRes = monHelper->createLocalMonotonicityResult(order, allSatRegion);
355 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
356 regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
357
358 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9,0.1<=q<=0.9", modelParameters);
359 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
360 regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
361
362 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=p<=0.9,0.1<=q<=0.2", modelParameters);
363 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
364 regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
365}
366
367TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Simple1_Mon) {
368 typedef typename TestFixture::ValueType ValueType;
369
370 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
371 std::string formulaAsString = "P<0.75 [F s=3 ]";
372 std::string constantsAsString = "";
373
374 // Program and formula
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 // Model parameters
383 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
384 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
385 modelParameters.insert(rewParameters.begin(), rewParameters.end());
386
387 // Modelcheckers
388 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
389 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
390
391 // Start testing
392 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p<=0.6", modelParameters);
393 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
394 auto order = monHelper->checkMonotonicityInBuild(std::cout).begin()->first;
395 auto monRes = monHelper->createLocalMonotonicityResult(order, allSatRegion);
396 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
397 regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
398
399 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
400 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
401 regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
402
403 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.05<=p<=0.1", modelParameters);
404 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
405 regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
406}
407
408TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Casestudy1_Mon) {
409 typedef typename TestFixture::ValueType ValueType;
410
411 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
412 std::string formulaAsString = "P<0.5 [F s=3 ]";
413 std::string constantsAsString = "";
414
415 // Program and formula
416 storm::prism::Program program = storm::api::parseProgram(programFile);
417 program = storm::utility::prism::preprocess(program, constantsAsString);
418 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
419 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
420 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
421 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
422
423 // Model parameters
424 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
425 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
426 modelParameters.insert(rewParameters.begin(), rewParameters.end());
427
428 // Modelcheckers
429 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
430 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
431
432 // Start testing
433 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.5", modelParameters);
434 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
435 auto order = monHelper->checkMonotonicityInBuild(std::cout).begin()->first;
436 auto monRes = monHelper->createLocalMonotonicityResult(order, allSatRegion);
437 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
438 regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
439
440 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p<=0.8", modelParameters);
441 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
442 regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
443
444 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=p<=0.9", modelParameters);
445 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
446 regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
447}
448
449TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Casestudy2_Mon) {
450 typedef typename TestFixture::ValueType ValueType;
451
452 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
453 std::string formulaAsString = "P<0.5 [F s=4 ]";
454 std::string constantsAsString = "";
455
456 // Program and formula
457 storm::prism::Program program = storm::api::parseProgram(programFile);
458 program = storm::utility::prism::preprocess(program, 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 // Model parameters
465 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
466 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
467 modelParameters.insert(rewParameters.begin(), rewParameters.end());
468
469 // Modelcheckers
470 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
471 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
472
473 // Start testing
474 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.4", modelParameters);
475 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
476 auto order = monHelper->checkMonotonicityInBuild(std::cout).begin()->first;
477 auto monRes = monHelper->createLocalMonotonicityResult(order, allSatRegion);
478 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
479 regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
480
481 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p<=0.9", modelParameters);
482 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
483 regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
484
485 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=p<=0.9", modelParameters);
486 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
487 regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
488}
489
490TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Casestudy3_Mon) {
491 typedef typename TestFixture::ValueType ValueType;
492
493 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
494 std::string formulaAsString = "P<0.5 [F s=3 ]";
495 std::string constantsAsString = "";
496
497 // Program and formula
498 storm::prism::Program program = storm::api::parseProgram(programFile);
499 program = storm::utility::prism::preprocess(program, constantsAsString);
500 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
501 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
502 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
503 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
504
505 // Model parameters
506 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
507 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
508 modelParameters.insert(rewParameters.begin(), rewParameters.end());
509
510 // Modelcheckers
511 auto regionCheckerMon = this->initializeRegionModelChecker(model, formulas[0], true);
512 auto regionChecker = this->initializeRegionModelChecker(model, formulas[0], false);
513
514 model->getTransitionMatrix().printAsMatlabMatrix(std::cout);
515
516 auto monHelper = new storm::analysis::MonotonicityHelper<storm::RationalFunction, ValueType>(model, formulas, {});
517 auto order = monHelper->checkMonotonicityInBuild(std::cout).begin()->first;
518 ASSERT_TRUE(order->getDoneBuilding());
519
520 // Start testing
521 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p<=0.9", modelParameters);
522 auto monRes = monHelper->createLocalMonotonicityResult(order, allSatRegion);
523 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
524 regionCheckerMon->analyzeRegion(this->env(), allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
525
526 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.3<=p<=0.7", modelParameters);
527 monRes = monHelper->createLocalMonotonicityResult(order, exBothRegion);
528 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
529 regionCheckerMon->analyzeRegion(this->env(), exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
530
531 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.4", modelParameters);
532 monRes = monHelper->createLocalMonotonicityResult(order, allVioRegion);
533 EXPECT_EQ(regionChecker->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true),
534 regionCheckerMon->analyzeRegion(this->env(), allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
535}
536} // 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::analysis::MonotonicityHelper::checkMonotonicityInBuild
std::map< std::shared_ptr< Order >, std::pair< std::shared_ptr< MonotonicityResult< VariableType > >, std::vector< std::shared_ptr< expressions::BinaryRelationExpression > > > > checkMonotonicityInBuild(std::ostream &outfile, bool usePLA=false, std::string dotOutfileName="dotOutput")
Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity...
Definition MonotonicityHelper.cpp:82
storm::analysis::MonotonicityHelper::createLocalMonotonicityResult
std::shared_ptr< LocalMonotonicityResult< VariableType > > createLocalMonotonicityResult(std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region)
Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity...
Definition MonotonicityHelper.cpp:159
storm::models::ModelBase::as
std::shared_ptr< ModelType > as()
Casts the model into the model type given by the template parameter.
Definition ModelBase.h:38
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::transformer::SparseParametricDtmcSimplifier
This class performs different steps to simplify the given (parametric) model.
Definition SparseParametricDtmcSimplifier.h:15
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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
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:46
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:136
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::performBisimulationMinimization
std::shared_ptr< storm::models::sparse::Model< ValueType > > performBisimulationMinimization(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::BisimulationType type=storm::storage::BisimulationType::Strong, bool graphPreserving=true)
Definition bisimulation.h:61
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::api::MonotonicitySetting
storm::pars::modelchecker::MonotonicityOptions MonotonicitySetting
Definition region.h:46
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
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::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::settings::getModule
SettingsType const & getModule()
Get module.
Definition SettingsManager.h:290
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
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:135
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