Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
AssumptionCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/api/region.h"
5#include "storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h"
6#include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h"
7#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h"
8#include "storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h"
9#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h"
10#include "storm-pars/modelchecker/region/monotonicity/Order.h"
11#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h"
12#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
13#include "storm-parsers/api/model_descriptions.h"
14#include "storm-parsers/api/properties.h"
15#include "storm-parsers/parser/AutoParser.h"
16#include "storm-parsers/parser/PrismParser.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/storage/StronglyConnectedComponentDecomposition.h"
22#include "storm/storage/expressions/BinaryRelationExpression.h"
23#include "storm/storage/expressions/ExpressionManager.h"
24#include "storm/utility/graph.h"
25
26class AssumptionCheckerTest : public ::testing::Test {
27 protected:
28 void SetUp() override {
29#ifndef STORM_HAVE_Z3
30 GTEST_SKIP() << "Z3 not available.";
31#endif
32 }
33};
34
35TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) {
36 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
37 std::string formulaAsString = "P=? [F s=4 & i=N ]";
38 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
39
40 // Program and formula
41 storm::prism::Program program = storm::api::parseProgram(programFile);
42 program = program.preprocess(constantsAsString);
43 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
44 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
45 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
46 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
47 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
48 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
49 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
50 model = simplifier.getSimplifiedModel();
51
52 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
53
54 ASSERT_EQ(193ul, dtmc->getNumberOfStates());
55 ASSERT_EQ(383ul, dtmc->getNumberOfTransitions());
56
57 // Create the region
58 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
59 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.00001, 0.00001 <= pL <= 0.99999", vars);
60
61 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
62 auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
63 expressionManager->declareRationalVariable("7");
64 expressionManager->declareRationalVariable("5");
65 storm::storage::BitVector above(193);
66 above.set(0);
67 storm::storage::BitVector below(193);
68 below.set(1);
69
70 storm::storage::StronglyConnectedComponentDecompositionOptions options;
71 options.forceTopologicalSort();
72 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
73
74 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
75 auto dummyOrder = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 193, decomposition, statesSorted));
76
77 auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
78 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
79 expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
80 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
81
82 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
83 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(),
84 expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
85 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
86
87 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
88 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
89 expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
90 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
91
92 checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3);
93 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
94 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
95 expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
96 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
97
98 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
99 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(),
100 expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
101 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region));
102
103 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
104 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
105 expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
106 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region));
107}
108
109TEST_F(AssumptionCheckerTest, Simple1) {
110 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
111 std::string formulaAsString = "P=? [F s=3]";
112 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
113
114 // Program and formula
115 storm::prism::Program program = storm::api::parseProgram(programFile);
116 program = program.preprocess(constantsAsString);
117 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
118 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
119 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
120 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
121 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
122 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
123 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
124 model = simplifier.getSimplifiedModel();
125 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
126
127 ASSERT_EQ(5ul, dtmc->getNumberOfStates());
128 ASSERT_EQ(8ul, dtmc->getNumberOfTransitions());
129
130 // Create the region
131 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
132 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars);
133
134 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
135
136 auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
137 expressionManager->declareRationalVariable("1");
138 expressionManager->declareRationalVariable("2");
139 storm::storage::StronglyConnectedComponentDecompositionOptions options;
140 options.forceTopologicalSort();
141 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
142
143 storm::storage::BitVector above(5);
144 above.set(3);
145 storm::storage::BitVector below(5);
146 below.set(4);
147 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
148 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
149
150 // Validating
151 auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
152 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
153 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
154 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
155
156 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
157 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
158 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
159 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
160
161 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
162 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
163 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
164 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
165
166 region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.99", vars);
167 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
168 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
169 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
170 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
171
172 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
173 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
174 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
175 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
176
177 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
178 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
179 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
180 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
181}
182
183TEST_F(AssumptionCheckerTest, Casestudy1) {
184 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
185 std::string formulaAsString = "P=? [F s=3]";
186 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
187
188 // Program and formula
189 storm::prism::Program program = storm::api::parseProgram(programFile);
190 program = program.preprocess(constantsAsString);
191 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
192 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
193 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
194 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
195 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
196 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
197 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
198 model = simplifier.getSimplifiedModel();
199 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
200
201 ASSERT_EQ(5ul, dtmc->getNumberOfStates());
202 ASSERT_EQ(8ul, dtmc->getNumberOfTransitions());
203
204 // Create the region
205 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
206 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars);
207
208 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
209
210 auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
211 expressionManager->declareRationalVariable("1");
212 expressionManager->declareRationalVariable("2");
213
214 storm::storage::BitVector above(5);
215 above.set(3);
216 storm::storage::BitVector below(5);
217 below.set(4);
218
219 storm::storage::StronglyConnectedComponentDecompositionOptions options;
220 options.forceTopologicalSort();
221 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
222 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
223 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
224
225 // Validating
226 auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
227 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
228 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
229 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
230
231 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
232 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
233 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
234 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
235
236 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
237 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
238 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
239 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
240
241 checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3);
242 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
243 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
244 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
245 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
246
247 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
248 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
249 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
250 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
251
252 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
253 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
254 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
255 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
256}
257
258TEST_F(AssumptionCheckerTest, Casestudy2) {
259 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
260 std::string formulaAsString = "P=? [F s=4]";
261 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
262
263 // Program and formula
264 storm::prism::Program program = storm::api::parseProgram(programFile);
265 program = program.preprocess(constantsAsString);
266 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
267 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
268 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
269 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
270 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
271 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
272 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
273 model = simplifier.getSimplifiedModel();
274 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
275
276 ASSERT_EQ(6ul, dtmc->getNumberOfStates());
277 ASSERT_EQ(12ul, dtmc->getNumberOfTransitions());
278
279 // Create the region
280 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
281 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars);
282
283 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
284
285 auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
286 expressionManager->declareRationalVariable("1");
287 expressionManager->declareRationalVariable("2");
288
289 storm::storage::BitVector above(6);
290 above.set(4);
291 storm::storage::BitVector below(6);
292 below.set(5);
293
294 storm::storage::StronglyConnectedComponentDecompositionOptions options;
295 options.forceTopologicalSort();
296 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
297 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
298 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 6, decomposition, statesSorted));
299 order->add(3);
300
301 // Checking on samples and validate
302 auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
303 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
304 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
305 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
306
307 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
308 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
309 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
310 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
311
312 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
313 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
314 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
315 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
316}
317
318TEST_F(AssumptionCheckerTest, Casestudy3) {
319 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
320 std::string formulaAsString = "P=? [F s=3]";
321 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
322
323 // Program and formula
324 storm::prism::Program program = storm::api::parseProgram(programFile);
325 program = program.preprocess(constantsAsString);
326 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
327 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
328 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
329 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
330 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
331 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
332 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
333 model = simplifier.getSimplifiedModel();
334 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
335
336 ASSERT_EQ(5ul, dtmc->getNumberOfStates());
337 ASSERT_EQ(8ul, dtmc->getNumberOfTransitions());
338
339 // Create the region
340 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
341 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.4", vars);
342
343 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
344
345 auto expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
346 expressionManager->declareRationalVariable("1");
347 expressionManager->declareRationalVariable("2");
348
349 // Order
350 storm::storage::BitVector above(5);
351 above.set(3);
352 storm::storage::BitVector below(5);
353 below.set(4);
354 storm::storage::StronglyConnectedComponentDecompositionOptions options;
355 options.forceTopologicalSort();
356 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
357 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
358 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
359
360 auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
361 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
362 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
363 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
364
365 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
366 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
367 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
368 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
369
370 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
371 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
372 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
373 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
374
375 checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3);
376
377 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
378 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
379 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
380 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
381
382 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
383 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(),
384 expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater));
385 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
386
387 assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(
388 *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),
389 expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal));
390 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
391}
TEST_F
TEST_F(AssumptionCheckerTest, Brp_no_bisimulation)
Definition AssumptionCheckerTest.cpp:35
storm::expressions::ExpressionManager
This class is responsible for managing a set of typed variables and all expressions using these varia...
Definition ExpressionManager.h:71
storm::models::ModelBase::as
std::shared_ptr< ModelType > as()
Casts the model into the model type given by the template parameter.
Definition ModelBase.h:38
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::sparse::Model::getTransitionMatrix
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:198
storm::models::sparse::Model::getNumberOfTransitions
virtual uint_fast64_t getNumberOfTransitions() const override
Returns the number of (non-zero) transitions of the model.
Definition Model.cpp:168
storm::models::sparse::Model::getNumberOfStates
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:163
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::storage::BitVector::set
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
Definition BitVector.cpp:244
storm::storage::StronglyConnectedComponentDecomposition
This class represents the decomposition of a graph-like structure into its strongly connected compone...
Definition StronglyConnectedComponentDecomposition.h:100
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::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::getTopologicalSort
std::vector< uint_fast64_t > getTopologicalSort(storm::storage::SparseMatrix< T > const &matrix, std::vector< uint64_t > const &firstStates)
Performs a topological sort of the states of the system according to the given transitions.
Definition graph.cpp:1845
storm_gtest.h
storm::storage::StronglyConnectedComponentDecompositionOptions::forceTopologicalSort
StronglyConnectedComponentDecompositionOptions & forceTopologicalSort(bool value=true)
Enforces that the returned SCCs are sorted in a topological order.
Definition StronglyConnectedComponentDecomposition.cpp:33