From c1f85b0fac2fa02677ea3db8375dc68c95630e2e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 26 Sep 2018 14:09:45 +0200
Subject: [PATCH] improved the assignmentsFinder a little

---
 .../jani/traverser/AssignmentsFinder.cpp      | 42 ++++++++++++-------
 1 file changed, 26 insertions(+), 16 deletions(-)

diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
index 4bf0d14d9..c232cddd8 100644
--- a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
@@ -8,7 +8,7 @@ namespace storm {
         AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, storm::jani::Variable const& variable) {
             return find(model, variable.getExpressionVariable());
         }
-        
+
         AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, storm::expressions::Variable const& variable) {
             ResultType res;
             res.hasLocationAssignment = false;
@@ -20,35 +20,45 @@ namespace storm {
         
         void AssignmentsFinder::traverse(Location const& location, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<storm::expressions::Variable const*, ResultType*>>(data);
-            for (auto const& assignment : location.getAssignments()) {
-                storm::jani::Variable const& assignedVariable = assignment.lValueIsArrayAccess() ? assignment.getLValue().getArray() : assignment.getVariable();
-                if (assignedVariable.getExpressionVariable() == *resVar.first) {
-                    resVar.second->hasLocationAssignment = true;
+            if (!resVar.second->hasLocationAssignment) {
+                for (auto const& assignment : location.getAssignments()) {
+                    storm::jani::Variable const& assignedVariable = assignment.lValueIsArrayAccess() ? assignment.getLValue().getArray() : assignment.getVariable();
+                    if (assignedVariable.getExpressionVariable() == *resVar.first) {
+                        resVar.second->hasLocationAssignment = true;
+                        break;
+                    }
                 }
             }
-            ConstJaniTraverser::traverse(location, data);
         }
         
         void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<storm::expressions::Variable const*, ResultType*>>(data);
-            for (auto const& assignment : templateEdge.getAssignments()) {
-                storm::jani::Variable const& assignedVariable = assignment.lValueIsArrayAccess() ? assignment.getLValue().getArray() : assignment.getVariable();
-                if (assignedVariable.getExpressionVariable() == *resVar.first) {
-                    resVar.second->hasEdgeAssignment = true;
+            if (!resVar.second->hasEdgeAssignment) {
+                for (auto const& assignment : templateEdge.getAssignments()) {
+                    storm::jani::Variable const& assignedVariable = assignment.lValueIsArrayAccess() ? assignment.getLValue().getArray() : assignment.getVariable();
+                    if (assignedVariable.getExpressionVariable() == *resVar.first) {
+                        resVar.second->hasEdgeAssignment = true;
+                        break;
+                    }
+                
                 }
             }
-            ConstJaniTraverser::traverse(templateEdge, data);
+            for (auto const& dest : templateEdge.getDestinations()) {
+                traverse(dest, data);
+            }
         }
         
         void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<storm::expressions::Variable const*, ResultType*>>(data);
-            for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) {
-                storm::jani::Variable const& assignedVariable = assignment.lValueIsArrayAccess() ? assignment.getLValue().getArray() : assignment.getVariable();
-                if (assignedVariable.getExpressionVariable() == *resVar.first) {
-                    resVar.second->hasEdgeDestinationAssignment = true;
+            if (!resVar.second->hasEdgeDestinationAssignment) {
+                for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) {
+                    storm::jani::Variable const& assignedVariable = assignment.lValueIsArrayAccess() ? assignment.getLValue().getArray() : assignment.getVariable();
+                    if (assignedVariable.getExpressionVariable() == *resVar.first) {
+                        resVar.second->hasEdgeDestinationAssignment = true;
+                        break;
+                    }
                 }
             }
-            ConstJaniTraverser::traverse(templateEdgeDestination, data);
         }
     }
 }