From cf299a63449878e629b0882ddd45b5cd371c3417 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@web.de>
Date: Tue, 28 Jun 2016 15:44:42 +0200
Subject: [PATCH] fixed the case where an expression occurred twice in the
 formulas

Former-commit-id: 5054ebcae4956eae70843def23ee22df9c5c78e6
---
 src/generator/NextStateGenerator.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index a99f0dcea..54fb2f280 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/src/generator/NextStateGenerator.cpp
@@ -250,10 +250,6 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
-            // Make the labels unique.
-            std::sort(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
-            auto it = std::unique(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );
-            labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it));
             
             for (auto const& expression : this->options.getExpressionLabels()) {
                 std::stringstream stream;
@@ -261,6 +257,11 @@ namespace storm {
                 labelsAndExpressions.push_back(std::make_pair(stream.str(), expression));
             }
             
+            // Make the labels unique.
+            std::sort(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first < b.first; } );
+            auto it = std::unique(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair<std::string, storm::expressions::Expression> const& a, std::pair<std::string, storm::expressions::Expression> const& b) { return a.first == b.first; } );
+            labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it));
+            
             // Prepare result.
             storm::models::sparse::StateLabeling result(states.size());
             
@@ -306,4 +307,4 @@ namespace storm {
         template class NextStateGenerator<storm::RationalFunction>;
         
     }
-}
\ No newline at end of file
+}