Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
verification.h
Go to the documentation of this file.
1#pragma once
2
3#include <type_traits>
4
6
20
24
28
33
35
39
40namespace storm {
41namespace api {
42
43template<typename ValueType>
44storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> createTask(std::shared_ptr<const storm::logic::Formula> const& formula,
45 bool onlyInitialStatesRelevant = false) {
46 return storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula, onlyInitialStatesRelevant);
47}
48
49//
50// Verifying with Exploration engine
51//
52template<typename ValueType>
53std::unique_ptr<storm::modelchecker::CheckResult> verifyWithExplorationEngine(storm::Environment const& env,
56 if (!std::is_same_v<ValueType, double>) {
57 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exploration engine does not support data type.");
58 } else {
59 STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Exploration engine is currently only applicable to PRISM models.");
60 storm::prism::Program const& program = model.asPrismProgram();
61
62 std::unique_ptr<storm::modelchecker::CheckResult> result;
65 if (checker.canHandle(task)) {
66 result = checker.check(env, task);
67 }
70 if (checker.canHandle(task)) {
71 result = checker.check(env, task);
72 }
73 } else {
74 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
75 "The model type " << program.getModelType() << " is not supported by the exploration engine.");
76 }
77
78 return result;
79 }
80}
81
82template<typename ValueType>
83std::unique_ptr<storm::modelchecker::CheckResult> verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model,
85 Environment env;
86 return verifyWithExplorationEngine(env, model, task);
87}
88
89//
90// Verifying with Sparse engine
91//
92template<typename ValueType>
93std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
94 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> const& dtmc,
96 if constexpr (storm::IsIntervalType<ValueType>) {
97 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify interval DTMCs.");
98 } else {
99 std::unique_ptr<storm::modelchecker::CheckResult> result;
100 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination &&
101 storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) {
103 if (modelchecker.canHandle(task)) {
104 result = modelchecker.check(env, task);
105 }
106 } else {
108 if (modelchecker.canHandle(task)) {
109 result = modelchecker.check(env, task);
110 }
111 }
112 return result;
113 }
114}
115
116template<typename ValueType>
117std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> const& dtmc,
119 Environment env;
120 return verifyWithSparseEngine(env, dtmc, task);
121}
122
123template<typename ValueType>
124std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
125 std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmc,
127 if constexpr (storm::IsIntervalType<ValueType>) {
128 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify interval CTMCs.");
129 } else {
130 std::unique_ptr<storm::modelchecker::CheckResult> result;
132 if (modelchecker.canHandle(task)) {
133 result = modelchecker.check(env, task);
134 }
135 return result;
136 }
137}
138
139template<typename ValueType>
140std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmc,
142 Environment env;
143 return verifyWithSparseEngine(env, ctmc, task);
144}
145
146template<typename ValueType>
147std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
148 std::shared_ptr<storm::models::sparse::Mdp<ValueType>> const& mdp,
150 using ModelCheckerType = std::conditional_t<std::is_same_v<ValueType, storm::RationalFunction>,
153
154 std::unique_ptr<storm::modelchecker::CheckResult> result;
155 ModelCheckerType modelchecker(*mdp);
156 // The CheckTask needs to have the SolutionType. For now, we create a copy.
157 // TODO: This is a little messy: the CheckTask should have been provided with the right solution type already.
158 auto newTask = task.template convertValueType<typename ModelCheckerType::SolutionType>();
159 if (modelchecker.canHandle(newTask)) {
160 result = modelchecker.check(env, newTask);
161 }
162 return result;
163}
164
165template<typename ValueType>
166std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Mdp<ValueType>> const& mdp,
168 Environment env;
169 return verifyWithSparseEngine(env, mdp, task);
170}
171
172template<typename ValueType>
173std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
174 std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const& ma,
176 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
177 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MAs with this data type.");
178 } else {
179 std::unique_ptr<storm::modelchecker::CheckResult> result;
180
181 // Close the MA, if it is not already closed.
182 if (!ma->isClosed()) {
183 STORM_LOG_WARN("Closing Markov automaton. Consider closing the MA before verification.");
184 ma->close();
185 }
186
188 if (modelchecker.canHandle(task)) {
189 result = modelchecker.check(env, task);
190 }
191 return result;
192 }
193}
194
195template<typename ValueType>
196std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const& ma,
198 Environment env;
199 return verifyWithSparseEngine(env, ma, task);
200}
201
202template<typename ValueType>
203std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
204 std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& smg,
206 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
207 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify SMGs with this data type.");
208 } else {
209 std::unique_ptr<storm::modelchecker::CheckResult> result;
211 if (modelchecker.canHandle(task)) {
212 result = modelchecker.check(env, task);
213 }
214 return result;
215 }
216}
217
218template<typename ValueType>
219std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& smg,
221 Environment env;
222 return verifyWithSparseEngine(env, smg, task);
223}
224
225template<typename ValueType>
226std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env,
227 std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model,
229 std::unique_ptr<storm::modelchecker::CheckResult> result;
230 if (model->getType() == storm::models::ModelType::Dtmc) {
231 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Dtmc<ValueType>>(), task);
232 } else if (model->getType() == storm::models::ModelType::Mdp) {
233 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Mdp<ValueType>>(), task);
234 } else if (model->getType() == storm::models::ModelType::Ctmc) {
235 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Ctmc<ValueType>>(), task);
236 } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
237 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), task);
238 } else if (model->getType() == storm::models::ModelType::Smg) {
239 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Smg<ValueType>>(), task);
240 } else {
241 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the sparse engine.");
242 }
243 return result;
244}
245
246template<typename ValueType>
247std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model,
249 Environment env;
250 return verifyWithSparseEngine(env, model, task);
251}
252
253template<typename ValueType>
254std::unique_ptr<storm::modelchecker::CheckResult> computeSteadyStateDistributionWithSparseEngine(
255 storm::Environment const& env, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> const& dtmc) {
256 if constexpr (storm::IsIntervalType<ValueType>) {
257 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Can not compute steady state distributions for interval models.");
258 } else {
259 std::unique_ptr<storm::modelchecker::CheckResult> result;
261 return modelchecker.computeSteadyStateDistribution(env);
262 }
263}
264
265template<typename ValueType>
266std::unique_ptr<storm::modelchecker::CheckResult> computeSteadyStateDistributionWithSparseEngine(
267 storm::Environment const& env, std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmc) {
268 if constexpr (storm::IsIntervalType<ValueType>) {
269 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Can not compute steady state distributions for interval models.");
270 } else {
271 std::unique_ptr<storm::modelchecker::CheckResult> result;
273 return modelchecker.computeSteadyStateDistribution(env);
274 }
275}
276
277template<typename ValueType>
278std::unique_ptr<storm::modelchecker::CheckResult> computeSteadyStateDistributionWithSparseEngine(
279 storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
280 std::unique_ptr<storm::modelchecker::CheckResult> result;
281 if (model->getType() == storm::models::ModelType::Dtmc) {
283 } else if (model->getType() == storm::models::ModelType::Ctmc) {
285 } else {
286 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
287 "Computing the long run average distribution for the model type " << model->getType() << " is not supported.");
288 }
289 return result;
290}
291
292template<typename ValueType>
293std::unique_ptr<storm::modelchecker::CheckResult> computeExpectedVisitingTimesWithSparseEngine(
294 storm::Environment const& env, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> const& dtmc) {
295 if constexpr (storm::IsIntervalType<ValueType>) {
296 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Can not compute expected visiting times for interval models.");
297 } else {
298 std::unique_ptr<storm::modelchecker::CheckResult> result;
300 return modelchecker.computeExpectedVisitingTimes(env);
301 }
302}
303
304template<typename ValueType>
305std::unique_ptr<storm::modelchecker::CheckResult> computeExpectedVisitingTimesWithSparseEngine(
306 storm::Environment const& env, std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmc) {
307 if constexpr (storm::IsIntervalType<ValueType>) {
308 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Can not compute expected visiting times for interval models.");
309 } else {
310 std::unique_ptr<storm::modelchecker::CheckResult> result;
312 return modelchecker.computeExpectedVisitingTimes(env);
313 }
314}
315
316template<typename ValueType>
317std::unique_ptr<storm::modelchecker::CheckResult> computeExpectedVisitingTimesWithSparseEngine(
318 storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
319 std::unique_ptr<storm::modelchecker::CheckResult> result;
320 if (model->getType() == storm::models::ModelType::Dtmc) {
322 } else if (model->getType() == storm::models::ModelType::Ctmc) {
324 } else {
325 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
326 "Computing expected visiting times for the model type " << model->getType() << " is not supported.");
327 }
328 return result;
329}
330
331//
332// Verifying with Hybrid engine
333//
334template<storm::dd::DdType DdType, typename ValueType>
335std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(storm::Environment const& env,
336 std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> const& dtmc,
338 if constexpr (storm::IsIntervalType<ValueType>) {
339 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify DTMC with this data type.");
340 } else {
341 std::unique_ptr<storm::modelchecker::CheckResult> result;
342 dtmc->getManager().execute([&]() {
344 if (modelchecker.canHandle(task)) {
345 result = modelchecker.check(env, task);
346 }
347 });
348 return result;
349 }
350}
351
352template<storm::dd::DdType DdType, typename ValueType>
353std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> const& dtmc,
355 Environment env;
356 return verifyWithHybridEngine(env, dtmc, task);
357}
358
359template<storm::dd::DdType DdType, typename ValueType>
360std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(storm::Environment const& env,
361 std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>> const& ctmc,
363 if constexpr (storm::IsIntervalType<ValueType>) {
364 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify CTMC with this data type.");
365 } else {
366 std::unique_ptr<storm::modelchecker::CheckResult> result;
367 ctmc->getManager().execute([&]() {
369 if (modelchecker.canHandle(task)) {
370 result = modelchecker.check(env, task);
371 }
372 });
373 return result;
374 }
375}
376
377template<storm::dd::DdType DdType, typename ValueType>
378std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>> const& ctmc,
380 Environment env;
381 return verifyWithHybridEngine(env, ctmc, task);
382}
383
384template<storm::dd::DdType DdType, typename ValueType>
385std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(storm::Environment const& env,
386 std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> const& mdp,
388 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
389 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify MDPs with this data type.");
390 } else {
391 std::unique_ptr<storm::modelchecker::CheckResult> result;
392 mdp->getManager().execute([&]() {
394 if (modelchecker.canHandle(task)) {
395 result = modelchecker.check(env, task);
396 }
397 });
398 return result;
399 }
400}
401
402template<storm::dd::DdType DdType, typename ValueType>
403std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> const& mdp,
405 Environment env;
406 return verifyWithHybridEngine(env, mdp, task);
407}
408
409template<storm::dd::DdType DdType, typename ValueType>
410std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(storm::Environment const& env,
413 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
414 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify MDPs with this data type.");
415 } else {
416 std::unique_ptr<storm::modelchecker::CheckResult> result;
417 ma->getManager().execute([&]() {
419 if (modelchecker.canHandle(task)) {
420 result = modelchecker.check(env, task);
421 }
422 });
423 return result;
424 }
425}
426
427template<storm::dd::DdType DdType, typename ValueType>
428std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>> const& ma,
430 Environment env;
431 return verifyWithHybridEngine(env, ma, task);
432}
433
434template<storm::dd::DdType DdType, typename ValueType>
435std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(storm::Environment const& env,
436 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
438 std::unique_ptr<storm::modelchecker::CheckResult> result;
439 if (model->getType() == storm::models::ModelType::Dtmc) {
440 result = verifyWithHybridEngine(env, model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), task);
441 } else if (model->getType() == storm::models::ModelType::Ctmc) {
442 result = verifyWithHybridEngine(env, model->template as<storm::models::symbolic::Ctmc<DdType, ValueType>>(), task);
443 } else if (model->getType() == storm::models::ModelType::Mdp) {
444 result = verifyWithHybridEngine(env, model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), task);
445 } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
447 } else {
448 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the hybrid engine.");
449 }
450 return result;
451}
452
453template<storm::dd::DdType DdType, typename ValueType>
454std::unique_ptr<storm::modelchecker::CheckResult> verifyWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
456 Environment env;
457 return verifyWithHybridEngine(env, model, task);
458}
459
460//
461// Verifying with DD engine
462//
463template<storm::dd::DdType DdType, typename ValueType>
464std::unique_ptr<storm::modelchecker::CheckResult> verifyWithDdEngine(storm::Environment const& env,
465 std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> const& dtmc,
467 if constexpr (storm::IsIntervalType<ValueType>) {
468 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify DTMC with this data type.");
469 } else {
470 std::unique_ptr<storm::modelchecker::CheckResult> result;
471 dtmc->getManager().execute([&]() {
473 if (modelchecker.canHandle(task)) {
474 result = modelchecker.check(env, task);
475 }
476 });
477 return result;
478 }
479}
480
481template<storm::dd::DdType DdType, typename ValueType>
482std::unique_ptr<storm::modelchecker::CheckResult> verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>> const& dtmc,
484 Environment env;
485 return verifyWithDdEngine(env, dtmc, task);
486}
487
488template<storm::dd::DdType DdType, typename ValueType>
489std::unique_ptr<storm::modelchecker::CheckResult> verifyWithDdEngine(storm::Environment const& env,
490 std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> const& mdp,
492 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || storm::IsIntervalType<ValueType>) {
493 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type.");
494 } else {
495 std::unique_ptr<storm::modelchecker::CheckResult> result;
496 mdp->getManager().execute([&]() {
498 if (modelchecker.canHandle(task)) {
499 result = modelchecker.check(env, task);
500 }
501 });
502 return result;
503 }
504}
505
506template<storm::dd::DdType DdType, typename ValueType>
507std::unique_ptr<storm::modelchecker::CheckResult> verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> const& mdp,
509 Environment env;
510 return verifyWithDdEngine(env, mdp, task);
511}
512
513template<storm::dd::DdType DdType, typename ValueType>
514std::unique_ptr<storm::modelchecker::CheckResult> verifyWithDdEngine(storm::Environment const& env,
515 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
517 std::unique_ptr<storm::modelchecker::CheckResult> result;
518 if (model->getType() == storm::models::ModelType::Dtmc) {
519 result = verifyWithDdEngine(env, model->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), task);
520 } else if (model->getType() == storm::models::ModelType::Mdp) {
521 result = verifyWithDdEngine(env, model->template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), task);
522 } else {
523 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the dd engine.");
524 }
525 return result;
526}
527
528template<storm::dd::DdType DdType, typename ValueType>
529std::unique_ptr<storm::modelchecker::CheckResult> verifyWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model,
531 Environment env;
532 return verifyWithDdEngine(env, model, task);
533}
534
535} // namespace api
536} // namespace storm
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
std::unique_ptr< CheckResult > computeExpectedVisitingTimes(Environment const &env)
Computes for each state the expected number of times we visit that state.
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
std::unique_ptr< CheckResult > computeSteadyStateDistribution(Environment const &env)
Computes the long run average (or: steady state) distribution over all states Assumes a uniform distr...
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
std::unique_ptr< CheckResult > computeExpectedVisitingTimes(Environment const &env)
Computes for each state the expected number of times we visit that state.
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
std::unique_ptr< CheckResult > computeSteadyStateDistribution(Environment const &env)
Computes the long run average (or: steady state) distribution over all states Assumes a uniform distr...
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
This class represents a continuous-time Markov chain.
Definition Ctmc.h:14
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
This class represents a Markov automaton.
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
Base class for all sparse models.
Definition Model.h:32
This class represents a stochastic multiplayer game.
Definition Smg.h:17
This class represents a continuous-time Markov chain.
Definition Ctmc.h:14
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
This class represents a discrete-time Markov decision process.
This class represents a discrete-time Markov decision process.
Definition Mdp.h:14
Base class for all symbolic models.
Definition Model.h:45
ModelType getModelType() const
Retrieves the model type of the model.
Definition Program.cpp:247
storm::prism::Program const & asPrismProgram() const
#define STORM_LOG_WARN(message)
Definition logging.h:25
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithHybridEngine(storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > createTask(std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithExplorationEngine(storm::Environment const &env, storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
std::unique_ptr< storm::modelchecker::CheckResult > computeExpectedVisitingTimesWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithDdEngine(storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
std::unique_ptr< storm::modelchecker::CheckResult > verifyWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
std::unique_ptr< storm::modelchecker::CheckResult > computeSteadyStateDistributionWithSparseEngine(storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)
LabParser.cpp.