all model builders: Added a canHandle method and a getSupportedJaniFeatures method.

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::dd::DdType Type, typename ValueType>
+        storm::jani::ModelFeatures DdJaniModelBuilder<Type, ValueType>::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 <storm::dd::DdType Type, typename ValueType>
+        bool DdJaniModelBuilder<Type, ValueType>::canHandle(storm::jani::Model const& model, boost::optional<std::vector<storm::jani::Property>> 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<std::string> 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 <storm::dd::DdType Type, typename ValueType>
         DdJaniModelBuilder<Type, ValueType>::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()) {

src/storm/builder/DdJaniModelBuilder.h

@@ -3,6 +3,7 @@
 #include <boost/optional.hpp>
 
 #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 <storm::dd::DdType Type, typename ValueType = double>
         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<std::vector<storm::jani::Property>> const& properties = boost::none);
+            
             struct Options {
                 /*!
                  * Creates an object representing the default building options.

src/storm/builder/DdPrismModelBuilder.cpp

@@ -539,6 +539,11 @@ namespace storm {
             typename DdPrismModelBuilder<Type, ValueType>::GenerationInformation& generationInfo;
         };
         
+        template <storm::dd::DdType Type, typename ValueType>
+        bool DdPrismModelBuilder<Type, ValueType>::canHandle(storm::prism::Program const& program) {
+            return program.getModelType() != storm::prism::Program::ModelType::PTA;
+        }
+        
         template <storm::dd::DdType Type, typename ValueType>
         DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.

src/storm/builder/DdPrismModelBuilder.h

@@ -31,6 +31,13 @@ namespace storm {
         template <storm::dd::DdType Type, typename ValueType = double>
         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.

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -53,6 +53,33 @@ namespace storm {
 #ifdef WINDOWS
             static const std::string DYLIB_EXTENSION = ".dll";
 #endif
+      
+            template <typename ValueType, typename RewardModelType>
+            storm::jani::ModelFeatures ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>
+            bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>
             ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model.substituteConstantsFunctions()), modelComponentsBuilder(model.getModelType()) {

src/storm/builder/jit/ExplicitJitJaniModelBuilder.h

@@ -48,6 +48,18 @@ namespace storm {
                 typedef JitModelBuilderInterface<IndexType, ValueType>* (CreateFunctionType)(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder);
                 typedef boost::function<CreateFunctionType> 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.

src/storm/generator/JaniNextStateGenerator.cpp

@@ -115,6 +115,33 @@ namespace storm {
                 }
             }
         }
+
+        template<typename ValueType, typename StateType>
+        storm::jani::ModelFeatures JaniNextStateGenerator<ValueType, StateType>::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<typename ValueType, typename StateType>
+        bool JaniNextStateGenerator<ValueType, StateType>::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<typename ValueType, typename StateType>
         ModelType JaniNextStateGenerator<ValueType, StateType>::getModelType() const {

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;

src/storm/generator/PrismNextStateGenerator.cpp

@@ -82,6 +82,12 @@ namespace storm {
             }
         }
 
+        template<typename ValueType, typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::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<typename ValueType, typename StateType>
         void PrismNextStateGenerator<ValueType, StateType>::checkValid() const {
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.

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;

src/storm/storage/jani/Property.cpp

@@ -114,6 +114,11 @@ namespace storm {
             return res;
         }
         
+        void Property::gatherReferencedRewardModels(std::set<std::string>& 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();
         }

src/storm/storage/jani/Property.h

@@ -137,6 +137,7 @@ namespace storm {
             bool containsUndefinedConstants() const;
             std::set<storm::expressions::Variable> getUsedVariablesAndConstants() const;
             std::set<std::string> getUsedLabels() const;
+            void gatherReferencedRewardModels(std::set<std::string>& rewardModelNames) const;
             
             std::shared_ptr<storm::logic::Formula const> getRawFormula() const;