diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 5940e4ac3..92512f6e8 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -14,6 +14,7 @@ #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" +#include "storm/storage/jani/ArrayEliminator.h" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" @@ -45,6 +46,71 @@ namespace storm { namespace builder { + template + storm::jani::ModelFeatures DdJaniModelBuilder::getSupportedJaniFeatures() { + storm::jani::ModelFeatures features; + features.add(storm::jani::ModelFeature::DerivedOperators); + features.add(storm::jani::ModelFeature::StateExitRewards); + // We do not add Functions and arrays as these should ideally be substituted before creating this generator. + // This is because functions or arrays may also occur in properties and the user of this builder should take care of that. + return features; + } + + template + bool DdJaniModelBuilder::canHandle(storm::jani::Model const& model, boost::optional> const& properties) { + // Check jani features + auto features = model.getModelFeatures(); + features.remove(storm::jani::ModelFeature::Arrays); // can be substituted + features.remove(storm::jani::ModelFeature::DerivedOperators); + features.remove(storm::jani::ModelFeature::Functions); // can be substituted + features.remove(storm::jani::ModelFeature::StateExitRewards); + if (!features.empty()) { + STORM_LOG_INFO("Symbolic engine can not build Jani model due to unsupported jani features."); + return false; + } + // Check assignment levels + if (model.usesAssignmentLevels()) { + STORM_LOG_INFO("Symbolic engine can not build Jani model due to assignment levels."); + return false; + } + // Check nonTrivial reward expressions + if (properties) { + std::set rewardModels; + for (auto const& p : properties.get()) { + p.gatherReferencedRewardModels(rewardModels); + } + for (auto const& r : rewardModels) { + if (model.isNonTrivialRewardModelExpression(r)) { + STORM_LOG_INFO("Symbolic engine can not build Jani model due to non-trivial reward expressions."); + return false; + } + } + } else { + if (model.hasNonTrivialRewardExpression()) { + STORM_LOG_INFO("Symbolic engine can not build Jani model due to non-trivial reward expressions."); + return false; + } + } + // Check system composition + auto compositionInfo = storm::jani::CompositionInformationVisitor(model, model.getSystemComposition()).getInformation(); + + // Every automaton has to occur exactly once. + if (compositionInfo.getAutomatonToMultiplicityMap().size() == model.getNumberOfAutomata()) { + STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once."); + return false; + } + for (auto automatonMultiplicity : compositionInfo.getAutomatonToMultiplicityMap()) { + if (automatonMultiplicity.second > 1) { + STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once."); + return false; + } + } + + // There probably are more cases where the model is unsupported. However, checking these is often more involved. + // As this method is supposed to be a quick check, we just return true at this point. + return true; + } + template DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. @@ -2064,10 +2130,19 @@ namespace storm { auto features = model.getModelFeatures(); features.remove(storm::jani::ModelFeature::DerivedOperators); features.remove(storm::jani::ModelFeature::StateExitRewards); - STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The dd jani model builder does not support the following model feature(s): " << features.toString() << "."); storm::jani::Model preparedModel = model; - preparedModel.substituteFunctions(); + if (features.hasArrays()) { + STORM_LOG_ERROR("The jani model still considers arrays. These should have been eliminated before calling the dd builder. The arrays are eliminated now, but occurrences in properties will not be handled properly."); + preparedModel.eliminateArrays(); + features.remove(storm::jani::ModelFeature::Arrays); + } + if (features.hasFunctions()) { + STORM_LOG_ERROR("The jani model still considers functions. These should have been substituted before calling the dd builder. The functions are substituted now, but occurrences in properties will not be handled properly."); + preparedModel.substituteFunctions(); + features.remove(storm::jani::ModelFeature::Functions); + } + STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The dd jani model builder does not support the following model feature(s): " << features.toString() << "."); // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway). if (preparedModel.hasTransientEdgeDestinationAssignments()) { diff --git a/src/storm/builder/DdJaniModelBuilder.h b/src/storm/builder/DdJaniModelBuilder.h index 371b52557..59c6de409 100644 --- a/src/storm/builder/DdJaniModelBuilder.h +++ b/src/storm/builder/DdJaniModelBuilder.h @@ -3,6 +3,7 @@ #include #include "storm/storage/dd/DdType.h" +#include "storm/storage/jani/Property.h" #include "storm/logic/Formula.h" @@ -16,13 +17,27 @@ namespace storm { } namespace jani { class Model; + class ModelFeatures; } namespace builder { template class DdJaniModelBuilder { - public: + public: + + /*! + * Returns the jani features with which this builder can deal natively. + */ + static storm::jani::ModelFeatures getSupportedJaniFeatures(); + + /*! + * A quick check to detect whether the given model is not supported. + * This method only over-approximates the set of models that can be handled, i.e., if this + * returns true, the model might still be unsupported. + */ + static bool canHandle(storm::jani::Model const& model, boost::optional> const& properties = boost::none); + struct Options { /*! * Creates an object representing the default building options. diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 1a25bdaa2..e0f352216 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -539,6 +539,11 @@ namespace storm { typename DdPrismModelBuilder::GenerationInformation& generationInfo; }; + template + bool DdPrismModelBuilder::canHandle(storm::prism::Program const& program) { + return program.getModelType() != storm::prism::Program::ModelType::PTA; + } + template DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index fb357a6c8..1cf0e5692 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -31,6 +31,13 @@ namespace storm { template class DdPrismModelBuilder { public: + /*! + * A quick check to detect whether the given model is not supported. + * This method only over-approximates the set of models that can be handled, i.e., if this + * returns true, the model might still be unsupported. + */ + static bool canHandle(storm::prism::Program const& program); + struct Options { /*! * Creates an object representing the default building options. diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index eb1b397dc..374f86f73 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -53,6 +53,33 @@ namespace storm { #ifdef WINDOWS static const std::string DYLIB_EXTENSION = ".dll"; #endif + + template + storm::jani::ModelFeatures ExplicitJitJaniModelBuilder::getSupportedJaniFeatures() { + storm::jani::ModelFeatures features; + features.add(storm::jani::ModelFeature::DerivedOperators); + features.add(storm::jani::ModelFeature::StateExitRewards); + // We do not add Functions and arrays as these should ideally be substituted before creating this generator. + // This is because functions or arrays may also occur in properties and the user of this builder should take care of that. + return features; + } + + template + bool ExplicitJitJaniModelBuilder::canHandle(storm::jani::Model const& model) { + // Check jani features + auto features = model.getModelFeatures(); + features.remove(storm::jani::ModelFeature::Arrays); // can be substituted + features.remove(storm::jani::ModelFeature::DerivedOperators); + features.remove(storm::jani::ModelFeature::Functions); // can be substituted + features.remove(storm::jani::ModelFeature::StateExitRewards); + if (!features.empty()) { + STORM_LOG_INFO("Jit engine can not build Jani model due to unsupported jani features."); + return false; + } + // There probably are more cases where the model is unsupported. However, checking these is often more involved. + // As this method is supposed to be a quick check, we just return true at this point. + return true; + } template ExplicitJitJaniModelBuilder::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model.substituteConstantsFunctions()), modelComponentsBuilder(model.getModelType()) { diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index cb2247d35..5ccf4eec6 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -48,6 +48,18 @@ namespace storm { typedef JitModelBuilderInterface* (CreateFunctionType)(ModelComponentsBuilder& modelComponentsBuilder); typedef boost::function ImportCreateFunctionType; + /*! + * Returns the jani features with which this builder can deal natively. + */ + static storm::jani::ModelFeatures getSupportedJaniFeatures(); + + /*! + * A quick check to detect whether the given model is not supported. + * This method only over-approximates the set of models that can be handled, i.e., if this + * returns true, the model might still be unsupported. + */ + static bool canHandle(storm::jani::Model const& model); + /*! * Creates a model builder for the given model. The provided options are used to determine which part of * the model is built. diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f2b05f74d..606c420bc 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -115,6 +115,33 @@ namespace storm { } } } + + template + storm::jani::ModelFeatures JaniNextStateGenerator::getSupportedJaniFeatures() { + storm::jani::ModelFeatures features; + features.add(storm::jani::ModelFeature::DerivedOperators); + features.add(storm::jani::ModelFeature::StateExitRewards); + features.add(storm::jani::ModelFeature::Arrays); + // We do not add Functions as these should ideally be substituted before creating this generator. + // This is because functions may also occur in properties and the user of this class should take care of that. + return features; + } + + template + bool JaniNextStateGenerator::canHandle(storm::jani::Model const& model) { + auto features = model.getModelFeatures(); + features.remove(storm::jani::ModelFeature::Arrays); + features.remove(storm::jani::ModelFeature::DerivedOperators); + features.remove(storm::jani::ModelFeature::Functions); // can be substituted + features.remove(storm::jani::ModelFeature::StateExitRewards); + if (!features.empty()) { + return false; + } + // There probably are more cases where the model is unsupported. However, checking these is more involved. + // As this method is supposed to be a quick check, we just return true at this point. + return true; + } + template ModelType JaniNextStateGenerator::getModelType() const { diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 790395faf..68a456cf8 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -32,6 +32,18 @@ namespace storm { JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); + /*! + * Returns the jani features with which this builder can deal natively. + */ + static storm::jani::ModelFeatures getSupportedJaniFeatures(); + + /*! + * A quick check to detect whether the given model is not supported. + * This method only over-approximates the set of models that can be handled, i.e., if this + * returns true, the model might still be unsupported. + */ + static bool canHandle(storm::jani::Model const& model); + virtual ModelType getModelType() const override; virtual bool isDeterministicModel() const override; virtual bool isDiscreteTimeModel() const override; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 68fda0abd..30e55f5bd 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -82,6 +82,12 @@ namespace storm { } } + template + bool PrismNextStateGenerator::canHandle(storm::prism::Program const& program) { + // We can handle all valid prism programs (except for PTAs) + return program.getModelType() != storm::prism::Program::ModelType::PTA; + } + template void PrismNextStateGenerator::checkValid() const { // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 2b9fdc678..b2eb1b555 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -24,7 +24,14 @@ namespace storm { enum class CommandFilter {All, Markovian, Probabilistic}; PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); - + + /*! + * A quick check to detect whether the given model is not supported. + * This method only over-approximates the set of models that can be handled, i.e., if this + * returns true, the model might still be unsupported. + */ + static bool canHandle(storm::prism::Program const& program); + virtual ModelType getModelType() const override; virtual bool isDeterministicModel() const override; virtual bool isDiscreteTimeModel() const override; diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index d24b3a3fe..add01f24d 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -114,6 +114,11 @@ namespace storm { return res; } + void Property::gatherReferencedRewardModels(std::set& rewardModelNames) const { + getFilter().getFormula()->gatherReferencedRewardModels(rewardModelNames); + getFilter().getStatesFormula()->gatherReferencedRewardModels(rewardModelNames); + } + std::ostream& operator<<(std::ostream& os, Property const& p) { return os << "(" << p.getName() << "): " << p.getFilter(); } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 199dbe19f..757db04a8 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -137,6 +137,7 @@ namespace storm { bool containsUndefinedConstants() const; std::set getUsedVariablesAndConstants() const; std::set getUsedLabels() const; + void gatherReferencedRewardModels(std::set& rewardModelNames) const; std::shared_ptr getRawFormula() const;