43template<
typename ValueType>
45 bool onlyInitialStatesRelevant =
false) {
52template<
typename ValueType>
56 if (!std::is_same_v<ValueType, double>) {
57 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Exploration engine does not support data type.");
59 STORM_LOG_THROW(model.
isPrismProgram(), storm::exceptions::NotSupportedException,
"Exploration engine is currently only applicable to PRISM models.");
62 std::unique_ptr<storm::modelchecker::CheckResult> result;
66 result = checker.
check(env, task);
71 result = checker.
check(env, task);
75 "The model type " << program.
getModelType() <<
" is not supported by the exploration engine.");
82template<
typename ValueType>
92template<
typename ValueType>
96 if constexpr (storm::IsIntervalType<ValueType>) {
97 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Sparse engine cannot verify interval DTMCs.");
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()) {
104 result = modelchecker.
check(env, task);
109 result = modelchecker.
check(env, task);
116template<
typename ValueType>
123template<
typename ValueType>
127 if constexpr (storm::IsIntervalType<ValueType>) {
128 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Sparse engine cannot verify interval CTMCs.");
130 std::unique_ptr<storm::modelchecker::CheckResult> result;
133 result = modelchecker.
check(env, task);
139template<
typename ValueType>
146template<
typename ValueType>
150 using ModelCheckerType = std::conditional_t<std::is_same_v<ValueType, storm::RationalFunction>,
154 std::unique_ptr<storm::modelchecker::CheckResult> result;
155 ModelCheckerType modelchecker(*mdp);
158 auto newTask = task.template convertValueType<typename ModelCheckerType::SolutionType>();
159 if (modelchecker.canHandle(newTask)) {
160 result = modelchecker.check(env, newTask);
165template<
typename ValueType>
172template<
typename ValueType>
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.");
179 std::unique_ptr<storm::modelchecker::CheckResult> result;
182 if (!ma->isClosed()) {
183 STORM_LOG_WARN(
"Closing Markov automaton. Consider closing the MA before verification.");
189 result = modelchecker.
check(env, task);
195template<
typename ValueType>
202template<
typename ValueType>
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.");
209 std::unique_ptr<storm::modelchecker::CheckResult> result;
212 result = modelchecker.
check(env, task);
218template<
typename ValueType>
225template<
typename ValueType>
229 std::unique_ptr<storm::modelchecker::CheckResult> result;
241 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The model type " << model->getType() <<
" is not supported by the sparse engine.");
246template<
typename ValueType>
253template<
typename ValueType>
256 if constexpr (storm::IsIntervalType<ValueType>) {
257 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Can not compute steady state distributions for interval models.");
259 std::unique_ptr<storm::modelchecker::CheckResult> result;
265template<
typename ValueType>
268 if constexpr (storm::IsIntervalType<ValueType>) {
269 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Can not compute steady state distributions for interval models.");
271 std::unique_ptr<storm::modelchecker::CheckResult> result;
277template<
typename ValueType>
280 std::unique_ptr<storm::modelchecker::CheckResult> result;
287 "Computing the long run average distribution for the model type " << model->getType() <<
" is not supported.");
292template<
typename ValueType>
295 if constexpr (storm::IsIntervalType<ValueType>) {
296 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Can not compute expected visiting times for interval models.");
298 std::unique_ptr<storm::modelchecker::CheckResult> result;
304template<
typename ValueType>
307 if constexpr (storm::IsIntervalType<ValueType>) {
308 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Can not compute expected visiting times for interval models.");
310 std::unique_ptr<storm::modelchecker::CheckResult> result;
316template<
typename ValueType>
319 std::unique_ptr<storm::modelchecker::CheckResult> result;
326 "Computing expected visiting times for the model type " << model->getType() <<
" is not supported.");
334template<storm::dd::DdType DdType,
typename ValueType>
338 if constexpr (storm::IsIntervalType<ValueType>) {
339 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Hybrid engine cannot verify DTMC with this data type.");
341 std::unique_ptr<storm::modelchecker::CheckResult> result;
342 dtmc->getManager().execute([&]() {
345 result = modelchecker.
check(env, task);
352template<storm::dd::DdType DdType,
typename ValueType>
359template<storm::dd::DdType DdType,
typename ValueType>
363 if constexpr (storm::IsIntervalType<ValueType>) {
364 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Hybrid engine cannot verify CTMC with this data type.");
366 std::unique_ptr<storm::modelchecker::CheckResult> result;
367 ctmc->getManager().execute([&]() {
370 result = modelchecker.
check(env, task);
377template<storm::dd::DdType DdType,
typename ValueType>
384template<storm::dd::DdType DdType,
typename ValueType>
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.");
391 std::unique_ptr<storm::modelchecker::CheckResult> result;
392 mdp->getManager().execute([&]() {
395 result = modelchecker.
check(env, task);
402template<storm::dd::DdType DdType,
typename ValueType>
409template<storm::dd::DdType DdType,
typename ValueType>
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.");
416 std::unique_ptr<storm::modelchecker::CheckResult> result;
417 ma->getManager().execute([&]() {
420 result = modelchecker.
check(env, task);
427template<storm::dd::DdType DdType,
typename ValueType>
434template<storm::dd::DdType DdType,
typename ValueType>
438 std::unique_ptr<storm::modelchecker::CheckResult> result;
448 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The model type " << model->getType() <<
" is not supported by the hybrid engine.");
453template<storm::dd::DdType DdType,
typename ValueType>
463template<storm::dd::DdType DdType,
typename ValueType>
467 if constexpr (storm::IsIntervalType<ValueType>) {
468 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Dd engine cannot verify DTMC with this data type.");
470 std::unique_ptr<storm::modelchecker::CheckResult> result;
471 dtmc->getManager().execute([&]() {
474 result = modelchecker.
check(env, task);
481template<storm::dd::DdType DdType,
typename ValueType>
488template<storm::dd::DdType DdType,
typename ValueType>
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.");
495 std::unique_ptr<storm::modelchecker::CheckResult> result;
496 mdp->getManager().execute([&]() {
499 result = modelchecker.
check(env, task);
506template<storm::dd::DdType DdType,
typename ValueType>
513template<storm::dd::DdType DdType,
typename ValueType>
517 std::unique_ptr<storm::modelchecker::CheckResult> result;
523 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"The model type " << model->getType() <<
" is not supported by the dd engine.");
528template<storm::dd::DdType DdType,
typename ValueType>
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.
This class represents a discrete-time Markov chain.
This class represents a Markov automaton.
This class represents a (discrete-time) Markov decision process.
Base class for all sparse models.
This class represents a stochastic multiplayer game.
This class represents a continuous-time Markov chain.
This class represents a discrete-time Markov chain.
This class represents a discrete-time Markov decision process.
This class represents a discrete-time Markov decision process.
Base class for all symbolic models.
ModelType getModelType() const
Retrieves the model type of the model.
storm::prism::Program const & asPrismProgram() const
bool isPrismProgram() const
#define STORM_LOG_WARN(message)
#define STORM_LOG_THROW(cond, exception, message)
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)