diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 23d3650b0..16bf04056 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/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 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"); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 9a741da86..3da43c78b 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/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& 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(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& 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 const& formulas, storm::jani::Model const& model) { std::vector 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; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 334e804ca..ce95a2c0f 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/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& 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 featureVector(modelFeatures.begin(), modelFeatures.end()); - jsonStruct["features"] = featureVector; + jsonStruct["features"] = modelFeatures.toString(); return jsonStruct; } modernjson::json jsonStruct; - std::set modelFeatures; + storm::jani::ModelFeatures modelFeatures; }; } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 6ff5cd28a..c326e7314 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/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; } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 937f58f42..3224c0353 100644 --- a/src/storm/storage/jani/Model.h +++ b/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 expressionManager; diff --git a/src/storm/storage/jani/ModelFeatures.cpp b/src/storm/storage/jani/ModelFeatures.cpp new file mode 100644 index 000000000..755ac99d8 --- /dev/null +++ b/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); + } + + } +} diff --git a/src/storm/storage/jani/ModelFeatures.h b/src/storm/storage/jani/ModelFeatures.h new file mode 100644 index 000000000..f2604af96 --- /dev/null +++ b/src/storm/storage/jani/ModelFeatures.h @@ -0,0 +1,29 @@ +#pragma once + +#include +#include + +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 features; + }; + } +}