From e85b9759e2eeb3bb55ac5de43af1d25bc6366dcb Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Sep 2018 15:32:15 +0200
Subject: [PATCH] better parsing of model features
---
src/storm-parsers/parser/JaniParser.cpp | 24 ++++++++++++------------
src/storm/storage/jani/ModelFeatures.cpp | 10 +++++++++-
src/storm/storage/jani/ModelFeatures.h | 6 +++++-
3 files changed, 26 insertions(+), 14 deletions(-)
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<ModelFeature> 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<ModelFeature> const& asSet() const;
- void add(ModelFeature const& modelFeature);
+ ModelFeatures& add(ModelFeature const& modelFeature);
void remove(ModelFeature const& modelFeature);
private:
std::set<ModelFeature> features;
};
+
+ ModelFeatures getAllKnownModelFeatures();
+
}
}