From 6dbe2441b91a9f06e314c7b9a10e7fe335248037 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 19 Mar 2019 16:23:52 +0100
Subject: [PATCH] Removed unnecessary members

---
 src/storm-dft/api/storm-dft.h                 |  4 +--
 .../modelchecker/dft/DFTModelChecker.cpp      | 25 +++++++------------
 .../modelchecker/dft/DFTModelChecker.h        | 25 +++++++++++++------
 3 files changed, 29 insertions(+), 25 deletions(-)

diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
index e960fb69c..6cd701e83 100644
--- a/src/storm-dft/api/storm-dft.h
+++ b/src/storm-dft/api/storm-dft.h
@@ -80,7 +80,7 @@ namespace storm {
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
             if (printOutput) {
                 modelChecker.printTimings();
-                modelChecker.printResults();
+                modelChecker.printResults(results);
             }
             return results;
         }
@@ -106,7 +106,7 @@ namespace storm {
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
             if (printOutput) {
                 modelChecker.printTimings();
-                modelChecker.printResults();
+                modelChecker.printResults(results);
             }
             return results;
         }
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 467125c35..c76495177 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -18,9 +18,8 @@ namespace storm {
 
         template<typename ValueType>
         typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
-            // Initialize
-            this->approximationError = approximationError;
             totalTimer.start();
+            dft_results results;
 
             // Optimizing DFT
             storm::storage::DFT<ValueType> dft = origDft.optimize();
@@ -34,13 +33,13 @@ namespace storm {
                 // Model checking
                 std::vector<ValueType> resultsValue = checkModel(model, properties);
                 for (ValueType result : resultsValue) {
-                    checkResults.push_back(result);
+                    results.push_back(result);
                 }
             } else {
-                checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
+                results = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
             }
             totalTimer.stop();
-            return checkResults;
+            return results;
         }
 
         template<typename ValueType>
@@ -442,22 +441,16 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void DFTModelChecker<ValueType>::printResults(std::ostream& os) {
+        void DFTModelChecker<ValueType>::printResults(dft_results const& results, std::ostream& os) {
             bool first = true;
             os << "Result: [";
-            for (auto result : checkResults) {
-                if (!first) {
-                    os << ", ";
-                }
-                if (this->approximationError > 0.0) {
-                    approximation_result resultApprox = boost::get<approximation_result>(result);
-                    os << "(" << resultApprox.first << ", " << resultApprox.second << ")";
-                } else {
-                    os << boost::get<ValueType>(result);
-                }
+            for (auto result : results) {
                 if (first) {
                     first = false;
+                } else {
+                    os << ", ";
                 }
+                os << boost::apply_visitor(ResultOutputVisitor(), result);
             }
             os << "]" << std::endl;
         }
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
index 56d1b4fad..7bc07e30e 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@@ -22,6 +22,22 @@ 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> {
+            public:
+                std::string operator()(ValueType result) const {
+                    std::stringstream stream;
+                    stream << result;
+                    return stream.str();
+                }
+
+                std::string operator()(std::pair<ValueType, ValueType> const& result) const {
+                    std::stringstream stream;
+                    stream << "(" << result.first << ", " << result.second << ")";
+                    return stream.str();
+                }
+
+            };
+
             /*!
              * Constructor.
              */
@@ -53,9 +69,10 @@ namespace storm {
             /*!
              * Print result to stream.
              *
+             * @param results List of results.
              * @param os Output stream to write to.
              */
-            void printResults(std::ostream& os = std::cout);
+            void printResults(dft_results const& results, std::ostream& os = std::cout);
 
         private:
 
@@ -68,12 +85,6 @@ namespace storm {
             storm::utility::Stopwatch modelCheckingTimer;
             storm::utility::Stopwatch totalTimer;
 
-            // Model checking results
-            dft_results checkResults;
-
-            // Allowed error bound for approximation
-            double approximationError;
-
             /*!
              * Internal helper for model checking a DFT.
              *