diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp index 3ff9611da..846c19a58 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.cpp @@ -17,6 +17,8 @@ #include "storm/utility/SignalHandler.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" +#include "storm/utility/Stopwatch.h" +#include "storm/utility/ProgressMeasurement.h" #include "storm/environment/solver/LongRunAverageSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" @@ -133,13 +135,21 @@ namespace storm { createDecomposition(); // Compute the long-run average for all components in isolation. + // Set up some logging + std::string const componentString = (Nondeterministic ? std::string("Maximal end") : std::string("Bottom strongly connected")) + (_longRunComponentDecomposition->size() == 1 ? std::string(" component") : std::string(" components")); + storm::utility::ProgressMeasurement progress(componentString); + progress.setMaxCount( _longRunComponentDecomposition->size()); + progress.startNewMeasurement(0); + STORM_LOG_INFO("Computing long run average values for " << _longRunComponentDecomposition->size() << " " << componentString << " individually..."); std::vector componentLraValues; componentLraValues.reserve(_longRunComponentDecomposition->size()); for (auto const& c : *_longRunComponentDecomposition) { componentLraValues.push_back(computeLraForComponent(underlyingSolverEnvironment, stateRewardsGetter, actionRewardsGetter, c)); + progress.updateProgress(componentLraValues.size()); } // Solve the resulting SSP where end components are collapsed into single auxiliary states + STORM_LOG_INFO("Solving stochastic shortest path problem."); return buildAndSolveSsp(underlyingSolverEnvironment, componentLraValues); }