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