From 0a1ed0270a2e6bb54ffcaf75356232092f1a29d1 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 18 Apr 2019 10:48:10 +0200
Subject: [PATCH] Output relevant events for better debugging

---
 .../builder/ExplicitDFTModelBuilder.cpp         |  1 +
 src/storm-dft/storage/dft/DFT.cpp               | 17 +++++++++++++++++
 src/storm-dft/storage/dft/DFT.h                 |  6 ++++++
 3 files changed, 24 insertions(+)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 9fc882e27..ffc7d2f45 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -44,6 +44,7 @@ namespace storm {
             this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents);
             // Mark top level element as relevant
             this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true);
+            STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString());
             if (this->relevantEvents.empty()) {
                 // Only interested in top level event -> introduce unique failed state
                 this->uniqueFailedState = true;
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 21251f044..39b57773f 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -874,6 +874,23 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        std::string DFT<ValueType>::getRelevantEventsString() const {
+            std::stringstream stream;
+            bool first = true;
+            for (auto const& elem : mElements) {
+                if (elem->isRelevant()) {
+                    if (first) {
+                        first = false;
+                    } else {
+                        stream << ", ";
+                    }
+                    stream << elem->name() << " [" << elem->id() << "]";
+                }
+            }
+            return stream.str();
+        }
+
         template<typename ValueType>
         void DFT<ValueType>::writeStatsToStream(std::ostream& stream) const {
             // Count individual types of elements
diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
index 27079a6ba..9c6b31020 100644
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@@ -325,6 +325,12 @@ namespace storm {
              */
             void setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const;
 
+            /*!
+             * Get a string containing the list of all relevant events.
+             * @return String containing all relevant events.
+             */
+            std::string getRelevantEventsString() const;
+
         private:
             std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const;