From 4da25662f8975a74a962d136e82cb08a274d0bc6 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 18 Feb 2020 10:22:27 +0100 Subject: [PATCH] Engine: check whether an engine can handle the query given by a model and a *list* of properties --- src/storm/builder/BuilderType.cpp | 9 ++-- src/storm/builder/BuilderType.h | 6 ++- src/storm/utility/Engine.cpp | 72 +++++++++++++++++++++++++++---- src/storm/utility/Engine.h | 8 +++- 4 files changed, 79 insertions(+), 16 deletions(-) diff --git a/src/storm/builder/BuilderType.cpp b/src/storm/builder/BuilderType.cpp index 6bc7e766a..35512a220 100644 --- a/src/storm/builder/BuilderType.cpp +++ b/src/storm/builder/BuilderType.cpp @@ -32,7 +32,7 @@ namespace storm { } template - bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) { + bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& properties) { storm::dd::DdType const ddType = storm::dd::DdType::Sylvan; if (!modelDescription.hasModel()) { // If there is no model to be build, we assume that the task of obtaining a model is either not required or can be accomplished somehow. @@ -50,7 +50,7 @@ namespace storm { if (modelDescription.isPrismProgram()) { return storm::builder::DdPrismModelBuilder::canHandle(modelDescription.asPrismProgram()); } else { - return storm::builder::DdJaniModelBuilder::canHandle(modelDescription.asJaniModel()); + return storm::builder::DdJaniModelBuilder::canHandle(modelDescription.asJaniModel(), properties); } case BuilderType::Jit: return storm::builder::jit::ExplicitJitJaniModelBuilder::canHandle(modelDescription.asJaniModel()); @@ -59,8 +59,9 @@ namespace storm { - template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription); - template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription); + template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& properties); + template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& properties); + template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& properties); } } \ No newline at end of file diff --git a/src/storm/builder/BuilderType.h b/src/storm/builder/BuilderType.h index a5732a950..22b08158c 100644 --- a/src/storm/builder/BuilderType.h +++ b/src/storm/builder/BuilderType.h @@ -1,5 +1,9 @@ #pragma once +#include +#include + +#include "storm/storage/jani/Property.h" #include "storm/storage/SymbolicModelDescription.h" namespace storm { @@ -17,6 +21,6 @@ namespace storm { storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType); template - bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription); + bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& properties = boost::none); } } \ No newline at end of file diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index a2b315822..345dc6a8e 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -14,6 +14,7 @@ #include "storm/modelchecker/CheckTask.h" #include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/jani/Property.h" #include "storm/utility/macros.h" @@ -144,21 +145,74 @@ namespace storm { return false; } + 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::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: + return storm::modelchecker::SparseDtmcPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::CTMC: + return storm::modelchecker::SparseCtmcCslModelChecker>::canHandleStatic(checkTask); + case ModelType::MDP: + case ModelType::MA: + case ModelType::POMDP: + return false; + } + case Engine::Hybrid: + switch (modelType) { + case ModelType::DTMC: + return storm::modelchecker::HybridDtmcPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::CTMC: + return storm::modelchecker::HybridCtmcCslModelChecker>::canHandleStatic(checkTask); + case ModelType::MDP: + case ModelType::MA: + case ModelType::POMDP: + return false; + } + case Engine::Dd: + switch (modelType) { + case ModelType::DTMC: + return storm::modelchecker::SymbolicDtmcPrctlModelChecker>::canHandleStatic(checkTask); + case ModelType::MDP: + case ModelType::CTMC: + case ModelType::MA: + case ModelType::POMDP: + return false; + } + default: + STORM_LOG_ERROR("The selected engine" << engine << " is not considered."); + } + 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 - 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; + bool canHandle(storm::utility::Engine const& engine, std::vector const& properties, storm::storage::SymbolicModelDescription const& modelDescription) { + // Check handability of properties based on model type + for (auto const& p : properties) { + for (auto const& f : {p.getRawFormula(), p.getFilter().getStatesFormula()}) { + auto task = storm::modelchecker::CheckTask(*f, true); + if (!canHandle(engine, modelDescription.getModelType(), task)) { + STORM_LOG_INFO("Engine " << engine << " can not handle formula '" << *f << "'."); + return false; + } + } } // Check whether the model builder can handle the model description - return storm::builder::canHandle(getBuilderType(engine), modelDescription); + return storm::builder::canHandle(getBuilderType(engine), modelDescription, properties); } // 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&); - - + template bool canHandle(storm::utility::Engine const&, std::vector const&, storm::storage::SymbolicModelDescription const&); + template bool canHandle(storm::utility::Engine const&, std::vector const&, storm::storage::SymbolicModelDescription const&); + template bool canHandle(storm::utility::Engine const&, std::vector const&, storm::storage::SymbolicModelDescription const&); + } } \ No newline at end of file diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h index dff20c8e6..3254749a9 100644 --- a/src/storm/utility/Engine.h +++ b/src/storm/utility/Engine.h @@ -10,6 +10,10 @@ namespace storm { // Forward Declarations + namespace jani { + class Property; + } + namespace logic { class Formula; } @@ -56,12 +60,12 @@ namespace storm { storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine); /*! - * Returns false if the given model description and checkTask can certainly not be handled by the given engine. + * Returns false if the given model description and one of the given properties 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::modelchecker::CheckTask const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription); + bool canHandle(storm::utility::Engine const& engine, std::vector const& properties, storm::storage::SymbolicModelDescription const& modelDescription); } } \ No newline at end of file