diff --git a/src/utility/storm.h b/src/utility/storm.h index 19f84b85d..49518170b 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -171,6 +171,28 @@ namespace storm { } #endif + template + std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula) { + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); + switch(settings.getEngine()) { + case storm::settings::modules::GeneralSettings::Engine::Sparse: { + std::shared_ptr> sparseModel = model->template as>(); + STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); + return verifySparseModel(sparseModel, formula); + } + case storm::settings::modules::GeneralSettings::Engine::Hybrid: { + std::shared_ptr> ddModel = model->template as>(); + STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model"); + return verifySymbolicModelWithHybridEngine(ddModel, formula); + } + case storm::settings::modules::GeneralSettings::Engine::Dd: { + std::shared_ptr> ddModel = model->template as>(); + STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model"); + return verifySymbolicModelWithDdEngine(ddModel, formula); + } + } + } + template std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) {