More statistics output.

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>

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

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;