From 746a58ff12f5049d2e500053a8d8a3aa24101068 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 27 Oct 2017 14:23:40 +0200
Subject: [PATCH] better statistics output
---
...dpRewardBoundedPcaaWeightVectorChecker.cpp | 20 +++++++++++++++++--
...eMdpRewardBoundedPcaaWeightVectorChecker.h | 15 ++------------
2 files changed, 20 insertions(+), 15 deletions(-)
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<SparseMdpModelType>::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 <class SparseMdpModelType>
+ SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::~SparseMdpRewardBoundedPcaaWeightVectorChecker() {
+ swAll.stop();
+ if (storm::settings::getModule<storm::settings::modules::CoreSettings>().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 <class SparseMdpModelType>
void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::check(std::vector<ValueType> const& weightVector) {
++numChecks;
@@ -212,7 +229,6 @@ namespace storm {
if (cachedData.schedulerChoices != choices) {
std::vector<uint64_t> choicesTmp = choices;
cachedData.minMaxSolver->setInitialScheduler(std::move(choicesTmp));
- ++numSchedChanges;
cachedData.schedulerChoices = choices;
storm::solver::GeneralLinearEquationSolverFactory<ValueType> 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<SparseMdpModelType> 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<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector, ValueType const& precision);
storm::utility::Stopwatch swAll, swEpochModelBuild, swEpochModelAnalysis;
- uint64_t numSchedChanges, numCheckedEpochs, numChecks;
+ uint64_t numCheckedEpochs, numChecks;
helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, false> rewardUnfolding;