diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 09188848b..a46e20e39 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -129,8 +129,8 @@ namespace storm { */ template storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const& additionalRelevantEventNames) { - storm::utility::RelevantEvents events(additionalRelevantEventNames); - events.addNamesFromProperty(properties); + storm::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end()); + events.insertNamesFromProperties(properties.begin(), properties.end()); return events; } @@ -153,7 +153,7 @@ namespace storm { */ template typename storm::modelchecker::DFTModelChecker::dft_results - analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false, + analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 71a5c8fdf..30f95b856 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -56,7 +56,7 @@ namespace storm { * @return Model checking results for the given properties.. */ dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, - storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false, + storm::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index ddca1e1f1..4823aad3c 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -7,6 +7,7 @@ #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include namespace storm { namespace utility { @@ -15,19 +16,35 @@ namespace storm { public: /*! - * Create relevant events from given event names. + * Constructs empty RelevantEvents object + */ + RelevantEvents() = default; + + /*! + * Create relevant events from given event names in an initializer list. * If name 'all' occurs, all elements are stored as relevant. * - * @param relevantEvents List of relevant event names. + * Allows syntactic sugar like: + * RelevantEvents e = {}; + * and + * RelevantEvents e{"a"}; + * + * @param init The initializer list. */ - 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()); - } + RelevantEvents(std::initializer_list init) { + insert(init.begin(), init.end()); + } + + /*! + * Create relevant events from given event names in a range. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param first Iterator pointing to the start of a range of names. + * @param last Iterator pointing to the end of a range of names. + */ + template + RelevantEvents(ForwardIt first, ForwardIt last) { + insert(first, last); } bool operator==(RelevantEvents const& rhs) { @@ -39,23 +56,25 @@ namespace storm { } /*! - * Add relevant event names required by the labels in properties. + * Add relevant event names required by the labels in properties of a range. * - * @param properties List of properties. All events occurring in a property are relevant. + * @param first Iterator pointing to the start of a std::shared_ptr range. + * @param last Iterator pointing to the end of a std::shared_ptr range. */ - void addNamesFromProperty(std::vector> const& properties) { + template + void insertNamesFromProperties(ForwardIt first, ForwardIt last) { if (this->allRelevant) { return; } // Get necessary labels from properties - std::vector> atomicLabels; - for (auto property : properties) { - property->gatherAtomicLabelFormulas(atomicLabels); - } + std::vector> atomicLabels{}; + std::for_each(first, last, [&atomicLabels](auto const& property){ + property->gatherAtomicLabelFormulas(atomicLabels); + }); // Add relevant event names from properties - for (auto atomic : atomicLabels) { + for (auto const& atomic : atomicLabels) { std::string label = atomic->getLabel(); if (label == "failed" or label == "skipped") { // Ignore as these label will always be added if necessary @@ -63,10 +82,10 @@ namespace storm { // Get name of event if (boost::ends_with(label, "_failed")) { // length of "_failed" = 7 - this->addEvent(label.substr(0, label.size() - 7)); + this->names.insert(label.substr(0, label.size() - 7)); } else if (boost::ends_with(label, "_dc")) { // length of "_dc" = 3 - this->addEvent(label.substr(0, label.size() - 3)); + this->names.insert(label.substr(0, label.size() - 3)); } else if (label.find("_claimed_") != std::string::npos) { STORM_LOG_THROW(storm::settings::getModule().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming."); } else { @@ -76,6 +95,36 @@ namespace storm { } } + /*! + * Add relevant event. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param name Name of relevant event. + */ + void insert(std::string const& name) { + if(name == "all") { + setAllRelevant(); + } + names.insert(name); + } + + /*! + * Add relevant event names from a range. + * If name 'all' occurs, all elements are stored as relevant. + * + * @param first Iterator pointing to the start of a range of names. + * @param last Iterator pointing to the end of a range of names. + */ + template + void insert(ForwardIt first, ForwardIt last) { + // check if the name "all" occurs + if (std::any_of(first, last, [](auto const& name) { return name == "all"; })) { + setAllRelevant(); + } else { + this->names.insert(first, last); + } + } + /*! * Check that the relevant names correspond to existing elements in the DFT. * @@ -104,14 +153,9 @@ namespace storm { } private: - - /*! - * Add relevant event. - * - * @param name Name of relevant event. - */ - void addEvent(std::string const& name) { - names.insert(name); + void setAllRelevant() { + this->allRelevant = true; + this->names.clear(); } // Names of relevant events.