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