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;