Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseRobustDtmcParameterLiftingTest.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/RegionCheckEngine.h"
6#include "storm-parsers/api/model_descriptions.h"
7#include "storm-parsers/api/properties.h"
8#include "storm/adapters/RationalFunctionAdapter.h"
9#include "storm/api/builder.h"
10#include "storm/api/properties.h"
11#include "storm/api/verification.h"
12#include "storm/environment/solver/MinMaxSolverEnvironment.h"
13#include "storm/storage/prism/Program.h"
14#include "storm/utility/constants.h"
15
16namespace {
17class IsGraphPreserving {
18 public:
19 typedef double ValueType;
20 static storm::Environment createEnvironment() {
21 storm::Environment env;
22 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
23 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
24 return env;
25 }
26 static bool graphPreserving() {
27 return true;
28 }
29};
30
31class AssumeGraphPreserving {
32 public:
33 typedef double ValueType;
34 static storm::Environment createEnvironment() {
35 storm::Environment env;
36 env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
37 env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
38 return env;
39 }
40 static bool graphPreserving() {
41 return false;
42 }
43};
44
45template<typename TestType>
46class SparseRobustDtmcParameterLiftingTest : public ::testing::Test {
47 public:
48 typedef typename TestType::ValueType ValueType;
49 SparseRobustDtmcParameterLiftingTest() : _environment(TestType::createEnvironment()), _graphPreserving(TestType::graphPreserving()) {}
50 storm::Environment const& env() const {
51 return _environment;
52 }
53 bool const& graphPreserving() const {
54 return _graphPreserving;
55 }
56 virtual void SetUp() {
57 carl::VariablePool::getInstance().clear();
58#ifndef STORM_HAVE_Z3
59 GTEST_SKIP() << "Z3 not available.";
60#endif
61 }
62 virtual void TearDown() {
63 carl::VariablePool::getInstance().clear();
64 }
65
66 private:
67 storm::Environment _environment;
68 bool _graphPreserving;
69};
70
71void checkBrpProb(storm::Environment const& env, bool graphPreserving) {
72 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
73 std::string formulaAsString = "P<=0.84 [F s=5 ]";
74 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
75
76 // Program and formula
77 storm::prism::Program program = storm::api::parseProgram(programFile);
78 program = program.preprocess(constantsAsString);
79 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
80 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
81 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
82 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
83
84 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
85 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
86 modelParameters.insert(rewParameters.begin(), rewParameters.end());
87
88 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
89 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
90 graphPreserving);
91
92 // start testing
93 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
94 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
95 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
96
97 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
98 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
99 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
100 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
101 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
102 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
103}
104
105void checkBrpRew(storm::Environment const& env, bool graphPreserving) {
106 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
107 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
108 std::string constantsAsString = "pL=0.9,TOAck=0.5";
109
110 storm::prism::Program program = storm::api::parseProgram(programFile);
111 program = program.preprocess(constantsAsString);
112 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
113 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
114 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
115 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
116
117 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
118 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
119 modelParameters.insert(rewParameters.begin(), rewParameters.end());
120
121 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
122 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
123 graphPreserving);
124
125 // start testing
126 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
127 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
128 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
129
130 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
131 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
132 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
133 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
134 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
135 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
136}
137
138void checkBrpRew4Par(storm::Environment const& env, bool graphPreserving) {
139 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
140 std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
141 std::string constantsAsString = "";
142 storm::prism::Program program = storm::api::parseProgram(programFile);
143 program = program.preprocess(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
149 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
150 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
151 modelParameters.insert(rewParameters.begin(), rewParameters.end());
152
153 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
154 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
155 graphPreserving);
156
157 // start testing
158 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
159 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
160 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
161
162 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
163 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
164 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
165 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
166 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
167 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
168}
169
170void checkCrowdsProb(storm::Environment const& env, bool graphPreserving) {
171 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
172 std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
173 std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5
174
175 storm::prism::Program program = storm::api::parseProgram(programFile);
176 program = program.preprocess(constantsAsString);
177 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
178 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
179 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
180 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
181
182 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
183 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
184 modelParameters.insert(rewParameters.begin(), rewParameters.end());
185
186 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
187 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
188 graphPreserving);
189
190 // start testing
191 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
192 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
193 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
194 auto allVioHardRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
195
196 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
197 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
198 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
199 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
200 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
201 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
202 EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated,
203 regionChecker->analyzeRegion(env, allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
204}
205
206void checkCrowdsProb1Par(storm::Environment const& env, bool graphPreserving) {
207 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
208 std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
209 std::string constantsAsString = "badC=0.3"; // e.g. pL=0.9,TOACK=0.5
210
211 storm::prism::Program program = storm::api::parseProgram(programFile);
212 program = program.preprocess(constantsAsString);
213 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
214 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
215 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
216 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
217
218 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
219 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
220 modelParameters.insert(rewParameters.begin(), rewParameters.end());
221
222 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
223 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
224 graphPreserving);
225
226 // start testing
227 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.9<=PF<=0.99", modelParameters);
228 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.9", modelParameters);
229 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.01<=PF<=0.8", modelParameters);
230
231 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
232 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
233 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
234 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
235 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
236 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
237}
238
239void checkCrowdsProbConst(storm::Environment const& env, bool graphPreserving) {
240 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
241 std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
242 std::string constantsAsString = "PF=0.9,badC=0.2";
243
244 storm::prism::Program program = storm::api::parseProgram(programFile);
245 program = program.preprocess(constantsAsString);
246 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
247 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
248 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
249 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
250
251 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
252 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
253 modelParameters.insert(rewParameters.begin(), rewParameters.end());
254
255 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
256 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
257 graphPreserving);
258
259 // start testing
260 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("", modelParameters);
261
262 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
263 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
264}
265
266void checkZeroConf(storm::Environment const& env, bool graphPreserving) {
267 std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/zeroconf4.pm";
268 std::string formulaAsString = "P>0.5 [F s=5 ]";
269 std::string constantsAsString = " n = 4"; // e.g. pL=0.9,TOACK=0.5
270
271 // Program and formula
272 storm::prism::Program program = storm::api::parseProgram(programFile);
273 program = program.preprocess(constantsAsString);
274 std::vector<std::shared_ptr<const storm::logic::Formula>> formulas =
275 storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
276 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model =
277 storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
278
279 auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
280 auto rewParameters = storm::models::sparse::getRewardParameters(*model);
281 modelParameters.insert(rewParameters.begin(), rewParameters.end());
282
283 auto regionChecker = storm::api::initializeRegionModelChecker<storm::RationalFunction>(
284 env, model, storm::api::createTask<storm::RationalFunction>(formulas[0], true), storm::modelchecker::RegionCheckEngine::RobustParameterLifting, true,
285 graphPreserving);
286
287 // start testing
288 auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.8<=pL<=0.95,0.8<=pK<=0.95", modelParameters);
289 auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=pL<=0.9,0.6<=pK<=0.9", modelParameters);
290 auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.7,0.1<=pK<=0.7", modelParameters);
291
292 EXPECT_EQ(storm::modelchecker::RegionResult::AllSat,
293 regionChecker->analyzeRegion(env, allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
294 EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth,
295 regionChecker->analyzeRegion(env, exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
296 EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated,
297 regionChecker->analyzeRegion(env, allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, true));
298}
299
300typedef ::testing::Types<IsGraphPreserving, AssumeGraphPreserving> TestingTypes;
301
302TYPED_TEST_SUITE(SparseRobustDtmcParameterLiftingTest, TestingTypes, );
303
304TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Prob) {
305 checkBrpProb(this->env(), this->graphPreserving());
306}
307
308TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Rew) {
309 checkBrpRew(this->env(), this->graphPreserving());
310}
311
312TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Rew_4Par) {
313 checkBrpRew4Par(this->env(), this->graphPreserving());
314}
315
316TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Crowds_Prob) {
317 checkCrowdsProb(this->env(), this->graphPreserving());
318}
319
320TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Crowds_Prob_1Par) {
321 checkCrowdsProb1Par(this->env(), this->graphPreserving());
322}
323
324TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Crowds_Prob_Const) {
325 checkCrowdsProbConst(this->env(), this->graphPreserving());
326}
327
328TYPED_TEST(SparseRobustDtmcParameterLiftingTest, ZeroConf) {
329 checkZeroConf(this->env(), this->graphPreserving());
330}
331} // namespace
storm::Environment::solver
SolverEnvironment & solver()
Definition Environment.cpp:26
storm::MinMaxSolverEnvironment::setPrecision
void setPrecision(storm::RationalNumber value)
Definition MinMaxSolverEnvironment.cpp:60
storm::MinMaxSolverEnvironment::setMethod
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
Definition MinMaxSolverEnvironment.cpp:43
storm::SolverEnvironment::minMax
MinMaxSolverEnvironment & minMax()
Definition SolverEnvironment.cpp:48
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
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
model_descriptions.h
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::createTask
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > createTask(std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)
Definition verification.h:44
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:133
storm::api::parseProgram
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
Definition model_descriptions.cpp:17
storm::api::initializeRegionModelChecker
std::unique_ptr< storm::modelchecker::RegionModelChecker< ValueType > > initializeRegionModelChecker(Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, storm::modelchecker::RegionCheckEngine engine, bool allowModelSimplification=true, bool graphPreserving=true, bool preconditionsValidated=false, MonotonicitySetting monotonicitySetting=MonotonicitySetting(), std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > > > monotoneParameters=std::nullopt)
Definition region.h:237
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::modelchecker::RegionResult::AllSat
@ AllSat
the formula is satisfied for all well-defined parameters in the given region
Definition RegionResult.h:19
storm::modelchecker::RegionResult::AllViolated
@ AllViolated
the formula is violated for all well-defined parameters in the given region
Definition RegionResult.h:20
storm::modelchecker::RegionResult::ExistsBoth
@ ExistsBoth
the formula is satisfied for some parameters but also violated for others
Definition RegionResult.h:18
storm::modelchecker::RegionResult::CenterViolated
@ CenterViolated
the formula is violated for the parameter Valuation that corresponds to the center point of the regio...
Definition RegionResult.h:16
storm::modelchecker::RegionCheckEngine::RobustParameterLifting
@ RobustParameterLifting
Parameter lifting approach based on robust markov models instead of generating nondeterminism.
Definition RegionCheckEngine.h:15
storm::models::sparse::getRewardParameters
std::set< storm::RationalFunctionVariable > getRewardParameters(Model< storm::RationalFunction > const &model)
Get all parameters occurring in rewards.
Definition Model.cpp:698
storm::models::sparse::getProbabilityParameters
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
Definition Model.cpp:694
storm::utility::convertNumber
TargetType convertNumber(SourceType const &number)
Definition constants.cpp:143
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:64
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h