diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 3e5f916a5..b878a6a7a 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -18,6 +18,7 @@ #include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" @@ -25,6 +26,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Smg.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" @@ -251,6 +253,28 @@ namespace storm { return verifyWithSparseEngine(env, ma, task); } + template<typename ValueType> + typename std::enable_if<std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& smg, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { + std::unique_ptr<storm::modelchecker::CheckResult> result; + storm::modelchecker::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>> modelchecker(*smg); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(env, task); + } + return result; + } + + template<typename ValueType> + typename std::enable_if<!std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& mdp, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify SMGs with this data type."); + } + + template<typename ValueType> + std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& smg, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { + Environment env; + return verifyWithSparseEngine(env, smg, task); + } + + template<typename ValueType> std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) { std::unique_ptr<storm::modelchecker::CheckResult> result; @@ -262,6 +286,8 @@ namespace storm { result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Ctmc<ValueType>>(), task); } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), task); + } else if (model->getType() == storm::models::ModelType::Smg) { + result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Smg<ValueType>>(), task); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the sparse engine."); }