From 54a7c847250a8b93d0ccf8347c8073a6525ea3d5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 2 Oct 2018 15:50:46 +0200
Subject: [PATCH] started fixing some issues related to transient variable
 assignments in DD-based JANI model builder

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

diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index b70a41db0..d71cc4cb4 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -960,7 +960,7 @@ namespace storm {
         private:
             AutomatonDd composeInParallel(std::vector<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) {
                 AutomatonDd result(this->variables.manager->template getAddOne<ValueType>());
-
+                
                 // Build the results of the synchronization vectors.
                 std::unordered_map<ActionIdentification, std::vector<ActionDd>, ActionIdentificationHash> actions;
                 for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) {
@@ -1002,6 +1002,9 @@ namespace storm {
                     }
                     
                     result.identity *= automaton.identity;
+                    
+                    // Add the transient location assignments of the automata.
+                    addToTransientAssignmentMap(result.transientLocationAssignments, automaton.transientLocationAssignments);
                 }
                 
                 if (!silentActionDds.empty()) {
@@ -1220,7 +1223,7 @@ namespace storm {
                         storm::dd::Add<Type, ValueType> nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables);
                         transitions += nondeterminismEncoding * action.transitions;
                         
-                        joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments);
+                        transientEdgeAssignments = joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments);
                         
                         storm::dd::Bdd<Type> nondeterminismEncodingBdd = nondeterminismEncoding.toBdd();
                         for (auto& entry : action.variableToWritingFragment) {
@@ -1352,7 +1355,7 @@ namespace storm {
                     guard |= edge.guard;
                     transitions += edge.transitions;
                     variableToWritingFragment = joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment);
-                    joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments);
+                    transientEdgeAssignments = joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments);
                 }
 
                 // Currently, we can only combine the transient edge assignments if there is no overlap of the guards of the edges.
@@ -1649,6 +1652,7 @@ namespace storm {
                     auto const& location = automaton.getLocation(locationIndex);
                     performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) {
                         storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
+                    
                         auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable());
                         if (it != result.transientLocationAssignments.end()) {
                             it->second += assignedValues;
@@ -1901,13 +1905,13 @@ namespace storm {
             std::vector<storm::expressions::Variable> rewardVariables;
             if (options.isBuildAllRewardModelsSet()) {
                 for (auto const& rewExpr : model.getAllRewardModelExpressions()) {
-                    STORM_LOG_ERROR_COND(rewExpr.second.isVariable(), "The jit builder can not build the non-trivial reward expression '" << rewExpr.second << "'.");
+                    STORM_LOG_ERROR_COND(rewExpr.second.isVariable(), "The DD-builder can not build the non-trivial reward expression '" << rewExpr.second << "'.");
                     rewardVariables.push_back(rewExpr.second.getBaseExpression().asVariableExpression().getVariable());
                 }
             } else {
                 for (auto const& rewardModelName : options.getRewardModelNames()) {
                     auto const& rewExpr = model.getRewardModelExpression(rewardModelName);
-                    STORM_LOG_ERROR_COND(rewExpr.isVariable(), "The jit builder can not build the non-trivial reward expression '" << rewExpr << "'.");
+                    STORM_LOG_ERROR_COND(rewExpr.isVariable(), "The DD-builder can not build the non-trivial reward expression '" << rewExpr << "'.");
                     rewardVariables.push_back(rewExpr.getBaseExpression().asVariableExpression().getVariable());
                 }
             }