From bb200fe9f42765ccfb83ac937b6c8dfb25690b87 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sat, 13 Jun 2020 18:10:06 -0700
Subject: [PATCH] simplify prism programs now also simplifies labels

---
 src/storm/storage/prism/Program.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index 49381ca8e..dfba08050 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -1498,8 +1498,13 @@ namespace storm {
                     }
                 }
             }
-            
-            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+
+            std::vector<Label> newLabels;
+            for(auto const& label : this->getLabels()) {
+                newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
+            }
+
+            return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
         }
         
         Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {