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