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 + SparsePcaaQuery::~SparsePcaaQuery() { + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("Pareto Curve Approximation Algorithm terminated after " << this->refinementSteps.size() << " refinement steps." << std::endl); + } + } template SparsePcaaQuery::SparsePcaaQuery(preprocessing::SparseMultiObjectivePreprocessorResult& 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 Point; typedef std::vector 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()); offsetsToOverApproximation.resize(this->objectives.size(), storm::utility::zero()); optimalChoices.resize(transitionMatrix.getRowGroupCount(), 0); + + // Print some statistics (if requested) + if (storm::settings::getModule().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