diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 17d963813..2f76e3dae 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -14,6 +14,7 @@ #include "storm/utility/export.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/InvalidOperationException.h" @@ -33,11 +34,27 @@ namespace storm { STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported."); STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states."); - numSchedChanges = 0; numCheckedEpochs = 0; numChecks = 0; } + template + SparseMdpRewardBoundedPcaaWeightVectorChecker::~SparseMdpRewardBoundedPcaaWeightVectorChecker() { + swAll.stop(); + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("--------------------------------------------------" << std::endl); + STORM_PRINT_AND_LOG("Statistics:" << std::endl); + STORM_PRINT_AND_LOG("--------------------------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" #checked weight vectors: " << numChecks << "." << std::endl); + STORM_PRINT_AND_LOG(" #checked epochs overall: " << numCheckedEpochs << "." << std::endl); + STORM_PRINT_AND_LOG("# checked epochs per weight vector: " << numCheckedEpochs / numChecks << "." << std::endl); + STORM_PRINT_AND_LOG(" overall Time: " << swAll << "." << std::endl); + STORM_PRINT_AND_LOG(" Epoch Model building time: " << swEpochModelBuild << "." << std::endl); + STORM_PRINT_AND_LOG(" Epoch Model checking time: " << swEpochModelAnalysis << "." << std::endl); + STORM_PRINT_AND_LOG("--------------------------------------------------" << std::endl); + } + } + template void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(std::vector const& weightVector) { ++numChecks; @@ -212,7 +229,6 @@ namespace storm { if (cachedData.schedulerChoices != choices) { std::vector choicesTmp = choices; cachedData.minMaxSolver->setInitialScheduler(std::move(choicesTmp)); - ++numSchedChanges; cachedData.schedulerChoices = choices; storm::solver::GeneralLinearEquationSolverFactory linEqSolverFactory; bool needEquationSystem = linEqSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index 16ce8130d..531f8b37c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -27,18 +27,7 @@ namespace storm { SparseMdpRewardBoundedPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult const& preprocessorResult); - virtual ~SparseMdpRewardBoundedPcaaWeightVectorChecker() { - swAll.stop(); - std::cout << "WVC statistics: " << std::endl; - std::cout << " overall Time: " << swAll << "." << std::endl; - std::cout << "---------------------------------------------" << std::endl; - std::cout << " #checked weight vectors: " << numChecks << "." << std::endl; - std::cout << " #checked epochs: " << numCheckedEpochs << "." << std::endl; - std::cout << "#Sched reused from prev. ep.: " << (numCheckedEpochs - numSchedChanges) << "." << std::endl; - std::cout << " Epoch Model building time: " << swEpochModelBuild << "." << std::endl; - std::cout << " Epoch Model checking time: " << swEpochModelAnalysis << "." << std::endl; - } - + virtual ~SparseMdpRewardBoundedPcaaWeightVectorChecker(); /*! * - computes the optimal expected reward w.r.t. the weighted sum of the rewards of the individual objectives @@ -78,7 +67,7 @@ namespace storm { void updateCachedData(typename helper::rewardbounded::MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector, ValueType const& precision); storm::utility::Stopwatch swAll, swEpochModelBuild, swEpochModelAnalysis; - uint64_t numSchedChanges, numCheckedEpochs, numChecks; + uint64_t numCheckedEpochs, numChecks; helper::rewardbounded::MultiDimensionalRewardUnfolding rewardUnfolding;