From ac35a04eecb0eb4b7312d93103506975bf37f81b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 17 Feb 2020 12:01:24 +0100 Subject: [PATCH] utility/engine: canHandle(...) compiles now. Moved getSupportedJaniFeatures to builder/BuilderType. --- src/storm/api/builder.h | 8 +--- src/storm/builder/BuilderType.cpp | 23 +++++++++++ src/storm/builder/BuilderType.h | 10 +++++ src/storm/utility/Engine.cpp | 63 ++++++++++++++----------------- src/storm/utility/Engine.h | 11 +----- 5 files changed, 64 insertions(+), 51 deletions(-) create mode 100644 src/storm/builder/BuilderType.cpp diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 0df66c7ff..a7f7ea52f 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -33,13 +33,7 @@ namespace storm { namespace api { inline storm::jani::ModelFeatures getSupportedJaniFeatures(storm::builder::BuilderType const& builderType) { - storm::jani::ModelFeatures features; - features.add(storm::jani::ModelFeature::DerivedOperators); - features.add(storm::jani::ModelFeature::StateExitRewards); - if (builderType == storm::builder::BuilderType::Explicit) { - features.add(storm::jani::ModelFeature::Arrays); - } - return features; + return storm::builder::getSupportedJaniFeatures(builderType); } template diff --git a/src/storm/builder/BuilderType.cpp b/src/storm/builder/BuilderType.cpp new file mode 100644 index 000000000..72e106011 --- /dev/null +++ b/src/storm/builder/BuilderType.cpp @@ -0,0 +1,23 @@ +#include "storm/builder/BuilderType.h" + +#include "storm/storage/jani/ModelFeatures.h" + +namespace storm { + namespace builder { + + storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType) { + storm::jani::ModelFeatures features; + features.add(storm::jani::ModelFeature::DerivedOperators); + features.add(storm::jani::ModelFeature::StateExitRewards); + if (builderType == BuilderType::Explicit) { + features.add(storm::jani::ModelFeature::Arrays); + } + return features; + } + + bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) { + return true; + } + + } +} \ No newline at end of file diff --git a/src/storm/builder/BuilderType.h b/src/storm/builder/BuilderType.h index 8e5e86ad0..297596ce1 100644 --- a/src/storm/builder/BuilderType.h +++ b/src/storm/builder/BuilderType.h @@ -1,11 +1,21 @@ #pragma once +#include "storm/storage/SymbolicModelDescription.h" + namespace storm { + namespace jani { + class ModelFeatures; + } + namespace builder { enum class BuilderType { Explicit, Dd, Jit }; + + storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType); + + bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription); } } \ No newline at end of file diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 52b59f610..4441d9a07 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -1,9 +1,5 @@ #include "storm/utility/Engine.h" -#include "storm/utility/macros.h" - -#include "storm/models/ModelType.h" - #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" @@ -96,74 +92,73 @@ namespace storm { } } - template - bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask const& checkTask) { + template + bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType, storm::modelchecker::CheckTask const& checkTask) { // Define types to improve readability - typedef storm::models::ModelType ModelType; -#ifdef TODO_IMPLEMENT_CAN_HANDLE_STATIC + typedef storm::storage::SymbolicModelDescription::ModelType ModelType; + // The Dd library does not make much of a difference (in case of exact or parametric models we will switch to sylvan anyway). + // Therefore, we always use sylvan here + storm::dd::DdType const ddType = storm::dd::DdType::Sylvan; switch (engine) { case Engine::Sparse: case Engine::DdSparse: switch (modelType) { - case ModelType::Dtmc: + case ModelType::DTMC: return storm::modelchecker::SparseDtmcPrctlModelChecker>::canHandleStatic(checkTask); - case ModelType::Mdp: + case ModelType::MDP: return storm::modelchecker::SparseMdpPrctlModelChecker>::canHandleStatic(checkTask); - case ModelType::Ctmc: + case ModelType::CTMC: return storm::modelchecker::SparseCtmcCslModelChecker>::canHandleStatic(checkTask); - case ModelType::MarkovAutomaton: + case ModelType::MA: return storm::modelchecker::SparseMarkovAutomatonCslModelChecker>::canHandleStatic(checkTask); - case ModelType::S2pg: - case ModelType::Pomdp: + case ModelType::POMDP: return false; } - break; case Engine::Hybrid: switch (modelType) { - case ModelType::Dtmc: + case ModelType::DTMC: return storm::modelchecker::HybridDtmcPrctlModelChecker>::canHandleStatic(checkTask); - case ModelType::Mdp: + case ModelType::MDP: return storm::modelchecker::HybridMdpPrctlModelChecker>::canHandleStatic(checkTask); - case ModelType::Ctmc: + case ModelType::CTMC: return storm::modelchecker::HybridCtmcCslModelChecker>::canHandleStatic(checkTask); - case ModelType::MarkovAutomaton: - case ModelType::S2pg: - case ModelType::Pomdp: + case ModelType::MA: + case ModelType::POMDP: return false; } - break; case Engine::Dd: switch (modelType) { - case ModelType::Dtmc: + case ModelType::DTMC: return storm::modelchecker::SymbolicDtmcPrctlModelChecker>::canHandleStatic(checkTask); - case ModelType::Mdp: + case ModelType::MDP: return storm::modelchecker::SymbolicMdpPrctlModelChecker>::canHandleStatic(checkTask); - case ModelType::Ctmc: - case ModelType::MarkovAutomaton: - case ModelType::S2pg: - case ModelType::Pomdp: + case ModelType::CTMC: + case ModelType::MA: + case ModelType::POMDP: return false; } - break; default: STORM_LOG_ERROR("The selected engine" << engine << " is not considered."); } -#endif STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType << ") does not seem to be supported for this value type."); return false; } + - template + template bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription const& modelDescription, storm::modelchecker::CheckTask const& checkTask) { // Check handability based on model type if (!canHandle(engine, modelDescription.getModelType(), checkTask)) { return false; } - // TODO - return true; + // Check whether the model builder can handle the model description + return storm::builder::canHandle(getBuilderType(engine), modelDescription); } - + // explicit template instantiations. + template bool canHandle(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&); + template bool canHandle(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&); + } } \ No newline at end of file diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h index 2c43047e5..dff20c8e6 100644 --- a/src/storm/utility/Engine.h +++ b/src/storm/utility/Engine.h @@ -55,22 +55,13 @@ namespace storm { */ storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine); - /*! - * Returns false if the given model type and checkTask can certainly not be handled by the given engine. - * Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true, - * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need - * to actually build the model in order to decide whether it is supported. - */ - template - bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask const& checkTask); - /*! * Returns false if the given model description and checkTask can certainly not be handled by the given engine. * Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true, * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need * to actually build the model in order to decide whether it is supported. */ - template + template bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription); } } \ No newline at end of file