From de27fa82fef6bd88847f2b7b6fab5d9ad1444230 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 11 Mar 2020 12:04:00 +0100
Subject: [PATCH] Changed result output iterator for DFTs

---
 .../modelchecker/dft/DFTModelChecker.cpp          |  3 ++-
 src/storm-dft/modelchecker/dft/DFTModelChecker.h  | 15 +++++----------
 2 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index fef4a5d7c..00fe1d0d9 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -534,7 +534,8 @@ namespace storm {
                 } else {
                     os << ", ";
                 }
-                os << boost::apply_visitor(ResultOutputVisitor(), result);
+                boost::variant<std::ostream&> stream(os);
+                boost::apply_visitor(ResultOutputVisitor(), result, stream);
             }
             os << "]" << std::endl;
         }
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
index d40d1488f..068481998 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@@ -22,20 +22,15 @@ namespace storm {
             typedef std::vector<boost::variant<ValueType, approximation_result>> dft_results;
             typedef std::vector<std::shared_ptr<storm::logic::Formula const>> property_vector;
 
-            class ResultOutputVisitor : public boost::static_visitor<std::string> {
+            class ResultOutputVisitor : public boost::static_visitor<> {
             public:
-                std::string operator()(ValueType result) const {
-                    std::stringstream stream;
-                    stream << result;
-                    return stream.str();
+                void operator()(ValueType result, std::ostream& os) const {
+                    os << result;
                 }
 
-                std::string operator()(std::pair<ValueType, ValueType> const& result) const {
-                    std::stringstream stream;
-                    stream << "(" << result.first << ", " << result.second << ")";
-                    return stream.str();
+                void operator()(std::pair<ValueType, ValueType> const& result, std::ostream& os) const {
+                    os << "(" << result.first << ", " << result.second << ")";
                 }
-
             };
 
             /*!