towards template edges

src/storm/storage/jani/EdgeDestination.cpp

@@ -6,22 +6,10 @@
 namespace storm {
     namespace jani {
         
-        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, OrderedAssignments const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) {
-            // Intentionally left empty.
-        }
-
-        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, Assignment const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) {
-            // Intentionally left empty.
-        }
-
-        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) {
+        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::shared_ptr<TemplateEdgeDestination const> const& templateEdgeDestination) : locationIndex(locationIndex), probability(probability), templateEdgeDestination(templateEdgeDestination) {
             // Intentionally left empty.
         }
         
-        void EdgeDestination::addAssignment(Assignment const& assignment) {
-            assignments.add(assignment);
-        }
-        
         uint64_t EdgeDestination::getLocationIndex() const {
             return locationIndex;
         }
@@ -45,24 +33,19 @@ namespace storm {
         }
         
         OrderedAssignments const& EdgeDestination::getOrderedAssignments() const {
-            return assignments;
+            return templateEdgeDestination->getOrderedAssignments();
         }
         
         void EdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             this->setProbability(this->getProbability().substitute(substitution));
-            assignments.substitute(substitution);
         }
         
         bool EdgeDestination::hasAssignment(Assignment const& assignment) const {
-            return assignments.contains(assignment);
-        }
-        
-        bool EdgeDestination::removeAssignment(Assignment const& assignment) {
-            return assignments.remove(assignment);
+            return this->getOrderedAssignments().contains(assignment);
         }
         
         bool EdgeDestination::hasTransientAssignment() const {
-            return !assignments.getTransientAssignments().empty();
+            return !this->getOrderedAssignments().getTransientAssignments().empty();
         }
         
         bool EdgeDestination::usesAssignmentLevels() const {
@@ -72,5 +55,8 @@ namespace storm {
             return this->getOrderedAssignments().getLowestLevel() != 0 || this->getOrderedAssignments().getHighestLevel() != 0;
         }
         
+        std::shared_ptr<TemplateEdgeDestination const> EdgeDestination::getTemplateEdgeDestination() const {
+            return templateEdgeDestination;
+        }
     }
 }

src/storm/storage/jani/EdgeDestination.h

@@ -4,7 +4,7 @@
 
 #include "storm/storage/expressions/Expression.h"
 
-#include "storm/storage/jani/OrderedAssignments.h"
+#include "storm/storage/jani/TemplateEdgeDestination.h"
 
 namespace storm {
     namespace jani {
@@ -14,16 +14,8 @@ namespace storm {
             /*!
              * Creates a new edge destination.
              */
-            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, OrderedAssignments const& assignments);
-            
-            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, Assignment const& assignment);
-            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {});
-            
-            /*!
-             * Additionally performs the given assignment when choosing this destination.
-             */
-            void addAssignment(Assignment const& assignment);
-            
+            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::shared_ptr<TemplateEdgeDestination const> const& templateEdgeDestination);
+                        
             /*!
              * Retrieves the id of the destination location.
              */
@@ -39,6 +31,11 @@ namespace storm {
              */
             void setProbability(storm::expressions::Expression const& probability);
 
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+
             /*!
              * Retrieves the mapping from variables to their assigned expressions that corresponds to the assignments
              * of this destination.
@@ -51,13 +48,9 @@ namespace storm {
             OrderedAssignments const& getOrderedAssignments() const;
             
             /*!
-             * Substitutes all variables in all expressions according to the given substitution.
+             * Checks whether this destination has the given assignment.
              */
-            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
-            
-            // Convenience methods to access the assignments.
             bool hasAssignment(Assignment const& assignment) const;
-            bool removeAssignment(Assignment const& assignment);
             
             /*!
              * Retrieves whether this destination has transient assignments.
@@ -69,6 +62,11 @@ namespace storm {
              */
             bool usesAssignmentLevels() const;
             
+            /*!
+             * Retrieves the template destination for this destination.
+             */
+            std::shared_ptr<TemplateEdgeDestination const> getTemplateEdgeDestination() const;
+            
         private:
             // The index of the destination location.
             uint64_t locationIndex;
@@ -76,8 +74,8 @@ namespace storm {
             // The probability to go to the destination.
             storm::expressions::Expression probability;
             
-            // The (ordered) assignments to make when choosing this destination.
-            OrderedAssignments assignments;
+            // The template edge destination
+            std::shared_ptr<TemplateEdgeDestination const> templateEdgeDestination;
         };
         
     }

