properly implemented model features

src/storm-parsers/parser/JaniParser.cpp

@@ -95,10 +95,17 @@ namespace storm {
             size_t featuresCount = parsedStructure.count("features");
             STORM_LOG_THROW(featuresCount < 2, storm::exceptions::InvalidJaniException, "features-declarations can be given at most once.");
             if (featuresCount == 1) {
-                std::unordered_set<std::string> supportedFeatures = {"derived-operators", "state-exit-rewards"};
                 for (auto const& feature : parsedStructure.at("features")) {
 					std::string featureStr = getString(feature, "Model feature");
-                    STORM_LOG_WARN_COND(supportedFeatures.find(featureStr) != supportedFeatures.end(), "Storm does not support the model feature " << featureStr << ".");
+                    if (featureStr == "arrays") {
+                        model.getModelFeatures().add(storm::jani::ModelFeature::Arrays);
+                    } else if (featureStr == "derived-operators") {
+                        model.getModelFeatures().add(storm::jani::ModelFeature::DerivedOperators);
+                    } else if (featureStr == "state-exit-rewards") {
+                        model.getModelFeatures().add(storm::jani::ModelFeature::StateExitRewards);
+                    } else {
+                        STORM_LOG_WARN("Storm does not support the model feature " << featureStr << ".");
+                    }
                 }
             }
             size_t actionCount = parsedStructure.count("actions");

src/storm/storage/jani/JSONExporter.cpp

@@ -196,11 +196,11 @@ namespace storm {
             }
         }
         
-        modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, std::set<std::string>& modelFeatures) {
+        modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
             FormulaToJaniJson translator(model);
             auto result = boost::any_cast<modernjson::json>(formula.accept(translator));
             if (translator.containsStateExitRewards()) {
-                modelFeatures.insert("state-exit-rewards");
+                modelFeatures.add(storm::jani::ModelFeature::StateExitRewards);
             }
             return result;
         }
@@ -971,7 +971,7 @@ namespace storm {
         }
         
         void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) {
-            modelFeatures = {"derived-operators"};
+            modelFeatures = janiModel.getModelFeatures();
             jsonStruct["jani-version"] = janiModel.getJaniVersion();
             jsonStruct["name"] = janiModel.getName();
             jsonStruct["type"] = to_string(janiModel.getModelType());
@@ -1011,7 +1011,7 @@ namespace storm {
             }
         }
         
