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