From b8fc1130d106bb57cd6d84a0b17a2dbe2dba222f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 15 Jul 2019 17:03:46 +0200 Subject: [PATCH] Statistics via --statistics switch. --- .../DeterministicSchedsLpChecker.cpp | 20 +++++++++++++------ .../DeterministicSchedsLpChecker.h | 1 + .../DeterministicSchedsParetoExplorer.cpp | 10 ++++++++++ 3 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index fbc2744a2..939255f31 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -63,24 +63,28 @@ namespace storm { template DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper), numLpQueries(0) { + swAll.start(); swInit.start(); initializeLpModel(env); swInit.stop(); + swAll.stop(); } template std::string DeterministicSchedsLpChecker::getStatistics(std::string const& prefix) const { std::stringstream out; - out << prefix << swInit << " seconds for LP initialization" << std::endl; - out << prefix << swCheckWeightVectors << " seconds for checking weight vectors" << std::endl; - out << prefix << swCheckAreas << " seconds for checking areas" << std::endl; - out << prefix << swValidate << " seconds for validating LP solutions" << std::endl; - out << prefix << numLpQueries << " calls to LP optimization" << std::endl; + out << prefix << swAll << " seconds for LP Checker including... " << std::endl; + out << prefix << " " << swInit << " seconds for LP initialization" << std::endl; + out << prefix << " " << swCheckWeightVectors << " seconds for checking weight vectors" << std::endl; + out << prefix << " " << swCheckAreas << " seconds for checking areas" << std::endl; + out << prefix << " " << swValidate << " seconds for validating LP solutions" << std::endl; + out << prefix << " " << numLpQueries << " calls to LP optimization" << std::endl; return out.str(); } template void DeterministicSchedsLpChecker::setCurrentWeightVector(std::vector const& weightVector) { + swAll.start(); STORM_LOG_ASSERT(weightVector.size() == objectiveHelper.size(), "Setting a weight vector with invalid number of entries."); if (!currentWeightVector.empty()) { // Pop information of the current weight vector. @@ -102,10 +106,12 @@ namespace storm { } } lpModel->update(); + swAll.stop(); } template boost::optional> DeterministicSchedsLpChecker::check(storm::Environment const& env, Polytope overapproximation) { + swAll.start(); STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector."); STORM_LOG_TRACE("Checking a vertex..."); lpModel->push(); @@ -127,11 +133,13 @@ namespace storm { swValidate.stop(); } lpModel->pop(); + swAll.stop(); return result; } template std::pair>, std::vector>>> DeterministicSchedsLpChecker::check(storm::Environment const& env, storm::storage::geometry::PolytopeTree& polytopeTree, Point const& eps) { + swAll.start(); STORM_LOG_INFO("Checking " << polytopeTree.toString()); STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector."); if (polytopeTree.isEmpty()) { @@ -150,7 +158,7 @@ namespace storm { std::vector foundPoints; std::vector infeasableAreas; checkRecursive(env, polytopeTree, eps, foundPoints, infeasableAreas, 0); - + swAll.stop(); return {foundPoints, infeasableAreas}; } diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index ff11d54a4..54b01dd29 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -69,6 +69,7 @@ namespace storm { std::vector currentObjectiveVariables; std::vector currentWeightVector; + storm::utility::Stopwatch swAll; storm::utility::Stopwatch swInit; storm::utility::Stopwatch swCheckWeightVectors; storm::utility::Stopwatch swCheckAreas; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 5fb09c720..10f6fcdc6 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -12,6 +12,9 @@ #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/CoreSettings.h" + #include "storm/utility/export.h" #include "storm/utility/solver.h" @@ -341,6 +344,13 @@ namespace storm { paretoPoints.push_back(storm::utility::vector::convertNumericVector(transformObjectiveValuesToOriginal(objectives, p.second.get()))); } } + if (storm::settings::getModule().isShowStatisticsSet()) { + STORM_PRINT_AND_LOG("#STATS " << paretoPoints.size() << " Pareto points" << std::endl); + STORM_PRINT_AND_LOG("#STATS " << unachievableAreas.size() << " unachievable Areas" << std::endl); + STORM_PRINT_AND_LOG("#STATS " << overApproximation->getHalfspaces().size() << " unachievable Halfspaces" << std::endl); + STORM_PRINT_AND_LOG(lpChecker->getStatistics("#STATS ")); + + } return std::make_unique>(originalModelInitialState, std::move(paretoPoints), nullptr, nullptr); }