make jani models copyable

src/storm/storage/jani/Automaton.cpp

@@ -12,47 +12,7 @@
 namespace storm {
     namespace jani {
         
-        namespace detail {
-            Edges::Edges(iterator it, iterator ite) : it(it), ite(ite) {
-                // Intentionally left empty.
-            }
-            
-            Edges::iterator Edges::begin() const {
-                return it;
-            }
-            
-            Edges::iterator Edges::end() const {
-                return ite;
-            }
-            
-            bool Edges::empty() const {
-                return it == ite;
-            }
-            
-            std::size_t Edges::size() const {
-                return std::distance(it, ite);
-            }
 
-            ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) {
-                // Intentionally left empty.
-            }
-            
-            ConstEdges::const_iterator ConstEdges::begin() const {
-                return it;
-            }
-            
-            ConstEdges::const_iterator ConstEdges::end() const {
-                return ite;
-            }
-
-            bool ConstEdges::empty() const {
-                return it == ite;
-            }
-
-            std::size_t ConstEdges::size() const {
-                return std::distance(it, ite);
-            }
-        }
         
         Automaton::Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable) : name(name), locationExpressionVariable(locationExpressionVariable) {
             // Add a sentinel element to the mapping from locations to starting indices.
@@ -176,7 +136,7 @@ namespace storm {
         }
 
         Edge const& Automaton::getEdge(uint64_t index) const {
-            return edges[index];
+            return edges.getConcreteEdges()[index];
         }
         
         Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) {
@@ -307,42 +267,30 @@ namespace storm {
         
         void Automaton::addEdge(Edge const& edge) {
             STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
+            assert(validate());
 
-            // Find the right position for the edge and insert it properly.
-            auto posIt = edges.begin();
-            std::advance(posIt, locationToStartingIndex[edge.getSourceLocationIndex() + 1]);
-            edges.insert(posIt, edge);
+            edges.insertEdge(edge, locationToStartingIndex[edge.getSourceLocationIndex()], locationToStartingIndex[edge.getSourceLocationIndex() + 1]);
+            // Update the set of action indices of this automaton.
+            actionIndices.insert(edge.getActionIndex());
 
             // Now update the starting indices of all subsequent locations.
             for (uint64_t locationIndex = edge.getSourceLocationIndex() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
                 ++locationToStartingIndex[locationIndex];
             }
             
-            // Sort all edges form the source location of the newly introduced edge by their action indices.
-            auto it = edges.begin();
-            std::advance(it, locationToStartingIndex[edge.getSourceLocationIndex()]);
-            auto ite = edges.begin();
-            std::advance(ite, locationToStartingIndex[edge.getSourceLocationIndex() + 1]);
-            std::sort(it, ite, [] (Edge const& a, Edge const& b) { return a.getActionIndex() < b.getActionIndex(); } );
 
-            // Update the set of action indices of this automaton.
-            actionIndices.insert(edge.getActionIndex());
         }
         
         std::vector<Edge>& Automaton::getEdges() {
-            return edges;
+            return edges.getConcreteEdges();
         }
         
         std::vector<Edge> const& Automaton::getEdges() const {
-            return edges;
+            return edges.getConcreteEdges();
         }
         
         std::set<uint64_t> Automaton::getActionIndices() const {
-            std::set<uint64_t> result;
-            for (auto const& edge : edges) {
-                result.insert(edge.getActionIndex());
-            }
-            return result;
+            return edges.getActionIndices();
         }
         
         uint64_t Automaton::getNumberOfLocations() const {
@@ -426,35 +374,22 @@ namespace storm {
             
             this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution));
             
-            for (auto& templateEdge : templateEdges) {
-                templateEdge->substitute(substitution);
-            }
-            for (auto& edge : this->getEdges()) {
-                edge.substitute(substitution);
-            }
+            edges.substitute(substitution);
         }
         void Automaton::registerTemplateEdge(std::shared_ptr<TemplateEdge> const& te) {
-            templateEdges.insert(te);
+            edges.insertTemplateEdge(te);
         }
 
         void Automaton::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
             for (auto& location : locations) {
                 location.changeAssignmentVariables(remapping);
             }
-            for (auto& templateEdge : templateEdges) {
-                templateEdge->changeAssignmentVariables(remapping);
-            }
+            edges.changeAssignmentVariables(remapping);
         }
         
         void Automaton::finalize(Model const& containingModel) {
             //simplifyIndexedAssignments();
-            templateEdges.clear();
-            for (auto& edge : edges) {
-                templateEdges.insert(edge.getTemplateEdge());
-            }
-            for (auto& templateEdge : templateEdges) {
-                templateEdge->finalize(containingModel);
-            }
+            edges.finalize(containingModel);
         }
         
         bool Automaton::containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set<storm::expressions::Variable> const& variables) const {
@@ -481,9 +416,7 @@ namespace storm {
         }
         
         void Automaton::pushEdgeAssignmentsToDestinations() {
-            for (auto& templateEdge : templateEdges) {
-                templateEdge->pushAssignmentsToDestinations();
-            }
+            edges.pushAssignmentsToDestinations();
         }
         
         bool Automaton::hasTransientEdgeDestinationAssignments() const {
@@ -496,25 +429,20 @@ namespace storm {
         }
         
         void Automaton::liftTransientEdgeDestinationAssignments() {
-            for (auto& templateEdge : templateEdges) {
-                templateEdge->liftTransientDestinationAssignments();
-            }
+            edges.liftTransientDestinationAssignments();
         }
 
-        void Automaton::simplifyIndexedAssignments() {
-            // TODO has to be fixed.
-            for (auto& edge : edges) {
-                edge.simplifyIndexedAssignments(variables);
+        bool Automaton::validate() const {
+            assert(locationToStartingIndex.size() == locations.size() + 1);
+            for(uint64_t i = 0; i < locations.size(); i++) {
+                assert(locationToStartingIndex[i] <= locationToStartingIndex[i+1]);
             }
+            return true;
         }
 
+
         bool Automaton::usesAssignmentLevels() const {
-            for (auto const& edge : this->getEdges()) {
-                if (edge.usesAssignmentLevels()) {
-                    return true;
-                }
-            }
-            return false;
+            return edges.usesAssignmentLevels();
         }
         
         bool Automaton::isLinear() const {
@@ -523,18 +451,16 @@ namespace storm {
             for (auto const& location : this->getLocations()) {
                 result &= location.isLinear();
             }
-            
-            for (auto const& templateEdge : templateEdges) {
-                result &= templateEdge->isLinear();
+            if (result) {
+                return edges.isLinear();
             }
-            
-            return result;
+            return false;
         }
 
         void Automaton::restrictToEdges(boost::container::flat_set<uint_fast64_t> const& edgeIndices) {
-            std::vector<Edge> oldEdges = this->edges;
+            std::vector<Edge> oldEdges = this->edges.getConcreteEdges();
             
-            this->edges.clear();
+            this->edges.clearConcreteEdges();
             actionIndices.clear();
             for (auto& e : locationToStartingIndex) {
                 e = 0;

src/storm/storage/jani/Automaton.h

@@ -7,6 +7,8 @@
 #include <boost/container/flat_set.hpp>
 
 #include "storm/storage/jani/VariableSet.h"
+#include "storm/storage/jani/TemplateEdgeContainer.h"
+#include "storm/storage/jani/EdgeContainer.h"
 
 
 namespace storm {
@@ -17,71 +19,6 @@ namespace storm {
         class TemplateEdge;
         class Location;
 
-        namespace detail {
-            class Edges {
-            public:
-                typedef std::vector<Edge>::iterator iterator;
-                typedef std::vector<Edge>::const_iterator const_iterator;
-                
-                Edges(iterator it, iterator ite);
-                
-                /*!
-                 * Retrieves an iterator to the edges.
-                 */
-                iterator begin() const;
-                
-                /*!
-                 * Retrieves an end iterator to the edges.
-                 */
-                iterator end() const;
-                
-                /*!
-                 * Determines whether this set of edges is empty.
-                 */
-                bool empty() const;
-                
-                /*!
-                 * Retrieves the number of edges.
-                 */
-                std::size_t size() const;
-                
-            private:
-                iterator it;
-                iterator ite;
-            };
-            
-            class ConstEdges {
-            public:
-                typedef std::vector<Edge>::iterator iterator;
-                typedef std::vector<Edge>::const_iterator const_iterator;
-                
-                ConstEdges(const_iterator it, const_iterator ite);
-                
-                /*!
-                 * Retrieves an iterator to the edges.
-                 */
-                const_iterator begin() const;
-                
-                /*!
-                 * Retrieves an end iterator to the edges.
-                 */
-                const_iterator end() const;
-
-                /*!
-                 * Determines whether this set of edges is empty.
-                 */
-                bool empty() const;
-
-                /*!
-                 * Retrieves the number of edges.
-                 */
-                std::size_t size() const;
-                
-            private:
-                const_iterator it;
-                const_iterator ite;
-            };
-        }
 
         class Model;
         
@@ -263,6 +200,8 @@ namespace storm {
              */
             void addEdge(Edge const& edge);
 
+            bool validate() const;
+            
             /*!
              * Retrieves the edges of the automaton.
              */
@@ -401,10 +340,7 @@ namespace storm {
             std::unordered_map<std::string, uint64_t> locationToIndex;
             
             /// All edges of the automaton
-            std::vector<Edge> edges;
-            
-            /// The templates for the contained edges.
-            std::unordered_set<std::shared_ptr<TemplateEdge>> templateEdges;
+            EdgeContainer edges;
             
             /// A mapping from location indices to the starting indices. If l is mapped to i, it means that the edges
             /// leaving location l start at index i of the edges vector.

src/storm/storage/jani/Edge.cpp

@@ -116,8 +116,24 @@ namespace storm {
             }
         }
 
+        void Edge::setTemplateEdge(std::shared_ptr<TemplateEdge> const& newTe) {
+            templateEdge = newTe;
+            uint64_t i = 0;
+            std::vector<EdgeDestination> newdestinations;
+
+            assert(destinations.size() == newTe->getNumberOfDestinations());
+            for (auto& destination : destinations) {
+                newdestinations.emplace_back(destination.getLocationIndex(), destination.getProbability(), newTe->getDestination(i));
+                //destination.updateTemplateEdgeDestination(newTe->getDestination(i));
+                ++i;
+            }
+            destinations = newdestinations;
+        }
+
         std::shared_ptr<TemplateEdge> const& Edge::getTemplateEdge() {
             return templateEdge;
         }
+
+
     }
 }

src/storm/storage/jani/Edge.h

@@ -113,6 +113,10 @@ namespace storm {
             
             std::shared_ptr<TemplateEdge> const& getTemplateEdge();
 
+            void setTemplateEdge(std::shared_ptr<TemplateEdge> const& newTe);
+
+            void assertValid() const;
+            
         private:
             /// The index of the source location.
             uint64_t sourceLocationIndex;

src/storm/storage/jani/EdgeContainer.cpp

@@ -0,0 +1,200 @@
+#include "storm/storage/jani/EdgeContainer.h"
+#include "storm/storage/jani/Edge.h"
+#include "storm/storage/jani/TemplateEdge.h"
+#include "storm/storage/jani/Variable.h"
+#include "storm/storage/jani/Model.h"
+
+
+
+namespace storm {
+    namespace jani {
+        namespace detail {
+            Edges::Edges(iterator it, iterator ite) : it(it), ite(ite) {
+                // Intentionally left empty.
+            }
+
+            Edges::iterator Edges::begin() const {
+                return it;
+            }
+
+            Edges::iterator Edges::end() const {
+                return ite;
+            }
+
+            bool Edges::empty() const {
+                return it == ite;
+            }
+
+            std::size_t Edges::size() const {
+                return std::distance(it, ite);
+            }
+
+            ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) {
+                // Intentionally left empty.
+            }
+
+            ConstEdges::const_iterator ConstEdges::begin() const {
+                return it;
+            }
+
+            ConstEdges::const_iterator ConstEdges::end() const {
+                return ite;
+            }
+
+            bool ConstEdges::empty() const {
+                return it == ite;
+            }
+
+            std::size_t ConstEdges::size() const {
+                return std::distance(it, ite);
+            }
+        }
+
+        EdgeContainer::EdgeContainer(EdgeContainer const& other) {
+            edges = other.getConcreteEdges();
+            //templates = other.templates;
+            std::map<std::shared_ptr<TemplateEdge>, std::shared_ptr<TemplateEdge>> map;
+            for (auto const& te : other.templates) {
+                auto newTe = std::make_shared<TemplateEdge>(*te);
+                this->templates.insert(newTe);
+                map[te] = newTe;
+            }
+
+            for (auto& e : edges) {
+                if(map.count(e.getTemplateEdge()) == 0) {
+                    e.setTemplateEdge(std::make_shared<TemplateEdge>(*(e.getTemplateEdge())));
+                } else {
+                    e.setTemplateEdge(map[e.getTemplateEdge()]);
+                }
+            }
+
+
+
+        }
+
+        void EdgeContainer::finalize(Model const& containingModel) {
+            templates.clear();
+            for (auto& edge : edges) {
+                templates.insert(edge.getTemplateEdge());
+            }
+            for (auto& templateEdge : templates) {
+                templateEdge->finalize(containingModel);
+            }
+        }
+
+        void EdgeContainer::clearConcreteEdges() {
+            edges.clear();
+        }
+
+        void EdgeContainer::liftTransientDestinationAssignments() {
+            for (auto& templateEdge : templates) {
+                templateEdge->liftTransientDestinationAssignments();
+            }
+        }
+
+        void EdgeContainer::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            for (auto& templateEdge : templates) {
+                templateEdge->substitute(substitution);
+            }
+            for (auto& edge : edges) {
+                edge.substitute(substitution);
+            }
+        }
+
+        bool EdgeContainer::isLinear() const {
+            for (auto const& templateEdge : templates) {
+                if (!templateEdge->isLinear()) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
+
+        bool EdgeContainer::usesAssignmentLevels() const {
+            for (auto const& edge : edges) {
+                if (edge.usesAssignmentLevels()) {
+                    return true;
+                }
+            }
+            return false;
+
+        }
+
+
+
+        std::vector<Edge> & EdgeContainer::getConcreteEdges() {
+            return edges;
+        }
+
+        std::vector<Edge> const& EdgeContainer::getConcreteEdges() const {
+            return edges;
+        }
+
+        std::set<uint64_t> EdgeContainer::getActionIndices() const {
+            std::set<uint64_t> result;
+            for (auto const& edge : edges) {
+                result.insert(edge.getActionIndex());
+            }
+            return result;
+        }
+
+        /**
+         * Insert an edge, then sort the range between locstart and locend according to the action index.
+         * @param e
+         * @param locStart index where to start
+         * @param locEnd index where to end
+         */
+        void EdgeContainer::insertEdge(Edge const &e, uint64_t locStart, uint64_t locEnd) {
+            assert(locStart <= locEnd);
+            // Find the right position for the edge and insert it properly.
+            auto posIt = edges.begin();
+            std::advance(posIt, locEnd);
+            edges.insert(posIt, e);
+
+            // Sort all edges form the source location of the newly introduced edge by their action indices.
+            auto it = edges.begin();
+            std::advance(it, locStart);
+            auto ite = edges.begin();
+            std::advance(ite, locEnd + 1);
+            std::sort(it, ite, [] (Edge const& a, Edge const& b) { return a.getActionIndex() < b.getActionIndex(); } );
+
+        }
+
+        void EdgeContainer::insertTemplateEdge(std::shared_ptr <TemplateEdge> const &te) {
+            templates.insert(te);
+        }
+
+        void EdgeContainer::pushAssignmentsToDestinations() {
+            for (auto& templateEdge : templates) {
+                templateEdge->pushAssignmentsToDestinations();
+            }
+        }
+
+        void EdgeContainer::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
+            for (auto& templateEdge : templates) {
+                templateEdge->changeAssignmentVariables(remapping);
+            }
+        }
+
+        size_t EdgeContainer::size() const {
+            return edges.size();
+        }
+
+        EdgeContainer::iterator EdgeContainer::begin() {
+            return edges.begin();
+        }
+        EdgeContainer::iterator EdgeContainer::end() {
+            return edges.end();
+        }
+        EdgeContainer::const_iterator EdgeContainer::begin() const {
+            return edges.begin();
+        }
+        EdgeContainer::const_iterator EdgeContainer::end() const {
+            return edges.end();
+        }
+
+
+
+    }
+}

src/storm/storage/jani/EdgeContainer.h

@@ -0,0 +1,125 @@
+#pragma once
+
+#include <vector>
+#include <set>
+#include <map>
+#include "storm/storage/expressions/Expression.h"
+#include "storm/storage/jani/TemplateEdgeContainer.h"
+
+namespace storm {
+    namespace jani {
+
+        class Edge;
+        class TemplateEdge;
+        class Variable;
+        class Model;
+
+        namespace detail {
+            class Edges {
+            public:
+                typedef std::vector<Edge>::iterator iterator;
+                typedef std::vector<Edge>::const_iterator const_iterator;
+
+                Edges(iterator it, iterator ite);
+
+                /*!
+                 * Retrieves an iterator to the edges.
+                 */
+                iterator begin() const;
+
+                /*!
+                 * Retrieves an end iterator to the edges.
+                 */
+                iterator end() const;
+
+                /*!
+                 * Determines whether this set of edges is empty.
+                 */
+                bool empty() const;
+
+                /*!
+                 * Retrieves the number of edges.
+                 */
+                std::size_t size() const;
+
+            private:
+                iterator it;
+                iterator ite;
+            };
+
+
+            class ConstEdges {
+            public:
+                typedef std::vector<Edge>::iterator iterator;
+                typedef std::vector<Edge>::const_iterator const_iterator;
+
+                ConstEdges(const_iterator it, const_iterator ite);
+
+                /*!
+                 * Retrieves an iterator to the edges.
+                 */
+                const_iterator begin() const;
+
+                /*!
+                 * Retrieves an end iterator to the edges.
+                 */
+                const_iterator end() const;
+
+                /*!
+                 * Determines whether this set of edges is empty.
+                 */
+                bool empty() const;
+
+                /*!
+                 * Retrieves the number of edges.
+                 */
+                std::size_t size() const;
+
+            private:
+                const_iterator it;
+                const_iterator ite;
+            };
+        }
+
+
+        class EdgeContainer {
+        public:
+
+            typedef std::vector<Edge>::iterator iterator;
+            typedef std::vector<Edge>::const_iterator const_iterator;
+
+
+            EdgeContainer() = default;
+            EdgeContainer(EdgeContainer const& other);
+
+            void clearConcreteEdges();
+            std::vector<Edge> const& getConcreteEdges() const;
+            std::vector<Edge> & getConcreteEdges();
+            size_t size() const;
+
+            iterator begin();
+            const_iterator begin() const;
+            iterator end();
+            const_iterator end() const;
+
+            std::set<uint64_t> getActionIndices() const;
+
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            void liftTransientDestinationAssignments();
+            void pushAssignmentsToDestinations();
+            void insertEdge(Edge const& e, uint64_t locStart, uint64_t locEnd);
+            void insertTemplateEdge(std::shared_ptr<TemplateEdge> const& te);
+            bool isLinear() const;
+            bool usesAssignmentLevels() const;
+            void finalize(Model const& containingModel);
+
+            void changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping);
+
+
+        private:
+            std::vector<Edge> edges;
+            TemplateEdgeContainer templates;
+        };
+    }
+}
+

src/storm/storage/jani/EdgeDestination.cpp

@@ -58,5 +58,9 @@ namespace storm {
         TemplateEdgeDestination const& EdgeDestination::getTemplateEdgeDestination() const {
             return templateEdgeDestination.get();
         }
+
+        void EdgeDestination::updateTemplateEdgeDestination(TemplateEdgeDestination const& newTed) {
+            templateEdgeDestination = newTed;
+        }
     }
 }

src/storm/storage/jani/EdgeDestination.h

@@ -67,6 +67,8 @@ namespace storm {
              */
             TemplateEdgeDestination const& getTemplateEdgeDestination() const;
 
+            void updateTemplateEdgeDestination(TemplateEdgeDestination const& newTed);
+            
         private:
             // The index of the destination location.
             uint64_t locationIndex;

src/storm/storage/jani/Model.cpp

@@ -212,11 +212,14 @@ namespace storm {
                 if (!SynchronizationVector::isNoActionInput(actionName)) {
                     components.push_back(i);
                     uint64_t actionIndex = oldModel.getActionIndex(actionName);
+                    // store that automaton occurs in the sync vector.
                     participatingAutomataAndActions.push_back(std::make_pair(composedAutomata[i], actionIndex));
+                    // Store for later that this action is one of the possible actions that synchronise
                     synchronizingActionIndices[i].insert(actionIndex);
                 }
             }
 
+            // What is the action label that should be attached to the composed actions
             uint64_t resultingActionIndex = Model::SILENT_ACTION_INDEX;
             if (vector.getOutput() != Model::SILENT_ACTION_NAME) {
                 if (newModel.hasAction(vector.getOutput())) {

src/storm/storage/jani/TemplateEdgeContainer.cpp

@@ -0,0 +1,12 @@
+#include "storm/storage/jani/TemplateEdgeContainer.h"
+#include "storm/storage/jani/TemplateEdge.h"
+
+namespace storm {
+    namespace jani {
+        TemplateEdgeContainer::TemplateEdgeContainer(TemplateEdgeContainer const &other) {
+            for (auto const& te : other) {
+                this->insert(std::make_shared<TemplateEdge>(*te));
+            }
+        }
+    }
+}

src/storm/storage/jani/TemplateEdgeContainer.h

@@ -0,0 +1,16 @@
+#pragma once
+
+#include <memory>
+#include <unordered_set>
+
+namespace storm {
+    namespace jani {
+
+        class TemplateEdge;
+
+        struct TemplateEdgeContainer : public std::unordered_set<std::shared_ptr<TemplateEdge>>   {
+            TemplateEdgeContainer() = default;
+            TemplateEdgeContainer(TemplateEdgeContainer const& other);
+        };
+    }
+}