From 0842cb1bd701303de41798071cfebd3fe3b81447 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 15 Oct 2019 20:51:01 +0200
Subject: [PATCH] DdJaniModelBuilder: adding source locations to guards to
 correctly track action fragments writing global variables

---
 src/storm/builder/DdJaniModelBuilder.cpp | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index f05199ccc..3e0250ac8 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -1325,9 +1325,10 @@ namespace storm {
                         
                         STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect.");
                     }
-                    
+                                        
                     // Now that we have built the destinations, we always take the full guard.
-                    guard = rangedGuard;
+                    storm::dd::Bdd<Type> sourceLocationBdd = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex());
+                    guard = sourceLocationBdd && rangedGuard;
                     
                     // Start by gathering all variables that were written in at least one destination.
                     std::set<storm::expressions::Variable> globalVariablesInSomeDestination;
@@ -1361,8 +1362,8 @@ namespace storm {
                     }
                     
                     // Add the source location and the guard.
-                    storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard.template toAdd<ValueType>();
-                    transitions *= sourceLocationAndGuard;
+                    storm::dd::Add<Type, ValueType> guardAdd = guard.template toAdd<ValueType>();
+                    transitions *= guardAdd;
                     
                     // If we multiply the ranges of global variables, make sure everything stays within its bounds.
                     if (!globalVariablesInSomeDestination.empty()) {
@@ -1381,8 +1382,8 @@ namespace storm {
                     // Finally treat the transient assignments.
                     std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                     if (!this->transientVariables.empty()) {
-                        performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &sourceLocationAndGuard, &exitRates] (storm::jani::Assignment const& assignment) {
-                            auto newTransientEdgeAssignments = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
+                        performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guardAdd, &exitRates] (storm::jani::Assignment const& assignment) {
+                            auto newTransientEdgeAssignments = guardAdd * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
                             if (exitRates) {
                                 newTransientEdgeAssignments *= exitRates.get();
                             }
@@ -1390,7 +1391,7 @@ namespace storm {
                         } );
                     }
                     
-                    return EdgeDd(isMarkovian, guard, guard.template toAdd<ValueType>() * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
+                    return EdgeDd(isMarkovian, guard, transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
                 } else {
                     return EdgeDd(false, rangedGuard, rangedGuard.template toAdd<ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>(), std::set<storm::expressions::Variable>());
                 }
@@ -1516,7 +1517,7 @@ namespace storm {
                     
                     // Check for overlapping guards.
                     overlappingGuards = !(edgeDd.guard && allGuards).isZero();
-                    
+
                     // Issue a warning if there are overlapping guards in a DTMC.
                     STORM_LOG_WARN_COND(!overlappingGuards || this->model.getModelType() == storm::jani::ModelType::CTMC || this->model.getModelType() == storm::jani::ModelType::MA, "Guard of an edge in a DTMC overlaps with previous guards.");