Storm 1.13.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/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 =
54 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
55 // Get the maybeStates
56 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
57 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
58 storm::storage::BitVector topStates = statesWithProbability01.second;
59 storm::storage::BitVector bottomStates = statesWithProbability01.first;
60 // OrderExtender
61 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
62 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
63 // Order
64 auto order = std::get<0>(orderExtender.toOrder(region, nullptr));
65 // monchecker
66 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(model->getTransitionMatrix());
67
68 // start testing
69 auto var = modelParameters.begin();
70 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr, monChecker->checkLocalMonotonicity(order, 1, *var, region));
71 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Decr, monChecker->checkLocalMonotonicity(order, 2, *var, region));
72}
73
74TEST_F(MonotonicityCheckerTest, Simple1_small_region) {
75 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
76 std::string formulaAsString = "P=? [F s=3 ]";
77 std::string constantsAsString = "";
78
79 // model
80 storm::prism::Program program = storm::api::parseProgram(programFile);
81 program = storm::utility::prism::preprocess(program, constantsAsString);
82 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
83 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
84 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
85 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
86 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
87 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
88 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
89 model = simplifier.getSimplifiedModel();
90
91 // Create the region
92 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
93 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
94 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
95
96 // For order extender
97 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
98 storm::storage::BitVector phiStates;
99 storm::storage::BitVector psiStates;
100 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
101 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
102 psiStates =
103 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().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 =
153 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
154 // Get the maybeStates
155 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
156 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
157 storm::storage::BitVector topStates = statesWithProbability01.second;
158 storm::storage::BitVector bottomStates = statesWithProbability01.first;
159 // OrderExtender
160 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
161 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
162 // Order
163 auto res = orderExtender.extendOrder(nullptr, region);
164 auto order = std::get<0>(res);
165 ASSERT_TRUE(order->getDoneBuilding());
166
167 // monchecker
168 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
169
170 // start testing
171 auto var = modelParameters.begin();
172 for (uint_fast64_t i = 0; i < 3; i++) {
173 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr,
174 monChecker->checkLocalMonotonicity(order, i, *var, region));
175 }
176}
177
178TEST_F(MonotonicityCheckerTest, Casestudy2) {
179 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
180 std::string formulaAsString = "P=? [F s=4 ]";
181 std::string constantsAsString = "";
182
183 // model
184 storm::prism::Program program = storm::api::parseProgram(programFile);
185 program = storm::utility::prism::preprocess(program, constantsAsString);
186 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
187 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
188 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
189 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
190 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
191 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
192 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
193 model = simplifier.getSimplifiedModel();
194
195 // Create the region
196 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
197 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
198 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
199
200 // For order extender
201 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
202 storm::storage::BitVector phiStates;
203 storm::storage::BitVector psiStates;
204 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
205 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
206 psiStates =
207 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
208 // Get the maybeStates
209 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
210 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
211 storm::storage::BitVector topStates = statesWithProbability01.second;
212 storm::storage::BitVector bottomStates = statesWithProbability01.first;
213 // OrderExtender
214 storm::storage::SparseMatrix<storm::RationalFunction> matrix = model->getTransitionMatrix();
215 auto orderExtender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, matrix);
216 // Order
217 auto res = orderExtender.extendOrder(nullptr, region);
218 auto order = std::get<0>(res);
219 order->addRelation(1, 3);
220 order->addRelation(3, 2);
221
222 // monchecker
223 auto monChecker = new storm::analysis::MonotonicityChecker<storm::RationalFunction>(matrix);
224
225 // start testing
226 auto var = modelParameters.begin();
227 for (uint_fast64_t i = 0; i < 3; i++) {
228 EXPECT_EQ(storm::analysis::MonotonicityChecker<storm::RationalFunction>::Monotonicity::Incr,
229 monChecker->checkLocalMonotonicity(order, i, *var, region));
230 }
231}
232
233TEST_F(MonotonicityCheckerTest, Casestudy3) {
234 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
235 std::string formulaAsString = "P=? [F s=3 ]";
236 std::string constantsAsString = "";
237
238 // model
239 storm::prism::Program program = storm::api::parseProgram(programFile);
240 program = storm::utility::prism::preprocess(program, constantsAsString);
241 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
242 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
243 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
244 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
245 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
246 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
247 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
248 model = simplifier.getSimplifiedModel();
249
250 // Create the region
251 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
252 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1<=p<=0.9", modelParameters);
253 std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions = {region};
254
255 // For order extender
256 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
257 storm::storage::BitVector phiStates;
258 storm::storage::BitVector psiStates;
259 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
260 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
261 psiStates =
262 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().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: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:38
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:329
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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
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:136
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: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::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