diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp index f2e3b9855..92e17afbc 100644 --- a/src/storm/storage/jani/EdgeContainer.cpp +++ b/src/storm/storage/jani/EdgeContainer.cpp @@ -67,9 +67,12 @@ namespace storm { e.setTemplateEdge(map[e.getTemplateEdge()]); } } - - - + } + + EdgeContainer& EdgeContainer::operator=(EdgeContainer const& other) { + EdgeContainer otherCpy(other); + this->templates = std::move(other.templates); + this->edges = std::move(other.edges); } void EdgeContainer::finalize(Model const& containingModel) { diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h index bf1e0cbe9..dc2cb8b69 100644 --- a/src/storm/storage/jani/EdgeContainer.h +++ b/src/storm/storage/jani/EdgeContainer.h @@ -91,6 +91,7 @@ namespace storm { EdgeContainer() = default; EdgeContainer(EdgeContainer const& other); + EdgeContainer& operator=(EdgeContainer const& other); void clearConcreteEdges(); std::vector const& getConcreteEdges() const; diff --git a/src/storm/storage/jani/TemplateEdgeContainer.cpp b/src/storm/storage/jani/TemplateEdgeContainer.cpp index ee83d9f6a..66d93a4fb 100644 --- a/src/storm/storage/jani/TemplateEdgeContainer.cpp +++ b/src/storm/storage/jani/TemplateEdgeContainer.cpp @@ -8,5 +8,13 @@ namespace storm { this->insert(std::make_shared(*te)); } } + + TemplateEdgeContainer& TemplateEdgeContainer::operator=(const TemplateEdgeContainer& other) { + this->clear(); + for (auto const& te : other) { + this->insert(std::make_shared(*te)); + } + return *this; + } } } diff --git a/src/storm/storage/jani/TemplateEdgeContainer.h b/src/storm/storage/jani/TemplateEdgeContainer.h index 293302594..12dd6050f 100644 --- a/src/storm/storage/jani/TemplateEdgeContainer.h +++ b/src/storm/storage/jani/TemplateEdgeContainer.h @@ -11,6 +11,7 @@ namespace storm { struct TemplateEdgeContainer : public std::unordered_set> { TemplateEdgeContainer() = default; TemplateEdgeContainer(TemplateEdgeContainer const& other); + TemplateEdgeContainer& operator=(TemplateEdgeContainer const& other); }; } } \ No newline at end of file