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/SparseParametricDtmcSimplifier.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::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
47 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
48 model = simplifier.getSimplifiedModel();
49
50 // Apply bisimulation
51 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
52
53 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
54 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
55
56 ASSERT_EQ(99ul, model->getNumberOfStates());
57 ASSERT_EQ(195ul, model->getNumberOfTransitions());
58
59 auto vars = storm::models::sparse::getProbabilityParameters(*model);
60 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
61
62 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
63 auto monRes = new storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>;
64 auto criticalTuple = extender.toOrder(
65 region,
66 std::make_shared<storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>>(*monRes));
67 EXPECT_EQ(model->getNumberOfStates(), std::get<1>(criticalTuple));
68 EXPECT_EQ(model->getNumberOfStates(), std::get<2>(criticalTuple));
69
70 auto order = std::get<0>(criticalTuple);
71 for (uint_fast64_t i = 0; i < model->getNumberOfStates(); ++i) {
72 EXPECT_TRUE((order->contains(i)));
73 }
74
75 // Check on some nodes
76 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
77 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 5));
78 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5, 0));
79 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94, 5));
80 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7, 13));
81}
82
83TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_model) {
84 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
85 std::string formulaAsString = "P=? [F s=4 & i=N ]";
86 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
87
88 // Program and formula
89 storm::prism::Program program = storm::api::parseProgram(programFile);
90 program = program.preprocess(constantsAsString);
91 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
92 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
93 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
94 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
95 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
96 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
97 model = simplifier.getSimplifiedModel();
98
99 ASSERT_EQ(193ul, model->getNumberOfStates());
100 ASSERT_EQ(383ul, model->getNumberOfTransitions());
101
102 auto vars = storm::models::sparse::getProbabilityParameters(*model);
103 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
104
105 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
106 auto monRes = new storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>;
107 auto criticalTuple = extender.toOrder(
108 region,
109 std::make_shared<storm::analysis::MonotonicityResult<typename storm::analysis::OrderExtender<storm::RationalFunction, double>::VariableType>>(*monRes));
110 EXPECT_EQ(183ul, std::get<1>(criticalTuple));
111 EXPECT_EQ(186ul, std::get<2>(criticalTuple));
112}
113
114TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_matrix) {
115 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
116 std::string formulaAsString = "P=? [F s=4 & i=N ]";
117 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
118
119 // Program and formula
120 storm::prism::Program program = storm::api::parseProgram(programFile);
121 program = program.preprocess(constantsAsString);
122 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
123 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
124 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
125 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
126 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
127 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
128 model = simplifier.getSimplifiedModel();
129
130 // Apply bisimulation
131 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
132
133 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
134 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
135
136 ASSERT_EQ(99ul, model->getNumberOfStates());
137 ASSERT_EQ(195ul, model->getNumberOfTransitions());
138
139 auto vars = storm::models::sparse::getProbabilityParameters(*model);
140 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
141 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
142 storm::storage::BitVector phiStates;
143 storm::storage::BitVector psiStates;
144 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
145 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
146 psiStates =
147 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
148 // Get the maybeStates
149 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
150 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
151 storm::storage::BitVector topStates = statesWithProbability01.second;
152 storm::storage::BitVector bottomStates = statesWithProbability01.first;
153
154 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
155 auto res = extender.extendOrder(nullptr, region);
156 auto order = std::get<0>(res);
157 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
158 EXPECT_TRUE(order->getDoneBuilding());
159
160 // Check on some nodes
161 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
162 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 5));
163 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5, 0));
164 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94, 5));
165 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7, 13));
166}
167
168TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) {
169 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
170 std::string formulaAsString = "P=? [F s=4 & i=N ]";
171 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
172
173 // Program and formula
174 storm::prism::Program program = storm::api::parseProgram(programFile);
175 program = program.preprocess(constantsAsString);
176 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
177 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
178 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
179 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
180 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
181 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
182 model = simplifier.getSimplifiedModel();
183
184 ASSERT_EQ(193ul, model->getNumberOfStates());
185 ASSERT_EQ(383ul, model->getNumberOfTransitions());
186
187 auto vars = storm::models::sparse::getProbabilityParameters(*model);
188 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
189 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
190 storm::storage::BitVector phiStates;
191 storm::storage::BitVector psiStates;
192 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
193 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
194 psiStates =
195 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
196 // Get the maybeStates
197 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
198 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
199 storm::storage::BitVector topStates = statesWithProbability01.second;
200 storm::storage::BitVector bottomStates = statesWithProbability01.first;
201
202 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
203 auto res = extender.extendOrder(nullptr, region);
204 auto order = std::get<0>(res);
205 EXPECT_FALSE(order->getDoneBuilding());
206}
207
208TEST_F(OrderExtenderTest, simple1_on_model) {
209 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
210 std::string formulaAsString = "P=? [F s=3 ]";
211 std::string constantsAsString = "";
212
213 // model
214 storm::prism::Program program = storm::api::parseProgram(programFile);
215 program = program.preprocess(constantsAsString);
216 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
217 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
218 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
219 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
220 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
221 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
222 model = simplifier.getSimplifiedModel();
223
224 // Create the region
225 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
226 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
227
228 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
229 auto order = std::get<0>(extender.toOrder(region));
230 EXPECT_EQ(5ul, order->getNumberOfAddedStates());
231 EXPECT_TRUE(order->getDoneBuilding());
232
233 // Check on all states
234 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
235 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
236 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
237 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
238 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
239 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
240 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
241 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
242 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
243 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
244}
245
246TEST_F(OrderExtenderTest, simple1_on_matrix) {
247 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
248 std::string formulaAsString = "P=? [F s=3 ]";
249 std::string constantsAsString = "";
250
251 // model
252 storm::prism::Program program = storm::api::parseProgram(programFile);
253 program = program.preprocess(constantsAsString);
254 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
255 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
256 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
257 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
258 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
259 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
260 model = simplifier.getSimplifiedModel();
261
262 // Create the region
263 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
264 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.9", modelParameters);
265
266 // For order extender
267 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
268 storm::storage::BitVector phiStates;
269 storm::storage::BitVector psiStates;
270 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
271 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
272 psiStates =
273 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
274 // Get the maybeStates
275 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
276 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
277 storm::storage::BitVector topStates = statesWithProbability01.second;
278 storm::storage::BitVector bottomStates = statesWithProbability01.first;
279
280 // OrderExtender
281 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
282 auto res = extender.extendOrder(nullptr, region);
283 auto order = std::get<0>(res);
284 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
285 EXPECT_TRUE(order->getDoneBuilding());
286
287 // Check on all states, as this one automatically handles assumptions (if there is one valid) all are ABOVE
288 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
289 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
290 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
291 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
292 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
293 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
294 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
295 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
296 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
297 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
298}
299
300TEST_F(OrderExtenderTest, casestudy1_on_model) {
301 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
302 std::string formulaAsString = "P=? [F s=3 ]";
303 std::string constantsAsString = "";
304
305 // model
306 storm::prism::Program program = storm::api::parseProgram(programFile);
307 program = program.preprocess(constantsAsString);
308 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
309 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
310 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
311 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
312 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
313 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
314 model = simplifier.getSimplifiedModel();
315
316 // Create the region
317 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
318 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
319
320 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
321 auto order = std::get<0>(extender.toOrder(region));
322
323 EXPECT_EQ(5ul, order->getNumberOfAddedStates());
324 EXPECT_TRUE(order->getDoneBuilding());
325 // Check on all states
326 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
327 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
328 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
329 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
330 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
331 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
332 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
333 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
334 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
335 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
336}
337
338TEST_F(OrderExtenderTest, casestudy1_on_matrix) {
339 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
340 std::string formulaAsString = "P=? [F s=3 ]";
341 std::string constantsAsString = "";
342
343 // model
344 storm::prism::Program program = storm::api::parseProgram(programFile);
345 program = program.preprocess(constantsAsString);
346 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
347 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
348 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
349 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
350 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
351 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
352 model = simplifier.getSimplifiedModel();
353
354 // Create the region
355 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
356 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.9", modelParameters);
357
358 // For order extender
359 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
360 storm::storage::BitVector phiStates;
361 storm::storage::BitVector psiStates;
362 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
363 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
364 psiStates =
365 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
366 // Get the maybeStates
367 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
368 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
369 storm::storage::BitVector topStates = statesWithProbability01.second;
370 storm::storage::BitVector bottomStates = statesWithProbability01.first;
371
372 // OrderExtender
373 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
374 auto res = extender.extendOrder(nullptr, region);
375 auto order = std::get<0>(res);
376 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
377 EXPECT_TRUE(order->getDoneBuilding());
378
379 // Check on all states
380 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
381 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
382 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
383 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
384 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
385 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
386 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
387 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
388 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
389 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
390}
391
392TEST_F(OrderExtenderTest, casestudy2_on_matrix) {
393 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
394 std::string formulaAsString = "P=? [F s=4 ]";
395 std::string constantsAsString = "";
396
397 // model
398 storm::prism::Program program = storm::api::parseProgram(programFile);
399 program = program.preprocess(constantsAsString);
400 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
401 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
402 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
403 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
404 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
405 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
406 model = simplifier.getSimplifiedModel();
407
408 // Create the region
409 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
410 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1 <= p <= 0.2", modelParameters);
411
412 // For order extender
413 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
414 storm::storage::BitVector phiStates;
415 storm::storage::BitVector psiStates;
416 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
417 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
418 psiStates =
419 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
420 // Get the maybeStates
421 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
422 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
423 storm::storage::BitVector topStates = statesWithProbability01.second;
424 storm::storage::BitVector bottomStates = statesWithProbability01.first;
425
426 // OrderExtender
427 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
428 auto res = extender.extendOrder(nullptr, region);
429 EXPECT_TRUE(std::get<0>(res)->getDoneBuilding());
430}
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:22
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::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::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::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::storage::BisimulationType type=storm::storage::BisimulationType::Strong, bool graphPreserving=true, std::optional< double > const &tolerance=std::nullopt)
Definition bisimulation.h:80
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