From 38eadad17db56c287a16ed9da72c1667e6c8bb8a Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 19 Apr 2017 13:46:44 +0200
Subject: [PATCH] Jit: Expression labels which occur twice in list of formulae
 now supported

---
 .../builder/jit/ExplicitJitJaniModelBuilder.cpp     | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 9844a64af..6df0210e9 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -1531,12 +1531,17 @@ namespace storm {
                         }
                     }
                 }
-                    
+
+                std::set<std::string> expressionLabelStrings;
                 for (auto const& expression : this->options.getExpressionLabels()) {
                     cpptempl::data_map label;
-                    label["name"] = expression.toString();
-                    label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
-                    labels.push_back(label);
+                    std::string expressionLabelString = expression.toString();
+                    if(expressionLabelStrings.count(expressionLabelString) == 0) {
+                        label["name"] = expression.toString();
+                        label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
+                        labels.push_back(label);
+                        expressionLabelStrings.insert(expressionLabelString);
+                    }
                 }
                     
                 modelData["labels"] = cpptempl::make_data(labels);