From ae1987f64c78fdbf8f4255e4ac6ab204acf17cf5 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Sep 2018 15:38:52 +0200
Subject: [PATCH] Function and array eliminator now do not perform any action,
if the corresponding model feature is not enabled
---
src/storm/storage/jani/ArrayEliminator.cpp | 14 +++++++++-----
src/storm/storage/jani/FunctionEliminator.cpp | 5 ++++-
2 files changed, 13 insertions(+), 6 deletions(-)
diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp
index 58379cfc4..cd78f95ca 100644
--- a/src/storm/storage/jani/ArrayEliminator.cpp
+++ b/src/storm/storage/jani/ArrayEliminator.cpp
@@ -668,12 +668,16 @@ namespace storm {
}
ArrayEliminatorData ArrayEliminator::eliminate(Model& model, bool keepNonTrivialArrayAccess) {
- auto sizes = detail::MaxArraySizeDeterminer().getMaxSizes(model);
- ArrayEliminatorData result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess, sizes).replace(model);
- if (!keepNonTrivialArrayAccess) {
- model.getModelFeatures().remove(ModelFeature::Arrays);
+ ArrayEliminatorData result;
+ // Only perform actions if there actually are arrays.
+ if (model.getModelFeatures().hasArrays()) {
+ auto sizes = detail::MaxArraySizeDeterminer().getMaxSizes(model);
+ result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess, sizes).replace(model);
+ if (!keepNonTrivialArrayAccess) {
+ model.getModelFeatures().remove(ModelFeature::Arrays);
+ }
+ model.finalize();
}
- model.finalize();
STORM_LOG_ASSERT(!containsArrayExpression(model), "the model still contains array expressions.");
return result;
}
diff --git a/src/storm/storage/jani/FunctionEliminator.cpp b/src/storm/storage/jani/FunctionEliminator.cpp
index 50d5deb95..ed2784d10 100644
--- a/src/storm/storage/jani/FunctionEliminator.cpp
+++ b/src/storm/storage/jani/FunctionEliminator.cpp
@@ -394,7 +394,10 @@ namespace storm {
void eliminateFunctions(Model& model, std::vector<Property>& properties) {
- detail::FunctionEliminatorTraverser().eliminate(model, properties);
+ // Only perform actions if there actually are functions.
+ if (model.getModelFeatures().hasFunctions()) {
+ detail::FunctionEliminatorTraverser().eliminate(model, properties);
+ }
STORM_LOG_ASSERT(!containsFunctionCallExpression(model), "The model still seems to contain function calls.");
}