diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 78e9c20a3..697f3bcbe 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -9,14 +9,15 @@ #include "storm/storage/jani/Property.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" +#include "storm/storage/jani/ModelType.h" #include "storm/storage/jani/CompositionInformationVisitor.h" #include "storm/storage/jani/expressions/JaniExpressions.h" +#include "storm/logic/RewardAccumulationEliminationVisitor.h" + #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/InvalidJaniException.h" - #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/NotImplementedException.h" -#include "storm/storage/jani/ModelType.h" #include "storm/modelchecker/results/FilterType.h" @@ -100,19 +101,18 @@ 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) { + auto allKnownModelFeatures = storm::jani::getAllKnownModelFeatures(); for (auto const& feature : parsedStructure.at("features")) { std::string featureStr = getString(feature, "Model feature"); - 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 == "functions") { - model.getModelFeatures().add(storm::jani::ModelFeature::Functions); - } 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 << "."); + bool found = false; + for (auto const& knownFeature : allKnownModelFeatures.asSet()) { + if (featureStr == storm::jani::toString(knownFeature)) { + model.getModelFeatures().add(knownFeature); + found = true; + break; + } } + STORM_LOG_THROW(found, storm::exceptions::NotSupportedException, "Storm does not support the model feature " << featureStr); } } size_t actionCount = parsedStructure.count("actions"); diff --git a/src/storm/storage/jani/ModelFeatures.cpp b/src/storm/storage/jani/ModelFeatures.cpp index 8ea1c769b..5a3aa9794 100644 --- a/src/storm/storage/jani/ModelFeatures.cpp +++ b/src/storm/storage/jani/ModelFeatures.cpp @@ -50,17 +50,25 @@ namespace storm { return features.count(ModelFeature::StateExitRewards) > 0; } + std::set const& ModelFeatures::asSet() const { + return features; + } + bool ModelFeatures::empty() const { return features.empty(); } - void ModelFeatures::add(ModelFeature const& modelFeature) { + ModelFeatures& ModelFeatures::add(ModelFeature const& modelFeature) { features.insert(modelFeature); + return *this; } void ModelFeatures::remove(ModelFeature const& modelFeature) { features.erase(modelFeature); } + ModelFeatures getAllKnownModelFeatures() { + return ModelFeatures().add(ModelFeature::Arrays).add(ModelFeature::DerivedOperators).add(ModelFeature::Functions).add(ModelFeature::StateExitRewards); + } } } diff --git a/src/storm/storage/jani/ModelFeatures.h b/src/storm/storage/jani/ModelFeatures.h index 32b4d3db3..f07477202 100644 --- a/src/storm/storage/jani/ModelFeatures.h +++ b/src/storm/storage/jani/ModelFeatures.h @@ -22,12 +22,16 @@ namespace storm { // Returns true, if no model feature is enabled. bool empty() const; + std::set const& asSet() const; - void add(ModelFeature const& modelFeature); + ModelFeatures& add(ModelFeature const& modelFeature); void remove(ModelFeature const& modelFeature); private: std::set features; }; + + ModelFeatures getAllKnownModelFeatures(); + } }