diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index fdf939916..2fa1ac2fe 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/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 void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(std::vector 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> 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().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().isExportCdfSet()) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index be6baadb6..0d708ee06 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/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().isSoundSet()) { precision = precision / storm::utility::convertNumber(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 result; diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index 21a33c27c..86dbf0bd1 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -16,9 +16,9 @@ namespace storm { template AbstractEquationSolver::AbstractEquationSolver() { - auto const& generalSettings = storm::settings::getModule(); - showProgressFlag = generalSettings.isVerboseSet(); - showProgressDelay = generalSettings.getShowProgressDelay(); + if (storm::settings::getModule().isVerboseSet()) { + this->progressMeasurement = storm::utility::ProgressMeasurement("iterations"); + } } template @@ -203,35 +203,29 @@ namespace storm { template bool AbstractEquationSolver::isShowProgressSet() const { - return showProgressFlag; + return this->progressMeasurement.is_initialized(); } template uint64_t AbstractEquationSolver::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 void AbstractEquationSolver::startMeasureProgress(uint64_t startingIteration) const { - timeOfStart = std::chrono::high_resolution_clock::now(); - timeOfLastMessage = timeOfStart; - iterationOfLastMessage = startingIteration; + if (this->isShowProgressSet()) { + this->progressMeasurement->startNewMeasurement(startingIteration); + } } template void AbstractEquationSolver::showProgressIterative(uint64_t iteration, boost::optional const& bound) const { if (this->isShowProgressSet()) { - auto now = std::chrono::high_resolution_clock::now(); - auto durationSinceLastMessage = static_cast(std::chrono::duration_cast(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(now - timeOfStart).count() << "s (currently " << (static_cast(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; template class AbstractEquationSolver; diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index be9cc9895..370e96fa1 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -7,6 +7,7 @@ #include #include "storm/solver/TerminationCondition.h" +#include "storm/utility/ProgressMeasurement.h" namespace storm { namespace solver { @@ -190,16 +191,8 @@ namespace storm { boost::optional> 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 progressMeasurement; }; } diff --git a/src/storm/utility/ProgressMeasurement.cpp b/src/storm/utility/ProgressMeasurement.cpp new file mode 100644 index 000000000..db471035f --- /dev/null +++ b/src/storm/utility/ProgressMeasurement.cpp @@ -0,0 +1,84 @@ +#include "storm/utility/ProgressMeasurement.h" + +#include + +#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().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(std::chrono::duration_cast(now - this->timeOfLastMessage).count()); + if (durationSinceLastMessage >= this->delay * 1000) { + double itemsPerSecond = (static_cast(count - this->lastDisplayedCount) * 1000.0 / static_cast(durationSinceLastMessage)); + outstream << "Completed " << count << " " << itemName << " " + << (this->isMaxCountSet() ? "(out of " + std::to_string(this->getMaxCount()) + ") " : "") + << "in " << std::chrono::duration_cast(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; + } + + } +} diff --git a/src/storm/utility/ProgressMeasurement.h b/src/storm/utility/ProgressMeasurement.h new file mode 100644 index 000000000..904294ef5 --- /dev/null +++ b/src/storm/utility/ProgressMeasurement.h @@ -0,0 +1,107 @@ +#pragma once + +#include +#include +#include + +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::zero()).count()) SecondType; + typedef decltype(std::chrono::duration_cast(std::chrono::milliseconds::zero()).count()) MilisecondType; + typedef decltype(std::chrono::duration_cast(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; + + }; + + } +}