Storm 1.14.0.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/region.h"
5#include "storm-pars/modelchecker/region/monotonicity/MonotonicityChecker.h"
6#include "storm-pars/modelchecker/region/monotonicity/Order.h"
7#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h"
8#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
9#include "storm-parsers/api/model_descriptions.h"
10#include "storm-parsers/api/properties.h"
11#include "storm-parsers/parser/PrismParser.h"
12#include "storm/adapters/RationalFunctionAdapter.h"
13#include "storm/api/builder.h"
14#include "storm/api/properties.h"
15#include "storm/logic/Formulas.h"
16#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
17#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
18#include "storm/storage/SparseMatrix.h"
19#include "storm/utility/graph.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 = program.preprocess(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 =
59 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
60 // Get the maybeStates
61 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
62 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
63 storm::storage::BitVector topStates = statesWithProbability01.second;
64 storm::storage::BitVector bottomStates = statesWithProbability01.first;
65 // OrderExtender
66 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
67 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
68 // Order
69 auto order = std::get<0>(orderExtender.toOrder(region, nullptr));
70 // monchecker
71 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(model->getTransitionMatrix());
72
73 // start testing
74 auto var = modelParameters.begin();
75 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
76 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
77}
78
79TEST_F(MonotonicityCheckerTest, Simple1_small_region) {
80 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
81 std::string formulaAsString = "P=? [F s=3 ]";
82 std::string constantsAsString = "";
83
84 // model
85 storm::prism::Program program = storm::api::parseProgram(programFile);
86 program = program.preprocess(constantsAsString);
87 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
88 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
89 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
90 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
91 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
92 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
93 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
94 model = simplifier.getSimplifiedModel();
95
96 // Create the region
97 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
98 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
99 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
100
101 // For order extender
102 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
103 storm::storage::BitVector phiStates;
104 storm::storage::BitVector psiStates;
105 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
106 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
107 psiStates =
108 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
109 // Get the maybeStates
110 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
111 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
112 storm::storage::BitVector topStates = statesWithProbability01.second;
113 storm::storage::BitVector bottomStates = statesWithProbability01.first;
114 // OrderExtender
115 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
116 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
117 // Order
118 auto order = std::get<0>(orderExtender.toOrder(region, nullptr));
119 // monchecker
120 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(model->getTransitionMatrix());
121
122 // start testing
123 auto var = modelParameters.begin();
124 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 0, *var, region));
125 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
126 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
127}
128
129TEST_F(MonotonicityCheckerTest, Casestudy1) {
130 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
131 std::string formulaAsString = "P=? [F s=3 ]";
132 std::string constantsAsString = "";
133
134 // model
135 storm::prism::Program program = storm::api::parseProgram(programFile);
136 program = program.preprocess(constantsAsString);
137 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
138 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
139 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
140 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
141 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
142 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
143 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
144 model = simplifier.getSimplifiedModel();
145
146 // Create the region
147 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
148 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
149 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
150
151 // For order extender
152 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
153 storm::storage::BitVector phiStates;
154 storm::storage::BitVector psiStates;
155 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
156 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
157 psiStates =
158 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
159 // Get the maybeStates
160 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
161 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
162 storm::storage::BitVector topStates = statesWithProbability01.second;
163 storm::storage::BitVector bottomStates = statesWithProbability01.first;
164 // OrderExtender
165 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
166 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
167 // Order
168 auto res = orderExtender.extendOrder(nullptr, region);
169 auto order = std::get<0>(res);
170 ASSERT_TRUE(order->getDoneBuilding());
171
172 // monchecker
173 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
174
175 // start testing
176 auto var = modelParameters.begin();
177 for (uint_fast64_t i = 0; i < 3; i++) {
178 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr,
179 monChecker->checkLocalMonotonicity(order, i, *var, region));
180 }
181}
182
183TEST_F(MonotonicityCheckerTest, Casestudy2) {
184 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
185 std::string formulaAsString = "P=? [F s=4 ]";
186 std::string constantsAsString = "";
187
188 // model
189 storm::prism::Program program = storm::api::parseProgram(programFile);
190 program = program.preprocess(constantsAsString);
191 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
192 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
193 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
194 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
195 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
196 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
197 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
198 model = simplifier.getSimplifiedModel();
199
200 // Create the region
201 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
202 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
203 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
204
205 // For order extender
206 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
207 storm::storage::BitVector phiStates;
208 storm::storage::BitVector psiStates;
209 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
210 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
211 psiStates =
212 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
213 // Get the maybeStates
214 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
215 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
216 storm::storage::BitVector topStates = statesWithProbability01.second;
217 storm::storage::BitVector bottomStates = statesWithProbability01.first;
218 // OrderExtender
219 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
220 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
221 // Order
222 auto res = orderExtender.extendOrder(nullptr, region);
223 auto order = std::get<0>(res);
224 order->addRelation(1, 3);
225 order->addRelation(3, 2);
226
227 // monchecker
228 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
229
230 // start testing
231 auto var = modelParameters.begin();
232 for (uint_fast64_t i = 0; i < 3; i++) {
233 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr,
234 monChecker->checkLocalMonotonicity(order, i, *var, region));
235 }
236}
237
238TEST_F(MonotonicityCheckerTest, Casestudy3) {
239 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
240 std::string formulaAsString = "P=? [F s=3 ]";
241 std::string constantsAsString = "";
242
243 // model
244 storm::prism::Program program = storm::api::parseProgram(programFile);
245 program = program.preprocess(constantsAsString);
246 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
247 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
248 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
249 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
250 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
251 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
252 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
253 model = simplifier.getSimplifiedModel();
254
255 // Create the region
256 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
257 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
258 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
259
260 // For order extender
261 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
262 storm::storage::BitVector phiStates;
263 storm::storage::BitVector psiStates;
264 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
265 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
266 psiStates =
267 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
268 // Get the maybeStates
269 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
270 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
271 storm::storage::BitVector topStates = statesWithProbability01.second;
272 storm::storage::BitVector bottomStates = statesWithProbability01.first;
273 // OrderExtender
274 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
275 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
276 // Order
277 auto res = orderExtender.extendOrder(nullptr, region);
278 auto order = std::get<0>(res);
279 ASSERT_TRUE(order->getDoneBuilding());
280
281 // monchecker
282 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
283
284 // start testing
285 auto var = modelParameters.begin();
286 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Not, 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
290 region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
291 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 0, *var, region));
292 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
293 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
294}
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: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:38
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::prism::Program::preprocess
Program preprocess(std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
Preprocesses the program by defining the given constant definitions, substituting constants and formu...
Definition Program.cpp:1170
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:329
storm::transformer::SparseParametricDtmcSimplifier
This class performs different steps to simplify the given (parametric) model.
Definition SparseParametricDtmcSimplifier.h:15
model_descriptions.h
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::parseRegion
storm::storage::ParameterRegion< ValueType > parseRegion(std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)
Definition region.h:133
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options, typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &explorationOptions=typename storm::builder::ExplicitModelBuilder< ValueType >::Options())
Definition builder.h:117
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:62
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:694
storm::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_gtest.h