-        modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, std::set<std::string>& modelFeatures) {
+        modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures) {
             modernjson::json propDecl;
             propDecl["states"]["op"] = "initial";
             propDecl["op"] = "filter";
@@ -1023,6 +1023,10 @@ namespace storm {
         
         void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) {
             std::vector<modernjson::json> properties;
+            
+            // Unset model-features that only relate to properties. These are only set if such properties actually exist.
+            modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards);
+            
             uint64_t index = 0;
             for(auto const& f : formulas) {
                 modernjson::json propDecl;

src/storm/storage/jani/JSONExporter.h

@@ -46,7 +46,7 @@ namespace storm {
         class FormulaToJaniJson : public storm::logic::FormulaVisitor {
             
         public:
-            static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& model, std::set<std::string>& modelFeatures);
+            static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& model, storm::jani::ModelFeatures& modelFeatures);
             bool containsStateExitRewards() const; // Returns true iff the  previously translated formula contained state exit rewards
             virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
@@ -96,13 +96,12 @@ namespace storm {
             void appendVariableDeclaration(storm::jani::Variable const& variable);
             
             modernjson::json finalize() {
-                std::vector<std::string> featureVector(modelFeatures.begin(), modelFeatures.end());
-                jsonStruct["features"] = featureVector;
+                jsonStruct["features"] = modelFeatures.toString();
                 return jsonStruct;
             }
             
             modernjson::json jsonStruct;
-            std::set<std::string> modelFeatures;
+            storm::jani::ModelFeatures modelFeatures;
             
         };
     }

src/storm/storage/jani/Model.cpp

@@ -114,6 +114,14 @@ namespace storm {
             return modelType;
         }
         
+        ModelFeatures const& Model::getModelFeatures() const {
+            return modelFeatures;
+        }
+        
+        ModelFeatures& Model::getModelFeatures() {
+            return modelFeatures;
+        }
+        
         std::string const& Model::getName() const {
             return name;
         }

src/storm/storage/jani/Model.h

@@ -14,6 +14,7 @@
 #include "storm/storage/jani/Edge.h"
 #include "storm/storage/jani/Location.h"
 #include "storm/storage/jani/TemplateEdge.h"
+#include "storm/storage/jani/ModelFeatures.h"
 
 #include "storm/utility/solver.h"
 #include "storm/utility/vector.h"
@@ -77,6 +78,16 @@ namespace storm {
              */
             ModelType const& getModelType() const;
             
+            /*!
+             * Retrieves the enabled model features
+             */
+            ModelFeatures const& getModelFeatures() const;
+            
+            /*!
+             * Retrieves the enabled model features
+             */
+            ModelFeatures& getModelFeatures();
+            
             /*!
              * Retrieves the name of the model.
              */
@@ -523,6 +534,9 @@ namespace storm {
             /// The JANI-version used to specify the model.
             uint64_t version;
             
+            /// The features enabled for this model.
+            ModelFeatures modelFeatures;
+            
             /// The manager responsible for the expressions in this model.
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
             

src/storm/storage/jani/ModelFeatures.cpp

@@ -0,0 +1,56 @@
+#include "storm/storage/jani/ModelFeatures.h"
+
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace jani {
+
+        std::string toString(ModelFeature const& modelFeature) {
+            switch(modelFeature) {
+                case ModelFeature::Arrays:
+                    return "arrays";
+                case ModelFeature::DerivedOperators:
+                    return "derived-operators";
+                case ModelFeature::StateExitRewards:
+                    return "state-exit-rewards";
+            }
+            STORM_LOG_ASSERT(false, "Unhandled model feature");
+            return "Unhandled-feature";
+        }
+        
+        std::string ModelFeatures::toString() const {
+            std::string res = "[";
+            bool first = true;
+            for (auto const& f : features) {
+                if (!first) {
+                    res += ", ";
+                }
+                res += storm::jani::toString(f);
+                first = false;
+            }
+            res += "]";
+            return res;
+        }
+        
+        bool ModelFeatures::hasArrays() const {
+            return features.count(ModelFeature::Arrays) > 0;
+        }
+        
+        bool ModelFeatures::hasDerivedOperators() const {
+            return features.count(ModelFeature::DerivedOperators) > 0;
+        }
+        
+        bool ModelFeatures::hasStateExitRewards() const {
+            return features.count(ModelFeature::StateExitRewards) > 0;
+        }
+        
+        void ModelFeatures::add(ModelFeature const& modelFeature) {
+            features.insert(modelFeature);
+        }
+        
+        void ModelFeatures::remove(ModelFeature const& modelFeature) {
+            features.erase(modelFeature);
+        }
+        
+    }
+}

src/storm/storage/jani/ModelFeatures.h

@@ -0,0 +1,29 @@
+#pragma once
+
+#include <string>
+#include <set>
+
+namespace storm {
+    namespace jani {
+
+        enum class ModelFeature {Arrays, DerivedOperators, StateExitRewards};
+
+        std::string toString(ModelFeature const& modelFeature);
+        
+        class ModelFeatures {
+        
+        public:
+            std::string toString() const;
+            
+            bool hasArrays() const;
+            bool hasDerivedOperators() const;
+            bool hasStateExitRewards() const;
+            
+            void add(ModelFeature const& modelFeature);
+            void remove(ModelFeature const& modelFeature);
+
+        private:
+            std::set<ModelFeature> features;
+        };
+    }
+}