From f6faf9e3a57d2ca24eabc9a105b941a7399cd580 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 15 Nov 2018 18:06:30 +0100
Subject: [PATCH] Flag for printing information about model generated from DFT

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

diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
index 136e8bfb4..ca4c7588d 100644
--- a/src/storm-dft/api/storm-dft.h
+++ b/src/storm-dft/api/storm-dft.h
@@ -69,7 +69,7 @@ namespace storm {
         typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
         analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation,
                    bool enableDC, bool printOutput) {
-            storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
+            storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
             if (printOutput) {
                 modelChecker.printTimings();
@@ -95,7 +95,7 @@ namespace storm {
         typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
         analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred,
                          bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
-            storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
+            storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC,
                                                                                                                approximationError);
             if (printOutput) {
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 658ed75c6..d96aacfc4 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -348,9 +348,13 @@ namespace storm {
                 typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet());
                 builder.buildModel(labeloptions, 0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
-                model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
 
+                // Print model information
+                if (printInfo) {
+                    model->printModelInformationToStream(std::cout);
+                }
+
                 // Export the model if required
                 // TODO move this outside of the model checker?
                 if (ioSettings.isExportExplicitSet()) {
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
index 6da5d5aaa..cf05cbb8f 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@@ -25,7 +25,7 @@ namespace storm {
             /*!
              * Constructor.
              */
-            DFTModelChecker() {
+            DFTModelChecker(bool printOutput) : printInfo(printOutput) {
             }
 
             /*!
@@ -58,6 +58,8 @@ namespace storm {
 
         private:
 
+            bool printInfo;
+
             // Timing values
             storm::utility::Stopwatch buildingTimer;
             storm::utility::Stopwatch explorationTimer;