src/storm/storage/jani/TemplateEdge.cpp

@@ -3,6 +3,9 @@
 namespace storm {
     namespace jani {
         
+        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, std::vector<std::shared_ptr<TemplateEdgeDestination const>> destinations) : guard(guard), destinations(destinations) {
+            // Intentionally left empty.
+        }
         
         
     }

src/storm/storage/jani/TemplateEdge.h

@@ -1,10 +1,11 @@
 #pragma once
 
 #include <vector>
+#include <memory>
 
 #include "storm/storage/expressions/Expression.h"
 
-#include "storm/storage/jani/EdgeDestination.h"
+#include "storm/storage/jani/TemplateEdgeDestination.h"
 
 namespace storm {
     namespace jani {
@@ -12,14 +13,14 @@ namespace storm {
         class TemplateEdge {
         public:
             TemplateEdge() = default;
-            TemplateEdge(storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
+            TemplateEdge(storm::expressions::Expression const& guard, std::vector<std::shared_ptr<TemplateEdgeDestination const>> destinations = {});
             
         private:
             // The guard of the template edge.
             storm::expressions::Expression guard;
             
             // The destinations of the template edge.
-            std::vector<EdgeDestination> destinations;
+            std::vector<std::shared_ptr<TemplateEdgeDestination const>> destinations;
         };
         
     }

src/storm/storage/jani/TemplateEdgeDestination.cpp

@@ -0,0 +1,31 @@
+#include "storm/storage/jani/TemplateEdgeDestination.h"
+
+namespace storm {
+    namespace jani {
+        
+        TemplateEdgeDestination::TemplateEdgeDestination(OrderedAssignments const& assignments) : assignments(assignments) {
+            // Intentionally left empty.
+        }
+        
+        TemplateEdgeDestination::TemplateEdgeDestination(Assignment const& assignment) : assignments(assignment) {
+            // Intentionally left empty.
+        }
+        
+        TemplateEdgeDestination::TemplateEdgeDestination(std::vector<Assignment> const& assignments) : assignments(assignments) {
+            // Intentionally left empty.
+        }
+        
+        void TemplateEdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            assignments.substitute(substitution);
+        }
+        
+        OrderedAssignments const& TemplateEdgeDestination::getOrderedAssignments() const {
+            return assignments;
+        }
+        
+        bool TemplateEdgeDestination::removeAssignment(Assignment const& assignment) {
+            return assignments.remove(assignment);
+        }
+        
+    }
+}

src/storm/storage/jani/TemplateEdgeDestination.h

@@ -0,0 +1,42 @@
+#pragma once
+
+#include "storm/storage/jani/OrderedAssignments.h"
+
+namespace storm {
+    namespace jani {
+        
+        class TemplateEdgeDestination {
+        public:
+            TemplateEdgeDestination() = default;
+            TemplateEdgeDestination(OrderedAssignments const& assignments);
+            TemplateEdgeDestination(Assignment const& assignment);
+            TemplateEdgeDestination(std::vector<Assignment> const& assignments = {});
+
+            /*!
+             * Substitutes all variables in all expressions according to the given substitution.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
+            OrderedAssignments const& getOrderedAssignments() const;
+            
+            // Convenience methods to access the assignments.
+            bool hasAssignment(Assignment const& assignment) const;
+            bool removeAssignment(Assignment const& assignment);
+            
+            /*!
+             * Retrieves whether this destination has transient assignments.
+             */
+            bool hasTransientAssignment() const;
+            
+            /*!
+             * Retrieves whether the edge uses an assignment level other than zero.
+             */
+            bool usesAssignmentLevels() const;
+            
+        private:
+            // The (ordered) assignments to make when choosing this destination.
+            OrderedAssignments assignments;
+        };
+        
+    }
+}