From c3859ec021a047a221bb0129050ab22a0280e9a4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= <dbasgoeze.github@basgoeze.com>
Date: Fri, 2 Apr 2021 15:04:27 +0200
Subject: [PATCH] Add merge operation to RelevantEvents

---
 src/storm-dft/utility/RelevantEvents.h | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h
index 4fa2d0769..16fde5118 100644
--- a/src/storm-dft/utility/RelevantEvents.h
+++ b/src/storm-dft/utility/RelevantEvents.h
@@ -152,6 +152,22 @@ namespace storm {
                 }
             }
 
+            /*!
+             * Merge the given RelevantEvents with *this
+             *
+             * @return A reference to *this, allowing chaining i.e. e.merge(a).merge(b)
+             */
+            RelevantEvents& merge(RelevantEvents const &other) {
+                if (!this->allRelevant) {
+                    if(other.allRelevant) {
+                        setAllRelevant();
+                    } else {
+                        this->names.insert(other.names.begin(), other.names.end());
+                    }
+                }
+                return *this;
+            }
+
         private:
             void setAllRelevant() {
                 this->allRelevant = true;