Browse Source

Function and array eliminator now do not perform any action, if the corresponding model feature is not enabled

tempestpy_adaptions
TimQu 6 years ago
parent
commit
ae1987f64c
  1. 14
      src/storm/storage/jani/ArrayEliminator.cpp
  2. 5
      src/storm/storage/jani/FunctionEliminator.cpp

14
src/storm/storage/jani/ArrayEliminator.cpp

@ -668,12 +668,16 @@ namespace storm {
} }
ArrayEliminatorData ArrayEliminator::eliminate(Model& model, bool keepNonTrivialArrayAccess) { 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."); STORM_LOG_ASSERT(!containsArrayExpression(model), "the model still contains array expressions.");
return result; return result;
} }

5
src/storm/storage/jani/FunctionEliminator.cpp

@ -394,7 +394,10 @@ namespace storm {
void eliminateFunctions(Model& model, std::vector<Property>& properties) { 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."); STORM_LOG_ASSERT(!containsFunctionCallExpression(model), "The model still seems to contain function calls.");
} }

Loading…
Cancel
Save