Storm 1.14.0.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/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/storage/StronglyConnectedComponentDecomposition.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 = program.preprocess(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::SparseParametricModelSimplifier<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 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 storm::analysis::Assumption assumption{7, 5, storm::analysis::AssumptionRelation::Greater};
74 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
75
76 assumption = storm::analysis::Assumption{5, 7, storm::analysis::AssumptionRelation::Greater};
77 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
78
79 assumption = storm::analysis::Assumption{7, 5, storm::analysis::AssumptionRelation::Equal};
80 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
81
82 checker.initializeCheckingOnSamples(storm::Environment(), formulas[0], dtmc, region, 3);
83 assumption = storm::analysis::Assumption{7, 5, storm::analysis::AssumptionRelation::Greater};
84 EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region));
85
86 assumption = storm::analysis::Assumption{5, 7, storm::analysis::AssumptionRelation::Greater};
87 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region));
88
89 assumption = storm::analysis::Assumption{7, 5, storm::analysis::AssumptionRelation::Equal};
90 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region));
91}
92
93TEST_F(AssumptionCheckerTest, Simple1) {
94 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/simple1.pm";
95 std::string formulaAsString = "P=? [F s=3]";
96 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
97
98 // Program and formula
99 storm::prism::Program program = storm::api::parseProgram(programFile);
100 program = program.preprocess(constantsAsString);
101 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
102 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
103 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
104 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
105 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
106 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
107 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
108 model = simplifier.getSimplifiedModel();
109 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
110
111 ASSERT_EQ(5ul, dtmc->getNumberOfStates());
112 ASSERT_EQ(8ul, dtmc->getNumberOfTransitions());
113
114 // Create the region
115 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
116 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars);
117
118 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
119
120 storm::storage::StronglyConnectedComponentDecompositionOptions options;
121 options.forceTopologicalSort();
122 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
123
124 storm::storage::BitVector above(5);
125 above.set(3);
126 storm::storage::BitVector below(5);
127 below.set(4);
128 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
129 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
130
131 // Validating
132 storm::analysis::Assumption assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
133 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
134
135 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
136 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
137
138 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
139 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
140
141 region = storm::api::parseRegion<storm::RationalFunction>("0.51 <= p <= 0.99", vars);
142 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
143 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
144
145 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
146 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
147
148 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
149 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
150}
151
152TEST_F(AssumptionCheckerTest, Casestudy1) {
153 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy1.pm";
154 std::string formulaAsString = "P=? [F s=3]";
155 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
156
157 // Program and formula
158 storm::prism::Program program = storm::api::parseProgram(programFile);
159 program = program.preprocess(constantsAsString);
160 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
161 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
162 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
163 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
164 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
165 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
166 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
167 model = simplifier.getSimplifiedModel();
168 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
169
170 ASSERT_EQ(5ul, dtmc->getNumberOfStates());
171 ASSERT_EQ(8ul, dtmc->getNumberOfTransitions());
172
173 // Create the region
174 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
175 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars);
176
177 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
178
179 storm::storage::BitVector above(5);
180 above.set(3);
181 storm::storage::BitVector below(5);
182 below.set(4);
183
184 storm::storage::StronglyConnectedComponentDecompositionOptions options;
185 options.forceTopologicalSort();
186 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
187 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
188 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 5, decomposition, statesSorted));
189
190 // Validating
191 storm::analysis::Assumption assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
192 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
193
194 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
195 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
196
197 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
198 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
199
200 checker.initializeCheckingOnSamples(storm::Environment(), formulas[0], dtmc, region, 3);
201 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
202 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
203
204 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
205 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
206
207 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
208 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
209}
210
211TEST_F(AssumptionCheckerTest, Casestudy2) {
212 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy2.pm";
213 std::string formulaAsString = "P=? [F s=4]";
214 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
215
216 // Program and formula
217 storm::prism::Program program = storm::api::parseProgram(programFile);
218 program = program.preprocess(constantsAsString);
219 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
220 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
221 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
222 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
223 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
224 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
225 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
226 model = simplifier.getSimplifiedModel();
227 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
228
229 ASSERT_EQ(6ul, dtmc->getNumberOfStates());
230 ASSERT_EQ(12ul, dtmc->getNumberOfTransitions());
231
232 // Create the region
233 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
234 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.99999", vars);
235
236 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
237
238 storm::storage::BitVector above(6);
239 above.set(4);
240 storm::storage::BitVector below(6);
241 below.set(5);
242
243 storm::storage::StronglyConnectedComponentDecompositionOptions options;
244 options.forceTopologicalSort();
245 auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<storm::RationalFunction>(model->getTransitionMatrix(), options);
246 auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix());
247 auto order = std::shared_ptr<storm::analysis::Order>(new storm::analysis::Order(above, below, 6, decomposition, statesSorted));
248 order->add(3);
249
250 // Checking on samples and validate
251 storm::analysis::Assumption assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
252 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
253
254 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
255 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
256
257 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
258 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
259}
260
261TEST_F(AssumptionCheckerTest, Casestudy3) {
262 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/casestudy3.pm";
263 std::string formulaAsString = "P=? [F s=3]";
264 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
265
266 // Program and formula
267 storm::prism::Program program = storm::api::parseProgram(programFile);
268 program = program.preprocess(constantsAsString);
269 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
270 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
271 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
272 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
273 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
274 auto simplifier = storm::transformer::SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>(*dtmc);
275 ASSERT_TRUE(simplifier.simplify(*(formulas[0])));
276 model = simplifier.getSimplifiedModel();
277 dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
278
279 ASSERT_EQ(5ul, dtmc->getNumberOfStates());
280 ASSERT_EQ(8ul, dtmc->getNumberOfTransitions());
281
282 // Create the region
283 auto vars = storm::models::sparse::getProbabilityParameters(*dtmc);
284 auto region = storm::api::parseRegion<storm::RationalFunction>("0.00001 <= p <= 0.4", vars);
285
286 auto checker = storm::analysis::AssumptionChecker<storm::RationalFunction, double>(dtmc->getTransitionMatrix());
287
288 // Order
289 storm::storage::BitVector above(5);
290 above.set(3);
291 storm::storage::BitVector below(5);
292 below.set(4);
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, 5, decomposition, statesSorted));
298
299 storm::analysis::Assumption assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
300 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
301
302 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
303 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
304
305 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
306 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
307
308 checker.initializeCheckingOnSamples(storm::Environment(), formulas[0], dtmc, region, 3);
309
310 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Greater};
311 EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region));
312
313 assumption = storm::analysis::Assumption{2, 1, storm::analysis::AssumptionRelation::Greater};
314 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
315
316 assumption = storm::analysis::Assumption{1, 2, storm::analysis::AssumptionRelation::Equal};
317 EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region));
318}
TEST_F
TEST_F(AssumptionCheckerTest, Brp_no_bisimulation)
Definition AssumptionCheckerTest.cpp:34
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::models::sparse::Model::getTransitionMatrix
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:226
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:196
storm::models::sparse::Model::getNumberOfStates
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:191
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::analysis::Assumption
A candidate relation between two states of a reachability order: either state1 > state2 (Greater) or ...
Definition Assumption.h:20
storm::storage::StronglyConnectedComponentDecompositionOptions::forceTopologicalSort
StronglyConnectedComponentDecompositionOptions & forceTopologicalSort(bool value=true)
Enforces that the returned SCCs are sorted in a topological order.
Definition StronglyConnectedComponentDecomposition.cpp:33