Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MonotonicityCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/api/storm-pars.h"
5#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
6#include "storm-parsers/api/storm-parsers.h"
7#include "storm-parsers/parser/PrismParser.h"
8#include "storm/adapters/RationalFunctionAdapter.h"
9#include "storm/api/builder.h"
10#include "storm/api/storm.h"
11#include "storm/logic/Formulas.h"
12#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
13#include "storm/storage/SparseMatrix.h"
14#include "storm/utility/graph.h"
15
16class MonotonicityCheckerTest : public ::testing::Test {
17 protected:
18 void SetUp() override {
19#ifndef STORM_HAVE_Z3
20 GTEST_SKIP() << "Z3 not available.";
21#endif
22 }
23};
24
25TEST_F(MonotonicityCheckerTest, Simple1_larger_region) {
26 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
27 std::string formulaAsString = "P=? [F s=3 ]";
28 std::string constantsAsString = "";
29
30 // model
31 storm::prism::Program program = storm::api::parseProgram(programFile);
32 program = storm::utility::prism::preprocess(program, constantsAsString);
33 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
34 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
35 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
36 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
37 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
38 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
39 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
40 model = simplifier.getSimplifiedModel();
41
42 // Create the region
43 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
44 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
45 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
46
47 // For order extender
48 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
49 storm::storage::BitVector phiStates;
50 storm::storage::BitVector psiStates;
51 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
52 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
53 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
54 // Get the maybeStates
55 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
56 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
57 storm::storage::BitVector topStates = statesWithProbability01.second;
58 storm::storage::BitVector bottomStates = statesWithProbability01.first;
59 // OrderExtender
60 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
61 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
62 // Order
63 auto order = std::get<0>(orderExtender.toOrder(region, nullptr));
64 // monchecker
65 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(model->getTransitionMatrix());
66
67 // start testing
68 auto var = modelParameters.begin();
69 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
70 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
71}
72
73TEST_F(MonotonicityCheckerTest, Simple1_small_region) {
74 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
75 std::string formulaAsString = "P=? [F s=3 ]";
76 std::string constantsAsString = "";
77
78 // model
79 storm::prism::Program program = storm::api::parseProgram(programFile);
80 program = storm::utility::prism::preprocess(program, constantsAsString);
81 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
82 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
83 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
84 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
85 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
86 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
87 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
88 model = simplifier.getSimplifiedModel();
89
90 // Create the region
91 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
92 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
93 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
94
95 // For order extender
96 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
97 storm::storage::BitVector phiStates;
98 storm::storage::BitVector psiStates;
99 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
100 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
101 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
102 // Get the maybeStates
103 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
104 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
105 storm::storage::BitVector topStates = statesWithProbability01.second;
106 storm::storage::BitVector bottomStates = statesWithProbability01.first;
107 // OrderExtender
108 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
109 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
110 // Order
111 auto order = std::get<0>(orderExtender.toOrder(region, nullptr));
112 // monchecker
113 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(model->getTransitionMatrix());
114
115 // start testing
116 auto var = modelParameters.begin();
117 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 0, *var, region));
118 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
119 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
120}
121
122TEST_F(MonotonicityCheckerTest, Casestudy1) {
123 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
124 std::string formulaAsString = "P=? [F s=3 ]";
125 std::string constantsAsString = "";
126
127 // model
128 storm::prism::Program program = storm::api::parseProgram(programFile);
129 program = storm::utility::prism::preprocess(program, constantsAsString);
130 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
131 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
132 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
133 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
134 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
135 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
136 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
137 model = simplifier.getSimplifiedModel();
138
139 // Create the region
140 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
141 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
142 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
143
144 // For order extender
145 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
146 storm::storage::BitVector phiStates;
147 storm::storage::BitVector psiStates;
148 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
149 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
150 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
151 // Get the maybeStates
152 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
153 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
154 storm::storage::BitVector topStates = statesWithProbability01.second;
155 storm::storage::BitVector bottomStates = statesWithProbability01.first;
156 // OrderExtender
157 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
158 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
159 // Order
160 auto res = orderExtender.extendOrder(nullptr, region);
161 auto order = std::get<0>(res);
162 ASSERT_TRUE(order->getDoneBuilding());
163
164 // monchecker
165 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
166
167 // start testing
168 auto var = modelParameters.begin();
169 for (uint_fast64_t i = 0; i < 3; i++) {
170 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr,
171 monChecker->checkLocalMonotonicity(order, i, *var, region));
172 }
173}
174
175TEST_F(MonotonicityCheckerTest, Casestudy2) {
176 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
177 std::string formulaAsString = "P=? [F s=4 ]";
178 std::string constantsAsString = "";
179
180 // model
181 storm::prism::Program program = storm::api::parseProgram(programFile);
182 program = storm::utility::prism::preprocess(program, constantsAsString);
183 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
184 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
185 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
186 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
187 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
188 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
189 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
190 model = simplifier.getSimplifiedModel();
191
192 // Create the region
193 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
194 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
195 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
196
197 // For order extender
198 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
199 storm::storage::BitVector phiStates;
200 storm::storage::BitVector psiStates;
201 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
202 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
203 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
204 // Get the maybeStates
205 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
206 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
207 storm::storage::BitVector topStates = statesWithProbability01.second;
208 storm::storage::BitVector bottomStates = statesWithProbability01.first;
209 // OrderExtender
210 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
211 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
212 // Order
213 auto res = orderExtender.extendOrder(nullptr, region);
214 auto order = std::get<0>(res);
215 order->addRelation(1, 3);
216 order->addRelation(3, 2);
217
218 // monchecker
219 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
220
221 // start testing
222 auto var = modelParameters.begin();
223 for (uint_fast64_t i = 0; i < 3; i++) {
224 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr,
225 monChecker->checkLocalMonotonicity(order, i, *var, region));
226 }
227}
228
229TEST_F(MonotonicityCheckerTest, Casestudy3) {
230 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
231 std::string formulaAsString = "P=? [F s=3 ]";
232 std::string constantsAsString = "";
233
234 // model
235 storm::prism::Program program = storm::api::parseProgram(programFile);
236 program = storm::utility::prism::preprocess(program, constantsAsString);
237 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
238 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
239 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
240 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
241 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
242 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
243 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
244 model = simplifier.getSimplifiedModel();
245
246 // Create the region
247 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
248 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
249 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
250
251 // For order extender
252 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
253 storm::storage::BitVector phiStates;
254 storm::storage::BitVector psiStates;
255 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
256 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
257 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
258 // Get the maybeStates
259 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
260 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
261 storm::storage::BitVector topStates = statesWithProbability01.second;
262 storm::storage::BitVector bottomStates = statesWithProbability01.first;
263 // OrderExtender
264 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
265 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
266 // Order
267 auto res = orderExtender.extendOrder(nullptr, region);
268 auto order = std::get<0>(res);
269 ASSERT_TRUE(order->getDoneBuilding());
270
271 // monchecker
272 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
273
274 // start testing
275 auto var = modelParameters.begin();
276 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Not, monChecker->checkLocalMonotonicity(order, 0, *var, region));
277 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
278 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
279
280 region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
281 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 0, *var, region));
282 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
283 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
284}
TEST_F
TEST_F(MonotonicityCheckerTest, Simple1_larger_region)
Definition MonotonicityCheckerTest.cpp:25
storm::analysis::MonotonicityChecker::checkLocalMonotonicity
Monotonicity checkLocalMonotonicity(std::shared_ptr< Order > const &order, uint_fast64_t state, VariableType const &var, storage::ParameterRegion< ValueType > const &region)
Checks for local monotonicity at the given state.
Definition MonotonicityChecker.cpp:14
storm::logic::Formula::asProbabilityOperatorFormula
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:476
storm::logic::Formula::asEventuallyFormula
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:341
storm::logic::UnaryPathFormula::getSubformula
Formula const & getSubformula() const
Definition UnaryPathFormula.cpp:13
storm::logic::UnaryStateFormula::getSubformula
Formula const & getSubformula() const
Definition UnaryStateFormula.cpp:15
storm::modelchecker::AbstractModelChecker::check
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Definition AbstractModelChecker.cpp:49
storm::models::ModelBase::as
std::shared_ptr< ModelType > as()
Casts the model into the model type given by the template parameter.
Definition ModelBase.h:37
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::SparseMatrix
A class that holds a possibly non-square matrix in the compressed row storage format.
Definition SparseMatrix.h:328
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::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:695
storm::utility::graph::performProb01
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01(storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi i...
Definition graph.cpp:393
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_gtest.h