Storm 1.13.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/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 =
148 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
149 // Get the maybeStates
150 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
151 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
152 storm::storage::BitVector topStates = statesWithProbability01.second;
153 storm::storage::BitVector bottomStates = statesWithProbability01.first;
154
155 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
156 auto res = extender.extendOrder(nullptr, region);
157 auto order = std::get<0>(res);
158 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
159 EXPECT_TRUE(order->getDoneBuilding());
160
161 // Check on some nodes
162 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
163 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 5));
164 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5, 0));
165 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94, 5));
166 EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7, 13));
167}
168
169TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) {
170 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
171 std::string formulaAsString = "P=? [F s=4 & i=N ]";
172 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
173
174 // Program and formula
175 storm::prism::Program program = storm::api::parseProgram(programFile);
176 program = storm::utility::prism::preprocess(program, constantsAsString);
177 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
178 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
179 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
180 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
181 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
182 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
183 model = simplifier.getSimplifiedModel();
184
185 ASSERT_EQ(193ul, model->getNumberOfStates());
186 ASSERT_EQ(383ul, model->getNumberOfTransitions());
187
188 auto vars = storm::models::sparse::getProbabilityParameters(*model);
189 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
190 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
191 storm::storage::BitVector phiStates;
192 storm::storage::BitVector psiStates;
193 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
194 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
195 psiStates =
196 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().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 =
274 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
275 // Get the maybeStates
276 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
277 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
278 storm::storage::BitVector topStates = statesWithProbability01.second;
279 storm::storage::BitVector bottomStates = statesWithProbability01.first;
280
281 // OrderExtender
282 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
283 auto res = extender.extendOrder(nullptr, region);
284 auto order = std::get<0>(res);
285 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
286 EXPECT_TRUE(order->getDoneBuilding());
287
288 // Check on all states, as this one automatically handles assumptions (if there is one valid) all are ABOVE
289 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
290 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
291 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
292 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
293 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
294 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
295 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
296 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
297 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
298 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
299}
300
301TEST_F(OrderExtenderTest, casestudy1_on_model) {
302 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
303 std::string formulaAsString = "P=? [F s=3 ]";
304 std::string constantsAsString = "";
305
306 // model
307 storm::prism::Program program = storm::api::parseProgram(programFile);
308 program = storm::utility::prism::preprocess(program, constantsAsString);
309 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
310 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
311 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
312 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
313 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
314 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
315 model = simplifier.getSimplifiedModel();
316
317 // Create the region
318 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
319 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51<=p<=0.9", modelParameters);
320
321 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
322 auto order = std::get<0>(extender.toOrder(region));
323
324 EXPECT_EQ(5ul, order->getNumberOfAddedStates());
325 EXPECT_TRUE(order->getDoneBuilding());
326 // Check on all states
327 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
328 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
329 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
330 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
331 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
332 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
333 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
334 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
335 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
336 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
337}
338
339TEST_F(OrderExtenderTest, casestudy1_on_matrix) {
340 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
341 std::string formulaAsString = "P=? [F s=3 ]";
342 std::string constantsAsString = "";
343
344 // model
345 storm::prism::Program program = storm::api::parseProgram(programFile);
346 program = storm::utility::prism::preprocess(program, constantsAsString);
347 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
348 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
349 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
350 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
351 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
352 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
353 model = simplifier.getSimplifiedModel();
354
355 // Create the region
356 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
357 auto region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.9", modelParameters);
358
359 // For order extender
360 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
361 storm::storage::BitVector phiStates;
362 storm::storage::BitVector psiStates;
363 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
364 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
365 psiStates =
366 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
367 // Get the maybeStates
368 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
369 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
370 storm::storage::BitVector topStates = statesWithProbability01.second;
371 storm::storage::BitVector bottomStates = statesWithProbability01.first;
372
373 // OrderExtender
374 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
375 auto res = extender.extendOrder(nullptr, region);
376 auto order = std::get<0>(res);
377 EXPECT_EQ(order->getNumberOfAddedStates(), model->getNumberOfStates());
378 EXPECT_TRUE(order->getDoneBuilding());
379
380 // Check on all states
381 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 0));
382 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 1));
383 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 2));
384 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(3, 4));
385 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 0));
386 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 2));
387 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1, 4));
388 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 2));
389 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(0, 4));
390 EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(2, 4));
391}
392
393TEST_F(OrderExtenderTest, casestudy2_on_matrix) {
394 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
395 std::string formulaAsString = "P=? [F s=4 ]";
396 std::string constantsAsString = "";
397
398 // model
399 storm::prism::Program program = storm::api::parseProgram(programFile);
400 program = storm::utility::prism::preprocess(program, constantsAsString);
401 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
402 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
403 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
404 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
405 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
406 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
407 model = simplifier.getSimplifiedModel();
408
409 // Create the region
410 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
411 auto region = storm::api::parseRegion<storm::RationalFunction>("0.1 <= p <= 0.2", modelParameters);
412
413 // For order extender
414 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>> propositionalChecker(*model);
415 storm::storage::BitVector phiStates;
416 storm::storage::BitVector psiStates;
417 phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true);
418 storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula();
419 psiStates =
420 propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult<storm::RationalFunction>().getTruthValuesVector();
421 // Get the maybeStates
422 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
423 storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates);
424 storm::storage::BitVector topStates = statesWithProbability01.second;
425 storm::storage::BitVector bottomStates = statesWithProbability01.first;
426
427 // OrderExtender
428 auto extender = storm::analysis::OrderExtender<storm::RationalFunction, double>(topStates, bottomStates, model->getTransitionMatrix());
429 auto res = extender.extendOrder(nullptr, region);
430 EXPECT_TRUE(std::get<0>(res)->getDoneBuilding());
431}
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:49
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::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)
Definition builder.h:109
storm::api::parseRegion
storm::storage::ParameterRegion< ValueType > parseRegion(std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)
Definition region.h:136
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::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)
Definition bisimulation.h:61
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:694
storm::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:393
storm::utility::prism::preprocess
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
Definition prism.cpp:13
storm_gtest.h