From 4b1af3c51e17e9f0ee8c86f97c7e44e36831b56a Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 17 Apr 2019 18:28:23 +0200
Subject: [PATCH] Set labels in property as relevant events as well

---
 src/storm-dft-cli/storm-dft.cpp | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 19dec5f9d..1c036a33d 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -127,8 +127,26 @@ void processOptions() {
         props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
     }
 
+    // Get necessary labels from properties
+    std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
+    for (auto property : props) {
+        property->gatherAtomicLabelFormulas(atomicLabels);
+    }
+
+    // Set relevant event names
+    std::vector<std::string> relevantEventNames = faultTreeSettings.getRelevantEvents();
+    // Events from properties are relevant as well
+    for (auto atomic : atomicLabels) {
+        std::string label = atomic->getLabel();
+        std::size_t foundIndex = label.find("_fail");
+        if (foundIndex != std::string::npos) {
+            relevantEventNames.push_back(label.substr(0, foundIndex));
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known.");
+        }
+    }
+
     // Set relevant elements
-    // TODO: also incorporate events from properties
     std::set<size_t> relevantEvents; // Per default only the toplevel event is relevant
     // Possible clash of relevantEvents and disableDC was already considered in FaultTreeSettings::check().
     if (faultTreeSettings.areRelevantEventsSet()) {