Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
AssumptionMakerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h"
5#include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h"
6#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h"
7#include "storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h"
8#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h"
9#include "storm-pars/modelchecker/region/monotonicity/Order.h"
10#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h"
11#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
12#include "storm-parsers/api/storm-parsers.h"
13#include "storm-parsers/parser/AutoParser.h"
14#include "storm-parsers/parser/PrismParser.h"
15#include "storm/api/builder.h"
16#include "storm/api/storm.h"
17#include "storm/logic/Formulas.h"
18#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
19#include "storm/models/sparse/StandardRewardModel.h"
20#include "storm/storage/StronglyConnectedComponentDecomposition.h"
21#include "storm/utility/graph.h"
22
23class AssumptionMakerTest : public ::testing::Test {
24 protected:
25 void SetUp() override {
26#ifndef STORM_HAVE_Z3
27 GTEST_SKIP() << "Z3 not available.";
28#endif
29 }
30};
31
32TEST_F(AssumptionMakerTest, Brp_without_bisimulation) {
33 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
34 std::string formulaAsString = "P=? [F s=4 & i=N ]";
35 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
36
37 // Program and formula
38 storm::prism::Program program = storm::api::parseProgram(programFile);
39 program = storm::utility::prism::preprocess(program, constantsAsString);
40 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
41 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
42 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
43 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
44 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
45 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
46 model = simplifier.getSimplifiedModel();
47 model = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
48
49 // Create the region
50 auto vars = storm::models::sparse::getProbabilityParameters(*model);
51 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
52
53 ASSERT_EQ(193ul, model->getNumberOfStates());
54 ASSERT_EQ(383ul, model->getNumberOfTransitions());
55
56 auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
57 auto criticalTuple = extender->toOrder(region, nullptr);
58 ASSERT_EQ(183ul, std::get<1>(criticalTuple));
59 ASSERT_EQ(186ul, std::get<2>(criticalTuple));
60
61 auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction, double>(model->getTransitionMatrix());
62 auto result = assumptionMaker.createAndCheckAssumptions(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple), region);
63
64 EXPECT_EQ(3ul, result.size());
65
66 for (auto res : result) {
67 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, res.second);
68 EXPECT_EQ(true, res.first->getFirstOperand()->isVariable());
69 EXPECT_EQ(true, res.first->getSecondOperand()->isVariable());
70 }
71
72 assumptionMaker.initializeCheckingOnSamples(formulas[0], model, region, 10);
73 result = assumptionMaker.createAndCheckAssumptions(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple), region);
74 EXPECT_EQ(1ul, result.size());
75 auto itr = result.begin();
76 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second);
77 EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
78 EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
79 EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName());
80 EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName());
81 EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType());
82}
83
84TEST_F(AssumptionMakerTest, Simple1) {
85 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
86 std::string formulaAsString = "P=? [F s=3 ]";
87 std::string constantsAsString = "";
88
89 storm::prism::Program program = storm::api::parseProgram(programFile);
90 program = storm::utility::prism::preprocess(program, constantsAsString);
91 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
92 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
93 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
94 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
95 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
96 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
97 model = simplifier.getSimplifiedModel();
98
99 // Create the region
100 auto vars = storm::models::sparse::getProbabilityParameters(*model);
101 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.999999", vars);
102
103 ASSERT_EQ(5ul, model->getNumberOfStates());
104 ASSERT_EQ(8ul, model->getNumberOfTransitions());
105
106 storm::storage::BitVector above(5);
107 above.set(3);
108 storm::storage::BitVector below(5);
109 below.set(4);
110 storm::storage::StronglyConnectedComponentDecompositionOptions options;
111 options.forceTopologicalSort();
112 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
113 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
114 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
115
116 auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction, double>(model->getTransitionMatrix());
117 auto result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
118 EXPECT_EQ(0ul, result.size());
119 assumptionMaker.initializeCheckingOnSamples(formulas[0], model, region, 10);
120 result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
121 EXPECT_EQ(0ul, result.size());
122
123 region = storm::api::parseRegion<storm::RationalFunction>("0.500001 <= p <= 0.999999", vars);
124 std::vector<std::vector<double>> samples;
125 assumptionMaker.setSampleValues(samples);
126 result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
127 EXPECT_EQ(1ul, result.size());
128 auto itr = result.begin();
129 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second);
130 EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
131 EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
132 EXPECT_EQ("1", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName());
133 EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName());
134 EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType());
135}
136
137TEST_F(AssumptionMakerTest, Casestudy1) {
138 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
139 std::string formulaAsString = "P=? [F s=3 ]";
140 std::string constantsAsString = "";
141
142 storm::prism::Program program = storm::api::parseProgram(programFile);
143 program = storm::utility::prism::preprocess(program, constantsAsString);
144 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
145 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
146 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
147 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
148 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
149 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
150 model = simplifier.getSimplifiedModel();
151 model = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
152 // Create the region
153 auto vars = storm::models::sparse::getProbabilityParameters(*model);
154 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.999999", vars);
155
156 ASSERT_EQ(5ul, model->getNumberOfStates());
157 ASSERT_EQ(8ul, model->getNumberOfTransitions());
158
159 storm::storage::BitVector above(5);
160 above.set(3);
161 storm::storage::BitVector below(5);
162 below.set(4);
163
164 storm::storage::StronglyConnectedComponentDecompositionOptions options;
165 options.forceTopologicalSort();
166 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
167 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
168 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
169
170 auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction, double>(model->getTransitionMatrix());
171 auto result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
172
173 EXPECT_EQ(1ul, result.size());
174 auto itr = result.begin();
175 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second);
176 EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
177 EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
178 EXPECT_EQ("1", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName());
179 EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName());
180 EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType());
181}
TEST_F
TEST_F(AssumptionMakerTest, Brp_without_bisimulation)
Definition AssumptionMakerTest.cpp:32
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::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