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<storm::dd::DdType LibraryType, typename ValueType>
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 <storm::dd::DdType ddType, typename ValueType>
- bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
+ template <typename ValueType>
+ bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> 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<storm::models::sparse::Dtmc<ValueType>>::canHandleStatic(checkTask);
- case ModelType::Mdp:
+ case ModelType::MDP:
return storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>>::canHandleStatic(checkTask);
- case ModelType::Ctmc:
+ case ModelType::CTMC:
return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>>::canHandleStatic(checkTask);
- case ModelType::MarkovAutomaton:
+ case ModelType::MA:
return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::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<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
- case ModelType::Mdp:
+ case ModelType::MDP:
return storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
- case ModelType::Ctmc:
+ case ModelType::CTMC:
return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, ValueType>>::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<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
- case ModelType::Mdp:
+ case ModelType::MDP:
return storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::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 <storm::dd::DdType ddType, typename ValueType>
+ template <typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription const& modelDescription, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> 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<double>(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, double> const&);
+ template bool canHandle<storm::RationalNumber>(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber> 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 <storm::dd::DdType ddType, typename ValueType>
- bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> 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 <storm::dd::DdType ddType, typename ValueType>
+ template <typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription);
}
}
\ No newline at end of file