From c3e390c59a0e7e1d14dfe8cd18634baf7fc41643 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 9 Sep 2015 14:20:23 +0200 Subject: [PATCH] extended api with an option to verify model according to given engine Former-commit-id: b2163590a539df3f038d203094fcb22a92db96f3 --- src/utility/storm.h | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) 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<typename ValueType, storm::dd::DdType DdType> + std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<storm::logic::Formula> const& formula) { + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); + switch(settings.getEngine()) { + case storm::settings::modules::GeneralSettings::Engine::Sparse: { + std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); + 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<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>(); + 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<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>(); + STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model"); + return verifySymbolicModelWithDdEngine(ddModel, formula); + } + } + } + template<typename ValueType> std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {