From 78237e8bb12130c7df9052adb8663ee82f3d3456 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 16 Jul 2019 14:26:03 +0200 Subject: [PATCH] LpChecker: Only build the LP model if it is actually needed. --- .../DeterministicSchedsLpChecker.cpp | 39 +++++++++++-------- .../DeterministicSchedsLpChecker.h | 8 ++-- .../DeterministicSchedsParetoExplorer.cpp | 14 +++---- .../DeterministicSchedsParetoExplorer.h | 2 +- .../multiObjectiveModelChecking.cpp | 2 +- 5 files changed, 37 insertions(+), 28 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index 721c05614..b121b68a2 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -24,24 +24,28 @@ namespace storm { namespace multiobjective { template - DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper), numLpQueries(0) { - if (env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) { - flowEncoding = true; - for (auto const& helper : objectiveHelper) { - if (!helper.isTotalRewardObjective()) { - flowEncoding = false; + DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(ModelType const& model, std::vector> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper), numLpQueries(0) { + // intentionally left empty + } + + template + void DeterministicSchedsLpChecker::initialize(Environment const& env) { + if (!lpModel) { + if (env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) { + flowEncoding = true; + for (auto const& helper : objectiveHelper) { + if (!helper.isTotalRewardObjective()) { + flowEncoding = false; + } } + } else { + flowEncoding = env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow; } - } else { - flowEncoding = env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow; + STORM_PRINT_AND_LOG("Using " << (flowEncoding ? "flow" : "classical") << " encoding." << std::endl); + swInit.start(); + initializeLpModel(env); + swInit.stop(); } - STORM_LOG_INFO_COND(flowEncoding, "Using classical encoding."); - STORM_LOG_INFO_COND(!flowEncoding, "Using flow encoding."); - swAll.start(); - swInit.start(); - initializeLpModel(env); - swInit.stop(); - swAll.stop(); } template @@ -57,8 +61,9 @@ namespace storm { } template - void DeterministicSchedsLpChecker::setCurrentWeightVector(std::vector const& weightVector) { + void DeterministicSchedsLpChecker::setCurrentWeightVector(Environment const& env, std::vector const& weightVector) { swAll.start(); + initialize(env); 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. @@ -86,6 +91,7 @@ namespace storm { template boost::optional> DeterministicSchedsLpChecker::check(storm::Environment const& env, Polytope overapproximation) { swAll.start(); + initialize(env); STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector."); STORM_LOG_TRACE("Checking a vertex..."); lpModel->push(); @@ -114,6 +120,7 @@ namespace storm { template std::pair>, std::vector>>> DeterministicSchedsLpChecker::check(storm::Environment const& env, storm::storage::geometry::PolytopeTree& polytopeTree, Point const& eps) { swAll.start(); + initialize(env); STORM_LOG_INFO("Checking " << polytopeTree.toString()); STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector."); if (polytopeTree.isEmpty()) { diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index 9e7ef2cd0..aa443f106 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -25,12 +25,12 @@ namespace storm { typedef typename std::shared_ptr> Polytope; typedef typename std::vector Point; - DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper); - + DeterministicSchedsLpChecker(ModelType const& model, std::vector> const& objectiveHelper); + /*! * Specifies the current direction. */ - void setCurrentWeightVector(std::vector const& weightVector); + void setCurrentWeightVector(Environment const& env, std::vector const& weightVector); /*! * Optimizes in the currently given direction @@ -51,6 +51,8 @@ namespace storm { std::string getStatistics(std::string const& prefix = "") const; private: + void initialize(Environment const& env); + bool processEndComponents(std::vector>& ecVars); void initializeLpModel(Environment const& env); diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 10f6fcdc6..1a5bcee4a 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -280,13 +280,13 @@ namespace storm { } template - DeterministicSchedsParetoExplorer::DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) { + DeterministicSchedsParetoExplorer::DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) { originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin(); objectiveHelper.reserve(objectives.size()); for (auto const& obj : objectives) { objectiveHelper.emplace_back(*model, obj); } - lpChecker = std::make_shared>(env, *model, objectiveHelper); + lpChecker = std::make_shared>(*model, objectiveHelper); if (preprocessorResult.containsOnlyTotalRewardFormulas()) { wvChecker = storm::modelchecker::multiobjective::WeightVectorCheckerFactory::create(preprocessorResult); } else { @@ -346,8 +346,8 @@ namespace storm { } 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("#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 ")); } @@ -449,7 +449,7 @@ namespace storm { point = storm::utility::vector::convertNumericVector(wvChecker->getUnderApproximationOfInitialStateResults()); negateMinObjectives(point); } else { - lpChecker->setCurrentWeightVector(weightVector); + lpChecker->setCurrentWeightVector(env, weightVector); auto optionalPoint = lpChecker->check(env, negateMinObjectives(this->overApproximation)); STORM_LOG_THROW(optionalPoint.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation."); point = std::move(optionalPoint.get()); @@ -494,7 +494,7 @@ namespace storm { template void DeterministicSchedsParetoExplorer::processFacet(Environment const& env, Facet& f) { if (!wvChecker) { - lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector()); + lpChecker->setCurrentWeightVector(env, f.getHalfspace().normalVector()); } if (optimizeAndSplitFacet(env, f)) { @@ -510,7 +510,7 @@ namespace storm { } if (!polytopeTree.isEmpty()) { if (wvChecker) { - lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector()); + lpChecker->setCurrentWeightVector(env, f.getHalfspace().normalVector()); } auto res = lpChecker->check(env, polytopeTree, eps); for (auto const& infeasableArea : res.second) { diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h index 68ea2511e..35ab48177 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h @@ -126,7 +126,7 @@ namespace storm { }; - DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); + DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); virtual std::unique_ptr check(Environment const& env); diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index 8c395ec5c..68e9fcd5e 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -53,7 +53,7 @@ namespace storm { { if (env.modelchecker().multi().isSchedulerRestrictionSet()) { STORM_LOG_THROW(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult::QueryType::Pareto, storm::exceptions::NotImplementedException, "Currently, only Pareto queries with scheduler restrictions are implemented."); - auto explorer = DeterministicSchedsParetoExplorer(env, preprocessorResult); + auto explorer = DeterministicSchedsParetoExplorer(preprocessorResult); result = explorer.check(env); if (env.modelchecker().multi().isExportPlotSet()) { explorer.exportPlotOfCurrentApproximation(env);