enabled pushing location assignments to edges

src/storm/storage/jani/Automaton.cpp

@@ -8,6 +8,7 @@
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidTypeException.h"
+#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace jani {
@@ -419,6 +420,33 @@ namespace storm {
             edges.pushAssignmentsToDestinations();
         }
         
+        void Automaton::pushTransientRealLocationAssignmentsToEdges() {
+            std::set<std::shared_ptr<storm::jani::TemplateEdge>> encounteredTemplateEdges;
+            
+            for (uint64_t locationIndex = 0; locationIndex < locations.size(); ++locationIndex) {
+                auto& location = locations[locationIndex];
+                auto edges = this->getEdgesFromLocation(locationIndex);
+            
+                for (auto& edge : edges) {
+                    STORM_LOG_THROW(encounteredTemplateEdges.find(edge.getTemplateEdge()) == encounteredTemplateEdges.end(), storm::exceptions::NotSupportedException, "Pushing location assignments to edges is only supported for automata with unique template edges.");
+
+                    auto& templateEdge = edge.getTemplateEdge();
+                    encounteredTemplateEdges.insert(templateEdge);
+                    
+                    storm::jani::Location newLocation(location.getName());
+                    for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
+                        if (assignment.getVariable().isTransient() && assignment.getVariable().isRealVariable()) {
+                            templateEdge->addTransientAssignment(assignment, true);
+                        } else {
+                            newLocation.addTransientAssignment(assignment);
+                        }
+                    }
+                    
+                    location = std::move(newLocation);
+                }
+            }
+        }
+        
         bool Automaton::hasTransientEdgeDestinationAssignments() const {
             for (auto const& edge : this->getEdges()) {
                 if (edge.hasTransientEdgeDestinationAssignments()) {
@@ -440,7 +468,6 @@ namespace storm {
             return true;
         }
 
-
         bool Automaton::usesAssignmentLevels() const {
             return edges.usesAssignmentLevels();
         }

src/storm/storage/jani/Automaton.h

@@ -294,6 +294,12 @@ namespace storm {
              */
             void pushEdgeAssignmentsToDestinations();
             
+            /*!
+             * Pushes the assignments to real-valued transient variables to the edges.
+             * Note: This is currently only supported if the template edges are uniquely coupled with one source location.
+             */
+            void pushTransientRealLocationAssignmentsToEdges();
+            
             /*!
              * Retrieves whether there is any transient edge destination assignment in the automaton.
              */

src/storm/storage/jani/Model.cpp

@@ -1107,6 +1107,11 @@ namespace storm {
      
         void Model::makeStandardJaniCompliant() {
             for (auto& automaton : automata) {
+                // For discrete-time models, we push the assignments to real-valued transient variables (rewards) to the
+                // edges.
+                if (this->isDiscreteTimeModel()) {
+                    automaton.pushTransientRealLocationAssignmentsToEdges();
+                }
                 automaton.pushEdgeAssignmentsToDestinations();
             }
         }

src/storm/storage/jani/OrderedAssignments.cpp

@@ -17,7 +17,7 @@ namespace storm {
             add(assignment);
         }
         
-        bool OrderedAssignments::add(Assignment const& assignment) {
+        bool OrderedAssignments::add(Assignment const& assignment, bool addToExisting) {
             // If the element is contained in this set of assignment, nothing needs to be added.
             if (this->contains(assignment)) {
                 return false;
@@ -27,18 +27,22 @@ namespace storm {
             auto it = lowerBound(assignment, allAssignments);
 
             if (it != allAssignments.end()) {
-                STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression()  << "') to variable '" <<  (*it)->getVariable().getName() << "' already exists.");
-            }
-            
-            // Finally, insert the new element in the correct vectors.
-            auto elementToInsert = std::make_shared<Assignment>(assignment);
-            allAssignments.emplace(it, elementToInsert);
-            if (assignment.isTransient()) {
-                auto transientIt = lowerBound(assignment, transientAssignments);
-                transientAssignments.emplace(transientIt, elementToInsert);
+                if ((!addToExisting || !assignment.getExpressionVariable().hasNumericalType())) {
+                    STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression()  << "') to variable '" <<  (*it)->getVariable().getName() << "' already exists.");
+                } else if (addToExisting && assignment.getExpressionVariable().hasNumericalType()) {
+                    (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression());
+                }
             } else {
-                auto nonTransientIt = lowerBound(assignment, nonTransientAssignments);
-                nonTransientAssignments.emplace(nonTransientIt, elementToInsert);
+                // Finally, insert the new element in the correct vectors.
+                auto elementToInsert = std::make_shared<Assignment>(assignment);
+                allAssignments.emplace(it, elementToInsert);
+                if (assignment.isTransient()) {
+                    auto transientIt = lowerBound(assignment, transientAssignments);
+                    transientAssignments.emplace(transientIt, elementToInsert);
+                } else {
+                    auto nonTransientIt = lowerBound(assignment, nonTransientAssignments);
+                    nonTransientAssignments.emplace(nonTransientIt, elementToInsert);
+                }
             }
             
             return true;

src/storm/storage/jani/OrderedAssignments.h

@@ -26,9 +26,11 @@ namespace storm {
             /*!
              * Adds the given assignment to the set of assignments.
              *
+             * @addToExisting If true the value of the assigned expression is added to a (potentially) previous assignment
+             * to the variable. If false and there is already an assignment, an exception is thrown.
              * @return True iff the assignment was added.
              */
-            bool add(Assignment const& assignment);
+            bool add(Assignment const& assignment, bool addToExisting = false);
             
             /*!
              * Removes the given assignment from this set of assignments.

src/storm/storage/jani/TemplateEdge.cpp

@@ -20,8 +20,8 @@ namespace storm {
             destinations.emplace_back(destination);
         }
         
-        bool TemplateEdge::addTransientAssignment(Assignment const& assignment) {
-            return assignments.add(assignment);
+        bool TemplateEdge::addTransientAssignment(Assignment const& assignment, bool addToExisting) {
+            return assignments.add(assignment, addToExisting);
         }
         
         void TemplateEdge::finalize(Model const& containingModel) {
@@ -106,7 +106,7 @@ namespace storm {
             STORM_LOG_ASSERT(!destinations.empty(), "Need non-empty destinations for this transformation.");
             for (auto const& assignment : this->getAssignments()) {
                 for (auto& destination : destinations) {
-                    destination.addAssignment(assignment);
+                    destination.addAssignment(assignment, true);
                 }
             }
             this->assignments.clear();

src/storm/storage/jani/TemplateEdge.h

@@ -40,9 +40,11 @@ namespace storm {
              * Adds a transient assignment to this edge.
              *
              * @param assignment The transient assignment to add.
+             * @param addToExisting Determines if adding the assigned expression to an already existing assignment is
+             * allowed (if the assigned variable is quantitative).
              * @return True if the assignment was added.
              */
-            bool addTransientAssignment(Assignment const& assignment);
+            bool addTransientAssignment(Assignment const& assignment, bool addToExisting = false);
             
             /*!
              * Retrieves a set of (global) variables that are written by at least one of the edge's destinations.

src/storm/storage/jani/TemplateEdgeDestination.cpp

@@ -31,8 +31,8 @@ namespace storm {
             return assignments.remove(assignment);
         }
         
-        void TemplateEdgeDestination::addAssignment(Assignment const& assignment) {
-            assignments.add(assignment);
+        void TemplateEdgeDestination::addAssignment(Assignment const& assignment, bool addToExisting) {
+            assignments.add(assignment, addToExisting);
         }
         
         bool TemplateEdgeDestination::hasAssignment(Assignment const& assignment) const {

src/storm/storage/jani/TemplateEdgeDestination.h

@@ -27,7 +27,7 @@ namespace storm {
             // Convenience methods to access the assignments.
             bool hasAssignment(Assignment const& assignment) const;
             bool removeAssignment(Assignment const& assignment);
-            void addAssignment(Assignment const& assignment);
+            void addAssignment(Assignment const& assignment, bool addToExisting = false);
             
             /*!
              * Retrieves whether this destination has transient assignments.