From 5213be9b69b6c68d66a9b16b7c6f36333d560ca0 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 2 Oct 2020 17:15:25 +0200
Subject: [PATCH] More statistics output.

---
 .../StandardMaPcaaWeightVectorChecker.cpp     |  6 ++++
 .../pcaa/StandardPcaaWeightVectorChecker.cpp  |  1 +
 .../SparseMultiObjectivePreprocessorResult.h  | 29 +++++++++++++------
 3 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
index 7a3455778..8b67a031a 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
@@ -10,6 +10,8 @@
 #include "storm/utility/SignalHandler.h"
 #include "storm/logic/Formulas.h"
 #include "storm/solver/SolverSelectionOptions.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
 
 #include "storm/environment/solver/SolverEnvironment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
@@ -63,6 +65,10 @@ namespace storm {
                         STORM_LOG_WARN_COND(this->objectives[objIndex].originalFormula->isProbabilityOperatorFormula() && this->objectives[objIndex].originalFormula->asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula(), "Objective " << this->objectives[objIndex].originalFormula << " was simplified to a cumulative reward formula. Correctness of the algorithm is unknown for this type of property.");
                     }
                 }
+                // Print some statistics (if requested)
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                    STORM_PRINT_AND_LOG("Final preprocessed model has " << markovianStates.getNumberOfSetBits() << " Markovian states." << std::endl);
+                }
             }
 
             template <class SparseMdpModelType>
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 0d7b6ab09..677b7987c 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -119,6 +119,7 @@ namespace storm {
                         }
                         STORM_PRINT_AND_LOG(numLraMecStates << " states lie on such an end component." << std::endl);
                     }
+                    STORM_PRINT_AND_LOG(std::endl);
                 }
             }
 
diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h
index 523098148..5b442b701 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h
@@ -38,23 +38,32 @@ namespace storm {
                         // Intentionally left empty
                     }
                     
-                    
-                    bool containsOnlyTotalRewardFormulas() const {
+                    uint64_t getNumberOfTotalRewardFormulas() const {
+                        uint64_t count = 0;
                         for (auto const& obj : objectives) {
-                            if (!obj.formula->isRewardOperatorFormula() || !obj.formula->getSubformula().isTotalRewardFormula()) {
-                                return false;
+                            if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) {
+                                ++count;
                             }
                         }
-                        return true;
+                        return count;
                     }
                     
-                    bool containsLongRunAverageRewardFormulas() const {
+                    bool containsOnlyTotalRewardFormulas() const {
+                        return getNumberOfTotalRewardFormulas() == objectives.size();
+                    }
+                    
+                    uint64_t getNumberOfLongRunAverageRewardFormulas() const {
+                        uint64_t count = 0;
                         for (auto const& obj : objectives) {
                             if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
-                                return true;
+                                ++count;
                             }
                         }
-                        return false;
+                        return count;
+                    }
+                    
+                    bool containsLongRunAverageRewardFormulas() const {
+                        return getNumberOfLongRunAverageRewardFormulas() > 0;
                     }
                     
                     bool containsOnlyTrivialObjectives() const {
@@ -88,12 +97,14 @@ namespace storm {
                         out << "--------------------------------------------------------------" << std::endl;
                         out << "\t" << originalFormula << std::endl;
                         out << std::endl;
-                        out << "Objectives:" << std::endl;
+                        out << "The query considers " << objectives.size() << " objectives:" << std::endl;
                         out << "--------------------------------------------------------------" << std::endl;
                         for (auto const& obj : objectives) {
                             obj.printToStream(out);
                             out << std::endl;
                         }
+                        out << "Number of Long-Run-Average Reward Objectives (after preprocessing): " << getNumberOfLongRunAverageRewardFormulas() << "." << std::endl;
+                        out << "Number of Total Reward Objectives (after preprocessing): " << getNumberOfTotalRewardFormulas() << "." << std::endl;
                         out << "--------------------------------------------------------------" << std::endl;
                         out << std::endl;
                         out << "Original Model Information:" << std::endl;