From 0ed64b62579de01f9d04c75c07d5e595283c57c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Thu, 25 Feb 2021 15:33:09 +0100 Subject: [PATCH] Add == and != ops to RelevantEvents and simplify constructor of RelevantEvents --- src/storm-dft/utility/RelevantEvents.h | 33 ++++++++++++++++---------- 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index 40627dbc1..ddca1e1f1 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -20,18 +20,24 @@ namespace storm { * * @param relevantEvents List of relevant event names. */ - RelevantEvents(std::vector const& relevantEvents = {}) : names(), allRelevant(false) { - for (auto const& name: relevantEvents) { - if (name == "all") { - this->allRelevant = true; - this->names.clear(); - break; - } else { - this->addEvent(name); - } + RelevantEvents(std::vector const& relevantEvents = {}) { + // check if the name "all" occurs + if (std::any_of(relevantEvents.begin(), relevantEvents.end(), + [](auto const& name) { return name == "all"; })) { + this->allRelevant = true; + } else { + this->names.insert(relevantEvents.begin(), relevantEvents.end()); } } + bool operator==(RelevantEvents const& rhs) { + return this->allRelevant == rhs.allRelevant || this->names == rhs.names; + } + + bool operator!=(RelevantEvents const& rhs) { + return !(*this == rhs); + } + /*! * Add relevant event names required by the labels in properties. * @@ -74,7 +80,7 @@ namespace storm { * Check that the relevant names correspond to existing elements in the DFT. * * @param dft DFT. - * @return True iff relevant names are consistent with DFT elements. + * @return True iff the relevant names are consistent with the given DFT. */ template bool checkRelevantNames(storm::storage::DFT const& dft) const { @@ -86,6 +92,9 @@ namespace storm { return true; } + /*! + * @return True iff the given name is the name of a relevant Event + */ bool isRelevant(std::string const& name) const { if (this->allRelevant) { return true; @@ -106,10 +115,10 @@ namespace storm { } // Names of relevant events. - std::set names; + std::set names{}; // Whether all elements are relevant. - bool allRelevant; + bool allRelevant{false}; }; } // namespace utility