Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
OrderExtenderTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2
3#include <memory>
4#include <vector>
5#include "storm-pars/api/storm-pars.h"
6#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
7
8#include "storm-parsers/api/storm-parsers.h"
9#include "storm-parsers/parser/AutoParser.h"
10#include "storm-parsers/parser/PrismParser.h"
11
12#include "storm/api/builder.h"
13#include "storm/api/storm.h"
14#include "storm/logic/Formulas.h"
15#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
16#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
17#include "storm/models/sparse/StandardRewardModel.h"
18#include "storm/utility/graph.h"
19
20#include "test/storm_gtest.h"
21
22class OrderExtenderTest : public ::testing::Test {
23 protected:
24 void SetUp() override {
25#ifndef STORM_HAVE_Z3
26 GTEST_SKIP() << "Z3 not available.";
27#endif
28 }
29};
30
31TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_model) {
32 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
33 std::string formulaAsString = "P=? [F s=4 & i=N ]";
34 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
35
36 // Program and formula
37 storm::prism::Program program = storm::api::parseProgram(programFile);
38 program = storm::utility::prism::preprocess(program, constantsAsString);
39 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
40 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
41 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
42 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
43 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
44 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
45 model = simplifier.getSimplifiedModel();
46
47 // Apply bisimulation
48 storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
49 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
50 bisimType = storm::storage::BisimulationType::Weak;
51 }
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 = storm::utility::prism::preprocess(program, 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 = storm::utility::prism::preprocess(program, 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 if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
133 bisimType = storm::storage::BisimulationType::Weak;
134 }
135
136 model = storm::api::performBisimulationMinimization<storm::RationalFunction>(model, formulas, bisimType)
137 ->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
138
139 ASSERT_EQ(99ul, model->getNumberOfStates());
140 ASSERT_EQ(195ul, model->getNumberOfTransitions());
141
142 auto vars = storm::models::sparse::getProbabilityParameters(*model);
143 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
144 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
145 storm::storage::BitVector phiStates;
146 storm::storage::BitVector psiStates;
147 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
148 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
149 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
150 // Get the maybeStates
151 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
152 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
153 storm::storage::BitVector topStates = statesWithProbability01.second;
154 storm::storage::BitVector bottomStates = statesWithProbability01.first;
155
156 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(&topStates, &bottomStates, model->getTransitionMatrix());
157 auto res = extender.extendOrder(nullptr, region);
158 auto order = std::get<0>(res);
159 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
160 EXPECT_TRUE(order->getDoneBuilding());
161
162 // Check on some nodes
163 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
164 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 5));
165 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5, 0));
166 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94, 5));
167 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7, 13));
168}
169
170TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) {
171 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
172 std::string formulaAsString = "P=? [F s=4 & i=N ]";
173 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
174
175 // Program and formula
176 storm::prism::Program program = storm::api::parseProgram(programFile);
177 program = storm::utility::prism::preprocess(program, constantsAsString);
178 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
179 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
180 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
181 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
182 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
183 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
184 model = simplifier.getSimplifiedModel();
185
186 ASSERT_EQ(193ul, model->getNumberOfStates());
187 ASSERT_EQ(383ul, model->getNumberOfTransitions());
188
189 auto vars = storm::models::sparse::getProbabilityParameters(*model);
190 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
191 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
192 storm::storage::BitVector phiStates;
193 storm::storage::BitVector psiStates;
194 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
195 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
196 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
197 // Get the maybeStates
198 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
199 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
200 storm::storage::BitVector topStates = statesWithProbability01.second;
201 storm::storage::BitVector bottomStates = statesWithProbability01.first;
202
203 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(&topStates, &bottomStates, model->getTransitionMatrix());
204 auto res = extender.extendOrder(nullptr, region);
205 auto order = std::get<0>(res);
206 EXPECT_FALSE(order->getDoneBuilding());
207}
208
209TEST_F(OrderExtenderTest, simple1_on_model) {
210 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
211 std::string formulaAsString = "P=? [F s=3 ]";
212 std::string constantsAsString = "";
213
214 // model
215 storm::prism::Program program = storm::api::parseProgram(programFile);
216 program = storm::utility::prism::preprocess(program, constantsAsString);
217 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
218 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
219 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
220 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
221 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
222 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
223 model = simplifier.getSimplifiedModel();
224
225 // Create the region
226 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
227 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
228
229 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
230 auto order = std::get<0>(extender.toOrder(region));
231 EXPECT_EQ(5ul, order->getNumberOfAddedStates());
232 EXPECT_TRUE(order->getDoneBuilding());
233
234 // Check on all states
235 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
236 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
237 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
238 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
239 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
240 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
241 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
242 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
243 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
244 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
245}
246
247TEST_F(OrderExtenderTest, simple1_on_matrix) {
248 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
249 std::string formulaAsString = "P=? [F s=3 ]";
250 std::string constantsAsString = "";
251
252 // model
253 storm::prism::Program program = storm::api::parseProgram(programFile);
254 program = storm::utility::prism::preprocess(program, constantsAsString);
255 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
256 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
257 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
258 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
259 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
260 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
261 model = simplifier.getSimplifiedModel();
262
263 // Create the region
264 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
265 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.9", modelParameters);
266
267 // For order extender
268 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
269 storm::storage::BitVector phiStates;
270 storm::storage::BitVector psiStates;
271 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
272 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
273 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().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 = storm::utility::prism::preprocess(program, 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 = storm::utility::prism::preprocess(program, 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 = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
365 // Get the maybeStates
366 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
367 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
368 storm::storage::BitVector topStates = statesWithProbability01.second;
369 storm::storage::BitVector bottomStates = statesWithProbability01.first;
370
371 // OrderExtender
372 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(&topStates, &bottomStates, model->getTransitionMatrix());
373 auto res = extender.extendOrder(nullptr, region);
374 auto order = std::get<0>(res);
375 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
376 EXPECT_TRUE(order->getDoneBuilding());
377
378 // Check on all states
379 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
380 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
381 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
382 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
383 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
384 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
385 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
386 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
387 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
388 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
389}
390
391TEST_F(OrderExtenderTest, casestudy2_on_matrix) {
392 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
393 std::string formulaAsString = "P=? [F s=4 ]";
394 std::string constantsAsString = "";
395
396 // model
397 storm::prism::Program program = storm::api::parseProgram(programFile);
398 program = storm::utility::prism::preprocess(program, constantsAsString);
399 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
400 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
401 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
402 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
403 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
404 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
405 model = simplifier.getSimplifiedModel();
406
407 // Create the region
408 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
409 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1 <= p <= 0.2", modelParameters);
410
411 // For order extender
412 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
413 storm::storage::BitVector phiStates;
414 storm::storage::BitVector psiStates;
415 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
416 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
417 psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
418 // Get the maybeStates
419 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
420 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
421 storm::storage::BitVector topStates = statesWithProbability01.second;
422 storm::storage::BitVector bottomStates = statesWithProbability01.first;
423
424 // OrderExtender
425 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(&topStates, &bottomStates, model->getTransitionMatrix());
426 auto res = extender.extendOrder(nullptr, region);
427 EXPECT_TRUE(std::get<0>(res)->getDoneBuilding());
428}
TEST_F
TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_model)
Definition OrderExtenderTest.cpp:31
OrderExtenderTest::SetUp
void SetUp() override
Definition OrderExtenderTest.cpp:24
storm::analysis::OrderExtender::VariableType
utility::parametric::VariableType< ValueType >::type VariableType
Definition OrderExtender.h:23
storm::logic::Formula::asProbabilityOperatorFormula
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:453
storm::logic::Formula::asEventuallyFormula
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:333
storm::logic::UnaryPathFormula::getSubformula
Formula const & getSubformula() const
Definition UnaryPathFormula.cpp:13
storm::logic::UnaryStateFormula::getSubformula
Formula const & getSubformula() const
Definition UnaryStateFormula.cpp:15
storm::modelchecker::AbstractModelChecker::check
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Definition AbstractModelChecker.cpp:51
storm::models::ModelBase::as
std::shared_ptr< ModelType > as()
Casts the model into the model type given by the template parameter.
Definition ModelBase.h:36
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
storm::transformer::SparseParametricDtmcSimplifier
This class performs different steps to simplify the given (parametric) model.
Definition SparseParametricDtmcSimplifier.h:15
storm::api::parsePropertiesForPrismProgram
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:69
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:703
storm::settings::getModule
SettingsType const & getModule()
Get module.
Definition SettingsManager.h:290
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:400
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:19
storm_gtest.h