From 6dcbf75fe3ef8e003fd7b842b45015bf6e097aec Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 8 Oct 2020 11:47:08 +0200
Subject: [PATCH] Update progress measurments only if --progress flag is set

---
 .../settings/modules/GeneralSettings.cpp      |  4 ++++
 src/storm/settings/modules/GeneralSettings.h  |  7 +++++++
 src/storm/utility/ProgressMeasurement.cpp     | 19 +++++++++++--------
 src/storm/utility/ProgressMeasurement.h       | 17 ++++++++++++-----
 4 files changed, 34 insertions(+), 13 deletions(-)

diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp
index b21e35c74..0392b61a3 100644
--- a/src/storm/settings/modules/GeneralSettings.cpp
+++ b/src/storm/settings/modules/GeneralSettings.cpp
@@ -65,6 +65,10 @@ namespace storm {
             bool GeneralSettings::isVerboseSet() const {
                 return this->getOption(verboseOptionName).getHasOptionBeenSet();
             }
+
+            bool GeneralSettings::isShowProgressSet() const {
+                return this->getOption(showProgressOptionName).getHasOptionBeenSet();
+            }
             
             uint64_t GeneralSettings::getShowProgressDelay() const {
                 return this->getOption(showProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger();
diff --git a/src/storm/settings/modules/GeneralSettings.h b/src/storm/settings/modules/GeneralSettings.h
index 25d434692..42f6a4dfe 100644
--- a/src/storm/settings/modules/GeneralSettings.h
+++ b/src/storm/settings/modules/GeneralSettings.h
@@ -50,6 +50,13 @@ namespace storm {
                  */
                 bool isVerboseSet() const;
 
+                /*!
+                 * Retrieves whether the progress option was set.
+                 *
+                 * @return True if the progress option was set.
+                 */
+                bool isShowProgressSet() const;
+
                 /*!
                  * Retrieves the delay for printing information about the exploration progress.
                  *
diff --git a/src/storm/utility/ProgressMeasurement.cpp b/src/storm/utility/ProgressMeasurement.cpp
index 4a0715323..de0af7c50 100644
--- a/src/storm/utility/ProgressMeasurement.cpp
+++ b/src/storm/utility/ProgressMeasurement.cpp
@@ -11,7 +11,9 @@ namespace storm {
     namespace utility {
 
         ProgressMeasurement::ProgressMeasurement(std::string const& itemName) : itemName(itemName), maxCount(std::numeric_limits<uint64_t>::max()) {
-            delay = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getShowProgressDelay();
+            auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            showProgress = generalSettings.isShowProgressSet();
+            delay = generalSettings.getShowProgressDelay();
         }
         
         void ProgressMeasurement::startNewMeasurement(uint64_t startCount) {
@@ -21,13 +23,14 @@ namespace storm {
         }
         
         bool ProgressMeasurement::updateProgress(uint64_t count) {
-            std::stringstream stream;
-            if (updateProgress(count, stream)) {
-                std::string message = stream.str();
-                // Remove the line break at the end of the message.
-                message.pop_back();
-                STORM_LOG_INFO(message);
-                return true;
+            if (showProgress) {
+                std::stringstream stream;
+                if (updateProgress(count, stream)) {
+                    std::string message = stream.str();
+                    // Message already contains line break at the end.
+                    STORM_PRINT_AND_LOG(message);
+                    return true;
+                }
             }
             return false;
         }
diff --git a/src/storm/utility/ProgressMeasurement.h b/src/storm/utility/ProgressMeasurement.h
index 089758583..2ae2331d0 100644
--- a/src/storm/utility/ProgressMeasurement.h
+++ b/src/storm/utility/ProgressMeasurement.h
@@ -29,19 +29,23 @@ namespace storm {
             void startNewMeasurement(uint64_t startCount);
             
             /*!
-             * Updates the progress to the current count.
+             * Updates the progress to the current count and prints it if the delay passed.
+             * The progress is only updated and printed if the ShowProgress setting is enabled.
+             *
              * @param count The currently achieved count.
-             * @return true iff the progress was printed (i.e., the delay passed).
+             * @return True iff the progress was printed (i.e., the delay passed and showProgress setting enabled).
              */
             bool updateProgress(uint64_t count);
             
             /*!
              * Updates the progress to the current count.
+             * The update and printing is done independently of the showProgress setting.
+             *
              * @param count The currently achieved count.
              * @param outstream The stream to which the progress is printed (if the delay passed)
-             * @return true iff the progress was printed (i.e., the delay passed)
+             * @return True iff the progress was printed (i.e., the delay passed)
              */
-            bool updateProgress(uint64_t value, std::ostream& outstream);
+            bool updateProgress(uint64_t count, std::ostream& outstream);
             
             /*!
              * Returns whether a maximal count (which is required to achieve 100% progress) has been specified
@@ -86,7 +90,10 @@ namespace storm {
             void setItemName(std::string const& name);
 
         private:
-        
+
+            // Whether progress should be printed to standard output.
+            bool showProgress;
+
             // The delay (in seconds) between progress emission.
             uint64_t delay;
             // A name for what this is measuring (iterations, states, ...)