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