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