Better progress info

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@@ -5,6 +5,7 @@
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
+#include "storm/utility/ProgressMeasurement.h"
 #include "storm/logic/Formulas.h"
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/solver/LinearEquationSolver.h"
@@ -39,9 +40,8 @@ namespace storm {
             
             template <class SparseMdpModelType>
             void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::check(std::vector<ValueType> const& weightVector) {
-                STORM_LOG_DEBUG("Analyzing weight vector " << storm::utility::vector::toString(weightVector));
-
                 ++numChecks;
+                STORM_LOG_INFO("Analyzing weight vector #" << numChecks << ": "  << storm::utility::vector::toString(weightVector));
                 
                 // In case we want to export the cdf, we will collect the corresponding data
                 std::vector<std::vector<ValueType>> cdfData;
@@ -61,7 +61,10 @@ namespace storm {
                     STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << this->objectives.size() << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" <<  epochOrder.size() << "."  << std::endl);
                 }
 
-
+                storm::utility::ProgressMeasurement progress("epochs");
+                progress.setMaxCount(epochOrder.size());
+                progress.startNewMeasurement(0);
+                uint64_t numCheckedEpochs = 0;
                 for (auto const& epoch : epochOrder) {
                     computeEpochSolution(epoch, weightVector, cachedData, precision);
                     if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
@@ -76,6 +79,8 @@ namespace storm {
                         cdfEntry.insert(cdfEntry.end(), solutionIt, solution.end());
                         cdfData.push_back(std::move(cdfEntry));
                     }
+                    ++numCheckedEpochs;
+                    progress.updateProgress(numCheckedEpochs);
                 }
                 
                 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet()) {

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -29,6 +29,7 @@
 #include "storm/settings/modules/CoreSettings.h"
 
 #include "storm/utility/Stopwatch.h"
+#include "storm/utility/ProgressMeasurement.h"
 
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
@@ -99,6 +100,10 @@ namespace storm {
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
                     precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
                 }
+                storm::utility::ProgressMeasurement progress("epochs");
+                progress.setMaxCount(epochOrder.size());
+                progress.startNewMeasurement(0);
+                uint64_t numCheckedEpochs = 0;
                 for (auto const& epoch : epochOrder) {
                     swBuild.start();
                     auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
@@ -196,6 +201,8 @@ namespace storm {
                         rewardUnfolding.setSolutionForCurrentEpoch(storm::utility::vector::filterVector(x, epochModel.epochInStates));
                     }
                     swCheck.stop();
+                    ++numCheckedEpochs;
+                    progress.updateProgress(numCheckedEpochs);
                 }
                 
                 std::map<storm::storage::sparse::state_type, ValueType> result;

src/storm/solver/AbstractEquationSolver.cpp

@@ -16,9 +16,9 @@ namespace storm {
         
         template<typename ValueType>
         AbstractEquationSolver<ValueType>::AbstractEquationSolver() {
-            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            showProgressFlag = generalSettings.isVerboseSet();
-            showProgressDelay = generalSettings.getShowProgressDelay();
+            if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isVerboseSet()) {
+                this->progressMeasurement = storm::utility::ProgressMeasurement("iterations");
+            }
         }
         
         template<typename ValueType>
@@ -203,35 +203,29 @@ namespace storm {
         
         template<typename ValueType>
         bool AbstractEquationSolver<ValueType>::isShowProgressSet() const {
-            return showProgressFlag;
+            return this->progressMeasurement.is_initialized();
         }
         
         template<typename ValueType>
         uint64_t AbstractEquationSolver<ValueType>::getShowProgressDelay() const {
-            return showProgressDelay;
+            STORM_LOG_ASSERT(this->isShowProgressSet(), "Tried to get the progress message delay but progress is not shown.");
+            return this->progressMeasurement->getShowProgressDelay();
         }
         
         template<typename ValueType>
         void AbstractEquationSolver<ValueType>::startMeasureProgress(uint64_t startingIteration) const {
-            timeOfStart = std::chrono::high_resolution_clock::now();
-            timeOfLastMessage = timeOfStart;
-            iterationOfLastMessage = startingIteration;
+            if (this->isShowProgressSet()) {
+                this->progressMeasurement->startNewMeasurement(startingIteration);
+            }
         }
         
         template<typename ValueType>
         void AbstractEquationSolver<ValueType>::showProgressIterative(uint64_t iteration, boost::optional<uint64_t> const& bound) const {
             if (this->isShowProgressSet()) {
-                auto now = std::chrono::high_resolution_clock::now();
-                auto durationSinceLastMessage = static_cast<uint64_t>(std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count());
-                if (durationSinceLastMessage >= this->getShowProgressDelay()) {
-                    uint64_t numberOfIterationsSinceLastMessage = iteration - iterationOfLastMessage;
-                    STORM_LOG_INFO("Completed " << iteration << " iterations "
-                                   << (bound ? "(out of " + std::to_string(bound.get()) + ") " : "")
-                                   << "in " << std::chrono::duration_cast<std::chrono::seconds>(now - timeOfStart).count() << "s (currently " << (static_cast<double>(numberOfIterationsSinceLastMessage) / durationSinceLastMessage) << " per second)."
-                                   );
-                    timeOfLastMessage = std::chrono::high_resolution_clock::now();
-                    iterationOfLastMessage = iteration;
+                if (bound) {
+                    this->progressMeasurement->setMaxCount(bound.get());
                 }
+                this->progressMeasurement->updateProgress(iteration);
             }
         }
         
@@ -240,8 +234,6 @@ namespace storm {
             STORM_LOG_DEBUG("Setting solver precision for a solver that does not support precisions.");
         }
 
-        
-        
         template class AbstractEquationSolver<double>;
         template class AbstractEquationSolver<float>;
 

src/storm/solver/AbstractEquationSolver.h

@@ -7,6 +7,7 @@
 #include <boost/optional.hpp>
 
 #include "storm/solver/TerminationCondition.h"
+#include "storm/utility/ProgressMeasurement.h"
 
 namespace storm {
     namespace solver {
@@ -190,16 +191,8 @@ namespace storm {
             boost::optional<std::vector<ValueType>> upperBounds;
 
         private:
-            // A flag that indicates whether progress is to be shown.
-            bool showProgressFlag;
-            
-            // The delay between progress emission.
-            uint64_t showProgressDelay;
-            
-            // Time points that are used when showing progress.
-            mutable uint64_t iterationOfLastMessage;
-            mutable std::chrono::high_resolution_clock::time_point timeOfStart;
-            mutable std::chrono::high_resolution_clock::time_point timeOfLastMessage;
+            // Indicates the progress of this solver.
+            mutable boost::optional<storm::utility::ProgressMeasurement> progressMeasurement;
         };
         
     }

src/storm/utility/ProgressMeasurement.cpp

@@ -0,0 +1,84 @@
+#include "storm/utility/ProgressMeasurement.h"
+
+#include <sstream>
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace utility {
+
+        ProgressMeasurement::ProgressMeasurement(std::string const& itemName) : itemName(itemName) {
+            delay = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getShowProgressDelay();
+        }
+        
+        void ProgressMeasurement::startNewMeasurement(uint64_t startCount) {
+            lastDisplayedCount = startCount;
+            timeOfStart =  std::chrono::high_resolution_clock::now();
+            timeOfLastMessage = timeOfStart;
+        }
+        
+        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;
+            }
+            return false;
+        }
+
+        bool ProgressMeasurement::updateProgress(uint64_t count, std::ostream& outstream) {
+            auto now = std::chrono::high_resolution_clock::now();
+            // Get the duration since the last message in milliseconds.
+            auto durationSinceLastMessage = static_cast<uint64_t>(std::chrono::duration_cast<std::chrono::milliseconds>(now - this->timeOfLastMessage).count());
+            if (durationSinceLastMessage >= this->delay * 1000) {
+                double itemsPerSecond = (static_cast<double>(count - this->lastDisplayedCount) * 1000.0 / static_cast<double>(durationSinceLastMessage));
+                outstream << "Completed " << count << " " << itemName << " "
+                               << (this->isMaxCountSet() ? "(out of " + std::to_string(this->getMaxCount()) + ") " : "")
+                               << "in " << std::chrono::duration_cast<std::chrono::seconds>(now - timeOfStart).count() << "s (currently " << itemsPerSecond << " " << itemName << " per second)." << std::endl;
+                timeOfLastMessage = std::chrono::high_resolution_clock::now();
+                lastDisplayedCount = count;
+                return true;
+            }
+            return false;
+        }
+        
+        bool ProgressMeasurement::isMaxCountSet() const {
+            return this->maxCount > 0;
+        }
+        
+        uint64_t ProgressMeasurement::getMaxCount() const {
+            STORM_LOG_ASSERT(this->isMaxCountSet(), "Tried to get the maximal count but it was not set before.");
+            return this->maxCount;
+        }
+        
+        void ProgressMeasurement::setMaxCount(uint64_t maxCount) {
+            this->maxCount = maxCount;
+        }
+        
+        void ProgressMeasurement::unsetMaxCount() {
+            this->maxCount = 0;
+        }
+        
+        uint64_t ProgressMeasurement::getShowProgressDelay() const {
+            return this->delay;
+        }
+
+        void ProgressMeasurement::setShowProgressDelay(uint64_t delay) {
+            this->delay = delay;
+        }
+        
+        std::string const& ProgressMeasurement::getItemName() const {
+            return this->itemName;
+        }
+
+        void ProgressMeasurement::setItemName(std::string const& name) {
+            this->itemName = name;
+        }
+        
+    }
+}

src/storm/utility/ProgressMeasurement.h

@@ -0,0 +1,107 @@
+#pragma once
+
+#include <chrono>
+#include <ostream>
+#include <boost/optional.hpp>
+
+namespace storm {
+    namespace utility {
+
+        /*!
+         * A class that provides convenience operations to display run times.
+         */
+        class ProgressMeasurement {
+        public:
+            typedef decltype(std::chrono::duration_cast<std::chrono::seconds>(std::chrono::seconds::zero()).count()) SecondType;
+            typedef decltype(std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::milliseconds::zero()).count()) MilisecondType;
+            typedef decltype(std::chrono::duration_cast<std::chrono::nanoseconds>(std::chrono::nanoseconds::zero()).count()) NanosecondType;
+            
+            /*!
+             * Initializes progress measurement.
+             * @param itemName the name of what we are counting (iterations, states, ...).
+             */
+            ProgressMeasurement(std::string const& itemName = "items");
+            
+            /*!
+             * Starts a new measurement, dropping all progress information collected so far.
+             * @param startCount the initial count.
+             */
+            void startNewMeasurement(uint64_t startCount);
+            
+            /*!
+             * Updates the progress to the current count.
+             * @param count The currently achieved count.
+             * @return true iff the progress was printed (i.e., the delay passed).
+             */
+            bool updateProgress(uint64_t count);
+            
+            /*!
+             * Updates the progress to the current count.
+             * @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)
+             */
+            bool updateProgress(uint64_t value, std::ostream& outstream);
+            
+            /*!
+             * Returns whether a maximal count (which is required to achieve 100% progress) has been specified
+             */
+            bool isMaxCountSet() const;
+            
+            /*!
+             * Returns the maximal possible count (if specified).
+             */
+            uint64_t getMaxCount() const;
+            
+            /*!
+             * Sets the maximal possible count.
+             */
+            void setMaxCount(uint64_t maxCount);
+            
+            /*!
+             * Erases a previously specified maximal count.
+             */
+            void unsetMaxCount();
+            
+            /*!
+             * Returns the currently specified minimal delay (in seconds) between two progress messages.
+             */
+            uint64_t getShowProgressDelay() const;
+            
+            /*!
+             * Customizes the minimal delay between two progress messages.
+             * @param delay the delay (in seconds).
+             */
+            void setShowProgressDelay(uint64_t delay);
+            
+            /*!
+             * Returns the current name of what we are counting (e.g. iterations, states, ...)
+             */
+            std::string const& getItemName() const;
+            
+            /*!
+             * Customizes the name of what we are counting (e.g. iterations, states, ...)
+             * @param name the name of what we are counting.
+             */
+            void setItemName(std::string const& name);
+
+        private:
+        
+            // The delay (in seconds) between progress emission.
+            uint64_t delay;
+            // A name for what this is measuring (iterations, states, ...)
+            std::string itemName;
+            
+            // The maximal count that can be achieved. Zero means unspecified.
+            uint64_t maxCount;
+            
+            // The last displayed count
+            uint64_t lastDisplayedCount;
+            
+            std::chrono::high_resolution_clock::time_point timeOfStart;
+            std::chrono::high_resolution_clock::time_point timeOfLastMessage;
+            
+        };
+        
+    }
+}