From d90c14b8f532b58c5e1c395c87fc91c84ec002c4 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 27 Aug 2020 17:35:45 +0200
Subject: [PATCH] Added progress information for LRA computations

---
 .../infinitehorizon/SparseInfiniteHorizonHelper.cpp    | 10 ++++++++++
 1 file changed, 10 insertions(+)

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<ValueType> 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);
             }