Refactored computation of relevant events

src/storm-dft-cli/storm-dft.cpp

@@ -184,56 +184,16 @@ void processOptions() {
 
 
     // Set relevant event names
-    std::vector<std::string> relevantEventNames;
-    //Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check().
+    std::vector<std::string> additionalRelevantEventNames;
     if (faultTreeSettings.areRelevantEventsSet()) {
-        relevantEventNames = faultTreeSettings.getRelevantEvents();
+        //Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check().
+        additionalRelevantEventNames = faultTreeSettings.getRelevantEvents();
     } else if (faultTreeSettings.isDisableDC()) {
         // All events are relevant
-        relevantEventNames = {"all"};
+        additionalRelevantEventNames = {"all"};
     }
+    std::set<size_t> relevantEvents = storm::api::computeRelevantEvents<ValueType>(*dft, props, additionalRelevantEventNames);
 
-    // Events from properties are relevant as well
-    // Get necessary labels from properties
-    std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
-    for (auto property : props) {
-        property->gatherAtomicLabelFormulas(atomicLabels);
-    }
-    // Add relevant event names from properties
-    for (auto atomic : atomicLabels) {
-        std::string label = atomic->getLabel();
-        if (label == "failed" or label == "skipped") {
-            // Ignore as these label will always be added if necessary
-        } else {
-            // Get name of event
-            if (boost::ends_with(label, "_failed")) {
-                relevantEventNames.push_back(label.substr(0, label.size() - 7));
-            } else if (boost::ends_with(label, "_dc")) {
-                relevantEventNames.push_back(label.substr(0, label.size() - 3));
-            } else if (label.find("_claimed_") != std::string::npos) {
-                STORM_LOG_THROW(faultTreeSettings.isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming.");
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known.");
-            }
-        }
-    }
-
-    // Set relevant elements
-    std::set<size_t> relevantEvents; // Per default no event (except the toplevel event) is relevant
-    for (std::string const& relevantName : relevantEventNames) {
-        if (relevantName == "none") {
-            // Only toplevel event is relevant
-            relevantEvents = {};
-            break;
-        } else if (relevantName == "all") {
-            // All events are relevant
-            relevantEvents = dft->getAllIds();
-            break;
-        } else {
-            // Find and add corresponding event id
-            relevantEvents.insert(dft->getIndex(relevantName));
-        }
-    }
 
     // Analyze DFT
     // TODO allow building of state space even without properties

src/storm-dft/api/storm-dft.h

@@ -12,6 +12,7 @@
 #include "storm-dft/transformations/DftTransformator.h"
 #include "storm-dft/utility/FDEPConflictFinder.h"
 #include "storm-dft/utility/FailureBoundFinder.h"
+#include "storm-dft/utility/RelevantEvents.h"
 
 #include "storm-gspn/api/storm-gspn.h"
 
@@ -117,6 +118,21 @@ namespace storm {
             return true;
         }
 
+        /*!
+         * Get relevant event ids from given relevant event names and labels in properties.
+         *
+         * @param dft DFT.
+         * @param properties List of properties. All events occurring in a property are relevant.
+         * @param additionalRelevantEventNames List of names of additional relevant events.
+         * @return Set of relevant event ids.
+         */
+        template<typename ValueType>
+        std::set<size_t> computeRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, std::vector<std::string> const additionalRelevantEventNames) {
+            std::vector<std::string> relevantNames = storm::utility::getRelevantEventNames<ValueType>(dft, properties);
+            relevantNames.insert(relevantNames.end(), additionalRelevantEventNames.begin(), additionalRelevantEventNames.end());
+            return storm::utility::getRelevantEvents<ValueType>(dft, relevantNames);
+        }
+
         /*!
          * Compute the exact or approximate analysis result of the given DFT according to the given properties.
          * First the Markov model is built from the DFT and then this model is checked against the given properties.

src/storm-dft/settings/modules/FaultTreeSettings.cpp

@@ -41,7 +41,7 @@ namespace storm {
                                                                "Avoid non-determinism by always taking the first possible dependency.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, relevantEventsOptionName, false, "Specifies the relevant events from the DFT.")
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values",
-                                                                                                            "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString(
+                                                                                                            "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' marks only the top level event as relevant.").setDefaultValueString(
                                                 "").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, addLabelsClaimingOptionName, false,

src/storm-dft/utility/RelevantEvents.h

@@ -0,0 +1,69 @@
+#pragma once
+
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
+
+namespace storm {
+    namespace utility {
+
+        /*!
+         * Get relevant event names from labels in properties.
+         *
+         * @param dft DFT.
+         * @param properties List of properties. All events occurring in a property are relevant.
+         * @return List of relevant event names.
+         */
+        template <typename ValueType>
+        std::vector<std::string> getRelevantEventNames(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties) {
+            // Get necessary labels from properties
+            std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
+            for (auto property : properties) {
+                property->gatherAtomicLabelFormulas(atomicLabels);
+            }
+            // Add relevant event names from properties
+            std::vector<std::string> relevantEventNames;
+            for (auto atomic : atomicLabels) {
+                std::string label = atomic->getLabel();
+                if (label == "failed" or label == "skipped") {
+                    // Ignore as these label will always be added if necessary
+                } else {
+                    // Get name of event
+                    if (boost::ends_with(label, "_failed")) {
+                        relevantEventNames.push_back(label.substr(0, label.size() - 7));
+                    } else if (boost::ends_with(label, "_dc")) {
+                        relevantEventNames.push_back(label.substr(0, label.size() - 3));
+                    } else if (label.find("_claimed_") != std::string::npos) {
+                        STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known.");
+                    }
+                }
+            }
+            return relevantEventNames;
+        }
+
+        /*!
+         * Get relevant event id from relevant event name.
+         *
+         * @param dft DFT.
+         * @param relevantEventNames Names of relevant events.
+         * @return Set of relevant event ids.
+         */
+        template <typename ValueType>
+        std::set<size_t> getRelevantEvents(storm::storage::DFT<ValueType> const& dft, std::vector<std::string> const& relevantEventNames) {
+            // Set relevant elements
+            std::set<size_t> relevantEvents; // Per default no event (except the toplevel event) is relevant
+            for (std::string const& relevantName : relevantEventNames) {
+                if (relevantName == "all") {
+                    // All events are relevant
+                    return dft.getAllIds();
+                } else {
+                    // Find and add corresponding event id
+                    relevantEvents.insert(dft.getIndex(relevantName));
+                }
+            }
+            return relevantEvents;
+        }
+
+    } // namespace utility
+} // namespace storm