Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
OrderExtenderTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include <memory>
5#include <vector>
6
7#include "storm-pars/api/region.h"
8#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h"
9#include "storm-pars/modelchecker/region/monotonicity/Order.h"
10#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h"
11#include "storm-pars/transformer/SparseParametricModelSimplifier.h"
12#include "storm-parsers/api/model_descriptions.h"
13#include "storm-parsers/api/properties.h"
14#include "storm-parsers/parser/AutoParser.h"
15#include "storm-parsers/parser/PrismParser.h"
16#include "storm/api/bisimulation.h"
17#include "storm/api/builder.h"
18#include "storm/api/properties.h"
19#include "storm/logic/Formulas.h"
20#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
21#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
22#include "storm/models/sparse/StandardRewardModel.h"
23#include "storm/utility/graph.h"
24
25class OrderExtenderTest : public ::testing::Test {
26 protected:
27 void SetUp() override {
28#ifndef STORM_HAVE_Z3
29 GTEST_SKIP() << "Z3 not available.";
30#endif
31 }
32};
33
34TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_model) {
35 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
36 std::string formulaAsString = "P=? [F s=4 & i=N ]";
37 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
38
39 // Program and formula
40 storm::prism::Program program = storm::api::parseProgram(programFile);
41 program = program.preprocess(constantsAsString);
42 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
43 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
44 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
45 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
46 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
47 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
48 model = simplifier.getSimplifiedModel();
49
50 // Apply bisimulation
51 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
52
53 ASSERT_EQ(99ul, model->getNumberOfStates());
54 ASSERT_EQ(195ul, model->getNumberOfTransitions());
55
56 auto vars = storm::models::sparse::getProbabilityParameters(*model);
57 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
58
59 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
60 auto monRes = new storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>;
61 auto criticalTuple = extender.toOrder(
62 region,
63 std::make_shared<storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>>(*monRes));
64 EXPECT_EQ(model->getNumberOfStates(), std::get<1>(criticalTuple));
65 EXPECT_EQ(model->getNumberOfStates(), std::get<2>(criticalTuple));
66
67 auto order = std::get<0>(criticalTuple);
68 for (uint_fast64_t i = 0; i < model->getNumberOfStates(); ++i) {
69 EXPECT_TRUE((order->contains(i)));
70 }
71
72 // Check on some nodes. The state indices refer to the bisimulation quotient. If that numbering changes, these indices have to be adapted.
73 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(97, 98));
74 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(97, 4));
75 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(4, 98));
76 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(6, 4));
77 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(94, 88));
78}
79
80TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_model) {
81 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
82 std::string formulaAsString = "P=? [F s=4 & i=N ]";
83 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
84
85 // Program and formula
86 storm::prism::Program program = storm::api::parseProgram(programFile);
87 program = program.preprocess(constantsAsString);
88 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
89 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
90 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
91 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
92 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
93 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
94 model = simplifier.getSimplifiedModel();
95
96 ASSERT_EQ(193ul, model->getNumberOfStates());
97 ASSERT_EQ(383ul, model->getNumberOfTransitions());
98
99 auto vars = storm::models::sparse::getProbabilityParameters(*model);
100 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
101
102 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
103 auto monRes = new storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>;
104 auto criticalTuple = extender.toOrder(
105 region,
106 std::make_shared<storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>>(*monRes));
107 EXPECT_EQ(183ul, std::get<1>(criticalTuple));
108 EXPECT_EQ(186ul, std::get<2>(criticalTuple));
109}
110
111TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_matrix) {
112 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
113 std::string formulaAsString = "P=? [F s=4 & i=N ]";
114 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
115
116 // Program and formula
117 storm::prism::Program program = storm::api::parseProgram(programFile);
118 program = program.preprocess(constantsAsString);
119 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
120 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
121 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
122 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
123 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
124 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
125 model = simplifier.getSimplifiedModel();
126
127 // Apply bisimulation
128 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
129
130 ASSERT_EQ(99ul, model->getNumberOfStates());
131 ASSERT_EQ(195ul, model->getNumberOfTransitions());
132
133 auto vars = storm::models::sparse::getProbabilityParameters(*model);
134 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
135 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
136 storm::storage::BitVector phiStates;
137 storm::storage::BitVector psiStates;
138 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
139 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
140 psiStates =
141 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
142 // Get the maybeStates
143 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
144 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
145 storm::storage::BitVector topStates = statesWithProbability01.second;
146 storm::storage::BitVector bottomStates = statesWithProbability01.first;
147
148 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
149 auto res = extender.extendOrder(nullptr, region);
150 auto order = std::get<0>(res);
151 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
152 EXPECT_TRUE(order->getDoneBuilding());
153
154 // Check on some nodes. The state indices refer to the bisimulation quotient. If that numbering changes, these indices have to be adapted.
155 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(97, 98));
156 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(97, 4));
157 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(4, 98));
158 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(6, 4));
159 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(94, 88));
160}
161
162TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) {
163 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
164 std::string formulaAsString = "P=? [F s=4 & i=N ]";
165 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
166
167 // Program and formula
168 storm::prism::Program program = storm::api::parseProgram(programFile);
169 program = program.preprocess(constantsAsString);
170 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
171 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
172 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
173 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
174 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
175 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
176 model = simplifier.getSimplifiedModel();
177
178 ASSERT_EQ(193ul, model->getNumberOfStates());
179 ASSERT_EQ(383ul, model->getNumberOfTransitions());
180
181 auto vars = storm::models::sparse::getProbabilityParameters(*model);
182 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
183 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
184 storm::storage::BitVector phiStates;
185 storm::storage::BitVector psiStates;
186 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
187 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
188 psiStates =
189 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
190 // Get the maybeStates
191 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
192 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
193 storm::storage::BitVector topStates = statesWithProbability01.second;
194 storm::storage::BitVector bottomStates = statesWithProbability01.first;
195
196 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
197 auto res = extender.extendOrder(nullptr, region);
198 auto order = std::get<0>(res);
199 EXPECT_FALSE(order->getDoneBuilding());
200}
201
202TEST_F(OrderExtenderTest, simple1_on_model) {
203 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
204 std::string formulaAsString = "P=? [F s=3 ]";
205 std::string constantsAsString = "";
206
207 // model
208 storm::prism::Program program = storm::api::parseProgram(programFile);
209 program = program.preprocess(constantsAsString);
210 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
211 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
212 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
213 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
214 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
215 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
216 model = simplifier.getSimplifiedModel();
217
218 // Create the region
219 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
220 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
221
222 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
223 auto order = std::get<0>(extender.toOrder(region));
224 EXPECT_EQ(5ul, order->getNumberOfAddedStates());
225 EXPECT_TRUE(order->getDoneBuilding());
226
227 // Check on all states
228 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
229 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
230 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
231 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
232 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
233 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
234 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
235 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
236 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
237 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
238}
239
240TEST_F(OrderExtenderTest, simple1_on_matrix) {
241 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
242 std::string formulaAsString = "P=? [F s=3 ]";
243 std::string constantsAsString = "";
244
245 // model
246 storm::prism::Program program = storm::api::parseProgram(programFile);
247 program = program.preprocess(constantsAsString);
248 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
249 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
250 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
251 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
252 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
253 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
254 model = simplifier.getSimplifiedModel();
255
256 // Create the region
257 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
258 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.9", modelParameters);
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
274 // OrderExtender
275 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
276 auto res = extender.extendOrder(nullptr, region);
277 auto order = std::get<0>(res);
278 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
279 EXPECT_TRUE(order->getDoneBuilding());
280
281 // Check on all states, as this one automatically handles assumptions (if there is one valid) all are ABOVE
282 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
283 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
284 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
285 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
286 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
287 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
288 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
289 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
290 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
291 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
292}
293
294TEST_F(OrderExtenderTest, casestudy1_on_model) {
295 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
296 std::string formulaAsString = "P=? [F s=3 ]";
297 std::string constantsAsString = "";
298
299 // model
300 storm::prism::Program program = storm::api::parseProgram(programFile);
301 program = program.preprocess(constantsAsString);
302 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
303 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
304 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
305 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
306 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
307 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
308 model = simplifier.getSimplifiedModel();
309
310 // Create the region
311 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
312 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
313
314 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
315 auto order = std::get<0>(extender.toOrder(region));
316
317 EXPECT_EQ(5ul, order->getNumberOfAddedStates());
318 EXPECT_TRUE(order->getDoneBuilding());
319 // Check on all states
320 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
321 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
322 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
323 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
324 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
325 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
326 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
327 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
328 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
329 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
330}
331
332TEST_F(OrderExtenderTest, casestudy1_on_matrix) {
333 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
334 std::string formulaAsString = "P=? [F s=3 ]";
335 std::string constantsAsString = "";
336
337 // model
338 storm::prism::Program program = storm::api::parseProgram(programFile);
339 program = program.preprocess(constantsAsString);
340 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
341 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
342 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
343 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
344 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
345 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
346 model = simplifier.getSimplifiedModel();
347
348 // Create the region
349 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
350 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.9", modelParameters);
351
352 // For order extender
353 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
354 storm::storage::BitVector phiStates;
355 storm::storage::BitVector psiStates;
356 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
357 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
358 psiStates =
359 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
360 // Get the maybeStates
361 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
362 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
363 storm::storage::BitVector topStates = statesWithProbability01.second;
364 storm::storage::BitVector bottomStates = statesWithProbability01.first;
365
366 // OrderExtender
367 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
368 auto res = extender.extendOrder(nullptr, region);
369 auto order = std::get<0>(res);
370 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
371 EXPECT_TRUE(order->getDoneBuilding());
372
373 // Check on all states
374 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
375 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
376 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
377 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
378 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
379 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
380 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
381 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
382 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
383 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
384}
385
386TEST_F(OrderExtenderTest, casestudy2_on_matrix) {
387 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
388 std::string formulaAsString = "P=? [F s=4 ]";
389 std::string constantsAsString = "";
390
391 // model
392 storm::prism::Program program = storm::api::parseProgram(programFile);
393 program = program.preprocess(constantsAsString);
394 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
395 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
396 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
397 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
398 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
399 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
400 model = simplifier.getSimplifiedModel();
401
402 // Create the region
403 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
404 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1 <= p <= 0.2", modelParameters);
405
406 // For order extender
407 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
408 storm::storage::BitVector phiStates;
409 storm::storage::BitVector psiStates;
410 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
411 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
412 psiStates =
413 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
414 // Get the maybeStates
415 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
416 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
417 storm::storage::BitVector topStates = statesWithProbability01.second;
418 storm::storage::BitVector bottomStates = statesWithProbability01.first;
419
420 // OrderExtender
421 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
422 auto res = extender.extendOrder(nullptr, region);
423 EXPECT_TRUE(std::get<0>(res)->getDoneBuilding());
424}
TEST_F
TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_model)
Definition OrderExtenderTest.cpp:34
OrderExtenderTest::SetUp
void SetUp() override
Definition OrderExtenderTest.cpp:27
storm::analysis::OrderExtender::VariableType
utility::parametric::VariableType< ValueType >::type VariableType
Definition OrderExtender.h:23
storm::logic::Formula::asProbabilityOperatorFormula
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:506
storm::logic::Formula::asEventuallyFormula
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:371
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:16
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::transformer::SparseParametricModelSimplifier
This class performs different steps to simplify the given (parametric) model.
Definition SparseParametricModelSimplifier.h:21
model_descriptions.h
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:134
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:70
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::api::performBisimulationMinimization
std::shared_ptr< storm::models::sparse::Model< ValueType > > performBisimulationMinimization(std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas={}, storm::bisimulation::Options const &options={})
Definition bisimulation.h:17
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:732
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:394
storm_gtest.h