sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Statistics via --statistics switch.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
55bf80d434
commit
b8fc1130d1
3 changed files with 25 additions and 6 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 20
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
  2. 1
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
  3. 10
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp

20
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
View File

@ -63,24 +63,28 @@ namespace storm {
template <typename ModelType, typename GeometryValueType>
DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper), numLpQueries(0) {
swAll.start();
swInit.start();
initializeLpModel(env);
swInit.stop();
swAll.stop();
}
template <typename ModelType, typename GeometryValueType>
std::string DeterministicSchedsLpChecker<ModelType, GeometryValueType>::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 <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::setCurrentWeightVector(std::vector<GeometryValueType> 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 <typename ModelType, typename GeometryValueType>
boost::optional<std::vector<GeometryValueType>> DeterministicSchedsLpChecker<ModelType, GeometryValueType>::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 <typename ModelType, typename GeometryValueType>
std::pair<std::vector<std::vector<GeometryValueType>>, std::vector<std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>>>> DeterministicSchedsLpChecker<ModelType, GeometryValueType>::check(storm::Environment const& env, storm::storage::geometry::PolytopeTree<GeometryValueType>& 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<Point> foundPoints;
std::vector<Polytope> infeasableAreas;
checkRecursive(env, polytopeTree, eps, foundPoints, infeasableAreas, 0);
swAll.stop();
return {foundPoints, infeasableAreas};
}

1
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
View File

@ -69,6 +69,7 @@ namespace storm {
std::vector<storm::expressions::Variable> currentObjectiveVariables;
std::vector<GeometryValueType> currentWeightVector;
storm::utility::Stopwatch swAll;
storm::utility::Stopwatch swInit;
storm::utility::Stopwatch swCheckWeightVectors;
storm::utility::Stopwatch swCheckAreas;

10
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
View File

@ -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<ModelValueType>(transformObjectiveValuesToOriginal(objectives, p.second.get())));
}
}
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().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<storm::modelchecker::ExplicitParetoCurveCheckResult<ModelValueType>>(originalModelInitialState, std::move(paretoPoints), nullptr, nullptr);
}

Write Preview
Loading…
Cancel
Save