diff --git a/src/storm/builder/BuilderType.cpp b/src/storm/builder/BuilderType.cpp index 72e106011..6bc7e766a 100644 --- a/src/storm/builder/BuilderType.cpp +++ b/src/storm/builder/BuilderType.cpp @@ -1,23 +1,66 @@ #include "storm/builder/BuilderType.h" +#include "storm/storage/dd/DdType.h" + #include "storm/storage/jani/ModelFeatures.h" +#include "storm/generator/JaniNextStateGenerator.h" +#include "storm/generator/PrismNextStateGenerator.h" +#include "storm/builder/DdJaniModelBuilder.h" +#include "storm/builder/DdPrismModelBuilder.h" +#include "storm/builder/jit/ExplicitJitJaniModelBuilder.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/UnexpectedException.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); + // The supported jani features should be independent of the ValueType and Dd type. We just take sylvan and double for all. + storm::dd::DdType const ddType = storm::dd::DdType::Sylvan; + typedef double ValueType; + switch (builderType) { + case BuilderType::Explicit: + return storm::generator::JaniNextStateGenerator::getSupportedJaniFeatures(); + case BuilderType::Dd: + return storm::builder::DdJaniModelBuilder::getSupportedJaniFeatures(); + case BuilderType::Jit: + return storm::builder::jit::ExplicitJitJaniModelBuilder::getSupportedJaniFeatures(); + } - return features; + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected builder type."); } + template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) { - return true; + 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. + return true; + } + STORM_LOG_THROW(modelDescription.isPrismProgram() || modelDescription.isJaniModel(), storm::exceptions::UnexpectedException, "The model is neither PRISM nor Jani which is not expected."); + switch (builderType) { + case BuilderType::Explicit: + if (modelDescription.isPrismProgram()) { + return storm::generator::PrismNextStateGenerator::canHandle(modelDescription.asPrismProgram()); + } else { + return storm::generator::JaniNextStateGenerator::canHandle(modelDescription.asJaniModel()); + } + case BuilderType::Dd: + if (modelDescription.isPrismProgram()) { + return storm::builder::DdPrismModelBuilder::canHandle(modelDescription.asPrismProgram()); + } else { + return storm::builder::DdJaniModelBuilder::canHandle(modelDescription.asJaniModel()); + } + case BuilderType::Jit: + return storm::builder::jit::ExplicitJitJaniModelBuilder::canHandle(modelDescription.asJaniModel()); + } } + + + template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription); + template bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription); + } } \ No newline at end of file diff --git a/src/storm/builder/BuilderType.h b/src/storm/builder/BuilderType.h index 297596ce1..a5732a950 100644 --- a/src/storm/builder/BuilderType.h +++ b/src/storm/builder/BuilderType.h @@ -16,6 +16,7 @@ namespace storm { storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType); + template 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 4441d9a07..a2b315822 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -152,7 +152,7 @@ namespace storm { 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); } // explicit template instantiations.