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