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