Storm 1.14.0.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/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/SparseParametricModelSimplifier.h"
13#include "storm-parsers/api/model_descriptions.h"
14#include "storm-parsers/api/properties.h"
15#include "storm-parsers/parser/AutoParser.h"
16#include "storm-parsers/parser/PrismParser.h"
17#include "storm/api/builder.h"
18#include "storm/api/properties.h"
19#include "storm/environment/Environment.h"
20#include "storm/logic/Formulas.h"
21#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
22#include "storm/models/sparse/StandardRewardModel.h"
23#include "storm/storage/StronglyConnectedComponentDecomposition.h"
24#include "storm/utility/graph.h"
25
26class AssumptionMakerTest : public ::testing::Test {
27 protected:
28 void SetUp() override {
29#ifndef STORM_HAVE_Z3
30 GTEST_SKIP() << "Z3 not available.";
31#endif
32 }
33};
34
35TEST_F(AssumptionMakerTest, Brp_without_bisimulation) {
36 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
37 std::string formulaAsString = "P=? [F s=4 & i=N ]";
38 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
39
40 // Program and formula
41 storm::prism::Program program = storm::api::parseProgram(programFile);
42 program = program.preprocess(constantsAsString);
43 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
44 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
45 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
46 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
47 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
48 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
49 model = simplifier.getSimplifiedModel();
50 model = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
51
52 // Create the region
53 auto vars = storm::models::sparse::getProbabilityParameters(*model);
54 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= pK <= 0.999999, 0.00001 <= pL <= 0.999999", vars);
55
56 ASSERT_EQ(193ul, model->getNumberOfStates());
57 ASSERT_EQ(383ul, model->getNumberOfTransitions());
58
59 auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction, double>(model, formulas[0]);
60 auto criticalTuple = extender->toOrder(region, nullptr);
61 ASSERT_EQ(183ul, std::get<1>(criticalTuple));
62 ASSERT_EQ(186ul, std::get<2>(criticalTuple));
63
64 auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction, double>(model->getTransitionMatrix());
65 auto result = assumptionMaker.createAndCheckAssumptions(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple), region);
66
67 // The candidate count is a prerequisite for the indexed accesses below, so fail hard here
68 // rather than continuing into unchecked operator[] calls.
69 ASSERT_EQ(3ul, result.size());
70
71 for (auto res : result) {
72 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, res.second);
73 }
74
75 // Regression test: when more than one candidate survives, they must be returned in construction
76 // order (val1 > val2, val2 > val1, val1 == val2), not e.g. heap-address order of some internal
77 // representation.
78 EXPECT_EQ(183ul, result[0].first.state1);
79 EXPECT_EQ(186ul, result[0].first.state2);
80 EXPECT_EQ(storm::analysis::AssumptionRelation::Greater, result[0].first.relation);
81 EXPECT_EQ(186ul, result[1].first.state1);
82 EXPECT_EQ(183ul, result[1].first.state2);
83 EXPECT_EQ(storm::analysis::AssumptionRelation::Greater, result[1].first.relation);
84 EXPECT_EQ(183ul, result[2].first.state1);
85 EXPECT_EQ(186ul, result[2].first.state2);
86 EXPECT_EQ(storm::analysis::AssumptionRelation::Equal, result[2].first.relation);
87
88 assumptionMaker.initializeCheckingOnSamples(storm::Environment(), formulas[0], model, region, 10);
89 result = assumptionMaker.createAndCheckAssumptions(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple), region);
90 EXPECT_EQ(1ul, result.size());
91 auto itr = result.begin();
92 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second);
93 EXPECT_EQ(186ul, itr->first.state1);
94 EXPECT_EQ(183ul, itr->first.state2);
95 EXPECT_EQ(storm::analysis::AssumptionRelation::Greater, itr->first.relation);
96}
97
98TEST_F(AssumptionMakerTest, Simple1) {
99 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
100 std::string formulaAsString = "P=? [F s=3 ]";
101 std::string constantsAsString = "";
102
103 storm::prism::Program program = storm::api::parseProgram(programFile);
104 program = program.preprocess(constantsAsString);
105 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
106 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
107 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
108 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
109 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
110 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
111 model = simplifier.getSimplifiedModel();
112
113 // Create the region
114 auto vars = storm::models::sparse::getProbabilityParameters(*model);
115 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.999999", vars);
116
117 ASSERT_EQ(5ul, model->getNumberOfStates());
118 ASSERT_EQ(8ul, model->getNumberOfTransitions());
119
120 storm::storage::BitVector above(5);
121 above.set(3);
122 storm::storage::BitVector below(5);
123 below.set(4);
124 storm::storage::StronglyConnectedComponentDecompositionOptions options;
125 options.forceTopologicalSort();
126 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
127 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
128 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
129
130 auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction, double>(model->getTransitionMatrix());
131 auto result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
132 EXPECT_EQ(0ul, result.size());
133 assumptionMaker.initializeCheckingOnSamples(storm::Environment(), formulas[0], model, region, 10);
134 result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
135 EXPECT_EQ(0ul, result.size());
136
137 region = storm::api::parseRegion<storm::RationalFunction>("0.500001 <= p <= 0.999999", vars);
138 std::vector<std::vector<double>> samples;
139 assumptionMaker.setSampleValues(samples);
140 result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
141 EXPECT_EQ(1ul, result.size());
142 auto itr = result.begin();
143 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second);
144 EXPECT_EQ(1ul, itr->first.state1);
145 EXPECT_EQ(2ul, itr->first.state2);
146 EXPECT_EQ(storm::analysis::AssumptionRelation::Greater, itr->first.relation);
147}
148
149TEST_F(AssumptionMakerTest, Casestudy1) {
150 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
151 std::string formulaAsString = "P=? [F s=3 ]";
152 std::string constantsAsString = "";
153
154 storm::prism::Program program = storm::api::parseProgram(programFile);
155 program = program.preprocess(constantsAsString);
156 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
157 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
158 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
159 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
160 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*model);
161 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
162 model = simplifier.getSimplifiedModel();
163 model = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
164 // Create the region
165 auto vars = storm::models::sparse::getProbabilityParameters(*model);
166 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.999999", vars);
167
168 ASSERT_EQ(5ul, model->getNumberOfStates());
169 ASSERT_EQ(8ul, model->getNumberOfTransitions());
170
171 storm::storage::BitVector above(5);
172 above.set(3);
173 storm::storage::BitVector below(5);
174 below.set(4);
175
176 storm::storage::StronglyConnectedComponentDecompositionOptions options;
177 options.forceTopologicalSort();
178 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
179 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
180 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
181
182 auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction, double>(model->getTransitionMatrix());
183 auto result = assumptionMaker.createAndCheckAssumptions(1, 2, order, region);
184
185 EXPECT_EQ(1ul, result.size());
186 auto itr = result.begin();
187 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second);
188 EXPECT_EQ(1ul, itr->first.state1);
189 EXPECT_EQ(2ul, itr->first.state2);
190 EXPECT_EQ(storm::analysis::AssumptionRelation::Greater, itr->first.relation);
191}
TEST_F
TEST_F(AssumptionMakerTest, Brp_without_bisimulation)
Definition AssumptionMakerTest.cpp:35
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:16
storm::prism::Program::preprocess
Program preprocess(std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions) const
Preprocesses the program by defining the given constant definitions, substituting constants and formu...
Definition Program.cpp:1170
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::BitVector::set
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
Definition BitVector.cpp:245
storm::storage::StronglyConnectedComponentDecomposition
This class represents the decomposition of a graph-like structure into its strongly connected compone...
Definition StronglyConnectedComponentDecomposition.h:100
storm::transformer::SparseParametricModelSimplifier
This class performs different steps to simplify the given (parametric) model.
Definition SparseParametricModelSimplifier.h:21
model_descriptions.h
storm::api::parseRegion
storm::storage::ParameterRegion< ValueType > parseRegion(std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)
Definition region.h:134
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:70
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::buildSparseModel
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildSparseModel(storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options, typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &explorationOptions=typename storm::builder::ExplicitModelBuilder< ValueType >::Options())
Definition builder.h:117
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:62
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:732
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:1883
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