From c1c0fcf8f32fa49a54811a1b1cbbeb66f1f9e905 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 2 Oct 2020 12:37:26 +0200
Subject: [PATCH] Display a bit more statistics for multi-objective model
 checking.

---
 .../multiobjective/pcaa/SparsePcaaQuery.cpp     |  8 ++++++++
 .../multiobjective/pcaa/SparsePcaaQuery.h       |  2 +-
 .../pcaa/StandardPcaaWeightVectorChecker.cpp    | 17 +++++++++++++++++
 3 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
index a97905f7d..730a79c4e 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
@@ -8,6 +8,8 @@
 #include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h"
 #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
 #include "storm/storage/geometry/Hyperrectangle.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
 #include "storm/io/export.h"
@@ -18,6 +20,12 @@ namespace storm {
     namespace modelchecker {
         namespace multiobjective {
             
+            template <class SparseModelType, typename GeometryValueType>
+            SparsePcaaQuery<SparseModelType, GeometryValueType>::~SparsePcaaQuery() {
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                    STORM_PRINT_AND_LOG("Pareto Curve Approximation Algorithm terminated after " << this->refinementSteps.size() << " refinement steps." << std::endl);
+                }
+            }
             
             template <class SparseModelType, typename GeometryValueType>
             SparsePcaaQuery<SparseModelType, GeometryValueType>::SparsePcaaQuery(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) :
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
index b1fb9d359..7df4ff7bc 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
@@ -25,7 +25,7 @@ namespace storm {
                 typedef std::vector<GeometryValueType> Point;
                 typedef std::vector<GeometryValueType> WeightVector;
                 
-                virtual ~SparsePcaaQuery() = default;
+                virtual ~SparsePcaaQuery();
                 
                 /*
                  * Invokes the computation and retrieves the result
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 42c8f5ff8..0d7b6ab09 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -11,6 +11,8 @@
 #include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
 #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
 #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/macros.h"
@@ -103,6 +105,21 @@ namespace storm {
                 offsetsToUnderApproximation.resize(this->objectives.size(), storm::utility::zero<ValueType>());
                 offsetsToOverApproximation.resize(this->objectives.size(), storm::utility::zero<ValueType>());
                 optimalChoices.resize(transitionMatrix.getRowGroupCount(), 0);
+                
+                // Print some statistics (if requested)
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                    STORM_PRINT_AND_LOG("Weight Vector Checker Statistics:" << std::endl);
+                    STORM_PRINT_AND_LOG("Final preprocessed model has " << transitionMatrix.getRowGroupCount() << " states." << std::endl);
+                    STORM_PRINT_AND_LOG("Final preprocessed model has " << transitionMatrix.getRowCount() << " actions." << std::endl);
+                    if (lraMecDecomposition) {
+                        STORM_PRINT_AND_LOG("Found " << lraMecDecomposition->mecs.size() << " end components that are relevant for LRA-analysis." << std::endl);
+                        uint64_t numLraMecStates = 0;
+                        for (auto const& mec : this->lraMecDecomposition->mecs) {
+                            numLraMecStates += mec.size();
+                        }
+                        STORM_PRINT_AND_LOG(numLraMecStates << " states lie on such an end component." << std::endl);
+                    }
+                }
             }
 
             template <class SparseModelType>