From 658f4a689876d8bf87c94899e98e6081b6466e24 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 15:32:17 +0200 Subject: [PATCH] DetScheds: 'better' reference point plus clean up --- .../DeterministicSchedsLpChecker.cpp | 11 +-- .../DeterministicSchedsLpChecker.h | 5 +- .../DeterministicSchedsParetoExplorer.cpp | 94 ++++++------------- .../DeterministicSchedsParetoExplorer.h | 28 ++---- 4 files changed, 40 insertions(+), 98 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index fac4052a5..d5391061b 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -9,9 +9,8 @@ namespace storm { namespace multiobjective { template - DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectives) : model(model) { + DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper) { swInit.start(); - initializeObjectiveHelper(objectives); initializeLpModel(env); swInit.stop(); } @@ -97,14 +96,6 @@ namespace storm { return {foundPoints, infeasableAreas}; } - template - void DeterministicSchedsLpChecker::initializeObjectiveHelper(std::vector> const& objectives) { - objectiveHelper.reserve(objectives.size()); - for (auto const& obj : objectives) { - objectiveHelper.emplace_back(model, obj); - } - } - template void DeterministicSchedsLpChecker::initializeLpModel(Environment const& env) { uint64_t numStates = model.getNumberOfStates(); diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index adf3079fd..d6a75a194 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -24,7 +24,7 @@ namespace storm { typedef typename std::shared_ptr> Polytope; typedef typename std::vector Point; - DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectives); + DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper); ~DeterministicSchedsLpChecker(); /*! @@ -45,13 +45,12 @@ namespace storm { std::pair, std::vector> check(storm::Environment const& env, storm::storage::geometry::PolytopeTree& polytopeTree, GeometryValueType const& eps); private: - void initializeObjectiveHelper(std::vector> const& objectives); void initializeLpModel(Environment const& env); void checkRecursive(storm::storage::geometry::PolytopeTree& polytopeTree, GeometryValueType const& eps, std::vector& foundPoints, std::vector& infeasableAreas); ModelType const& model; - std::vector> objectiveHelper; + std::vector> const& objectiveHelper; std::unique_ptr> lpModel; std::vector initialStateResults; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 2c7ca7ec5..b99a6b5c7 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -23,12 +23,12 @@ namespace storm { namespace multiobjective { template - DeterministicSchedsParetoExplorer::Point::Point(std::vector const& coordinates) : coordinates(coordinates), paretoOptimal(false), onFacet(false) { + DeterministicSchedsParetoExplorer::Point::Point(std::vector const& coordinates) : coordinates(coordinates), onFacet(false) { STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported"); } template - DeterministicSchedsParetoExplorer::Point::Point(std::vector&& coordinates) : coordinates(std::move(coordinates)), paretoOptimal(false), onFacet(false) { + DeterministicSchedsParetoExplorer::Point::Point(std::vector&& coordinates) : coordinates(std::move(coordinates)), onFacet(false) { STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported"); } @@ -84,16 +84,6 @@ namespace storm { } } - template - void DeterministicSchedsParetoExplorer::Point::setParetoOptimal(bool value) { - paretoOptimal = value; - } - - template - bool DeterministicSchedsParetoExplorer::Point::isParetoOptimal() const { - return paretoOptimal; - } - template void DeterministicSchedsParetoExplorer::Point::setOnFacet(bool value) { onFacet = value; @@ -123,19 +113,6 @@ namespace storm { return out.str(); } - // template - // bool operator<(typename DeterministicSchedsParetoExplorer::Point const& lhs, typename DeterministicSchedsParetoExplorer::Point const& rhs) { - // STORM_LOG_ASSERT(lhs.dimension() == rhs.dimension(), "Non-Equal dimensions of points: " << lhs << " vs. " << rhs); - // for (uint64_t i = 0; i < lhs.dimension(); ++i) { - // if (lhs.get()[i] < rhs.get()[i]) { - // return true; - // } else if (lhs.get()[i] != rhs.get()[i]) { - // return false; - // } - // } - // return false; - // } - template DeterministicSchedsParetoExplorer::Pointset::Pointset() : currId(1) { // Intentionally left empty @@ -153,11 +130,6 @@ namespace storm { ++pointsIt; break; case Point::DominanceResult::Dominates: - // Found a point in the set that is dominated by the new point, so we erase it - if (pointsIt->second.isParetoOptimal()) { - STORM_LOG_WARN("Potential precision issues: Found a point that dominates another point which was flagged as pareto optimal. Distance of points is " << std::sqrt(storm::utility::convertNumber(storm::storage::geometry::squaredEuclideanDistance(pointsIt->second.get(), point.get())))); - point.setParetoOptimal(true); - } if (pointsIt->second.liesOnFacet()) { // Do not erase points that lie on a facet ++pointsIt; @@ -169,9 +141,6 @@ namespace storm { // The new point is dominated by another point. return boost::none; case Point::DominanceResult::Equal: - if (point.isParetoOptimal()) { - pointsIt->second.setParetoOptimal(); - } if (point.liesOnFacet()) { pointsIt->second.setOnFacet(); } @@ -254,7 +223,6 @@ namespace storm { template void DeterministicSchedsParetoExplorer::Facet::addPoint(PointId const& pointId, Point const& point) { - inducedSimplex = nullptr; GeometryValueType product = storm::utility::vector::dotProduct(getHalfspace().normalVector(), point.get()); if (product != getHalfspace().offset()) { if (product < getHalfspace().offset()) { @@ -264,48 +232,44 @@ namespace storm { halfspace.offset() = product; } } - paretoPointsOnFacet.push_back(pointId); + pointsOnFacet.push_back(pointId); } template std::vector::PointId> const& DeterministicSchedsParetoExplorer::Facet::getPoints() const { - return paretoPointsOnFacet; + return pointsOnFacet; } template uint64_t DeterministicSchedsParetoExplorer::Facet::getNumberOfPoints() const { - return paretoPointsOnFacet.size(); + return pointsOnFacet.size(); } template - typename DeterministicSchedsParetoExplorer::Polytope const& DeterministicSchedsParetoExplorer::Facet::getInducedSimplex(Pointset const& pointset, std::vector const& referenceCoordinates) { - if (!inducedSimplex) { - std::vector> vertices = {referenceCoordinates}; - for (auto const& pId : paretoPointsOnFacet) { - vertices.push_back(pointset.getPoint(pId).get()); - } - // This facet might lie at the 'border', which means that the downward closure has to be taken in some directions - storm::storage::BitVector dimensionsForDownwardClosure = storm::utility::vector::filterZero(this->halfspace.normalVector()); - STORM_LOG_ASSERT(dimensionsForDownwardClosure.getNumberOfSetBits() + vertices.size() >= halfspace.normalVector().size() + 1, "The number of points on the facet is insufficient"); - if (dimensionsForDownwardClosure.empty()) { - inducedSimplex = storm::storage::geometry::Polytope::create(vertices); - } else { - inducedSimplex = storm::storage::geometry::Polytope::createSelectiveDownwardClosure(vertices, dimensionsForDownwardClosure); - } + typename DeterministicSchedsParetoExplorer::Polytope const& DeterministicSchedsParetoExplorer::Facet::getInducedPolytope(Pointset const& pointset, std::vector const& referenceCoordinates) { + std::vector> vertices = {referenceCoordinates}; + for (auto const& pId : pointsOnFacet) { + vertices.push_back(pointset.getPoint(pId).get()); + } + // This facet might lie at the 'border', which means that the downward closure has to be taken in some directions + storm::storage::BitVector dimensionsForDownwardClosure = storm::utility::vector::filterZero(this->halfspace.normalVector()); + STORM_LOG_ASSERT(dimensionsForDownwardClosure.getNumberOfSetBits() + vertices.size() >= halfspace.normalVector().size() + 1, "The number of points on the facet is insufficient"); + if (dimensionsForDownwardClosure.empty()) { + return storm::storage::geometry::Polytope::create(vertices); + } else { + return storm::storage::geometry::Polytope::createSelectiveDownwardClosure(vertices, dimensionsForDownwardClosure); } - return inducedSimplex; - } - - template - DeterministicSchedsParetoExplorer::FacetAnalysisContext::FacetAnalysisContext(Facet& f) : facet(f) { - // Intentionally left empty } template DeterministicSchedsParetoExplorer::DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) { originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin(); - lpChecker = std::make_shared>(env, *model, objectives); + objectiveHelper.reserve(objectives.size()); + for (auto const& obj : objectives) { + objectiveHelper.emplace_back(*model, obj); + } + lpChecker = std::make_shared>(env, *model, objectiveHelper); } template @@ -444,11 +408,15 @@ namespace storm { } template - std::vector DeterministicSchedsParetoExplorer::getReferenceCoordinates() const { + std::vector DeterministicSchedsParetoExplorer::getReferenceCoordinates(Environment const& env) const { std::vector result; - for (auto const& obj : objectives) { - // TODO: use objectiveHelper here. - ModelValueType value = storm::solver::minimize(obj.formula->getOptimalityType()) ? -obj.upperResultBound.get() : obj.lowerResultBound.get(); + for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { + ModelValueType value; + if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { + value = -objectiveHelper[objIndex].getUpperValueBoundAtState(env, *model->getInitialStates().begin()); + } else { + value = objectiveHelper[objIndex].getLowerValueBoundAtState(env, *model->getInitialStates().begin()); + } result.push_back(storm::utility::convertNumber(value)); } return result; @@ -466,7 +434,7 @@ namespace storm { GeometryValueType eps = storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); eps += eps; // The unknown area (box) can actually have size 2*eps - storm::storage::geometry::PolytopeTree polytopeTree(f.getInducedSimplex(pointset, getReferenceCoordinates())); + storm::storage::geometry::PolytopeTree polytopeTree(f.getInducedPolytope(pointset, getReferenceCoordinates(env))); for (auto const& point : pointset) { polytopeTree.substractDownwardClosure(point.second.get(), eps); if (polytopeTree.isEmpty()) { diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h index c283d9aa2..652806bbd 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h @@ -5,6 +5,7 @@ #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h" +#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h" #include "storm/storage/geometry/Polytope.h" #include "storm/storage/geometry/Halfspace.h" @@ -44,8 +45,6 @@ namespace storm { }; DominanceResult getDominance(Point const& other) const; - void setParetoOptimal(bool value = true); - bool isParetoOptimal() const; void setOnFacet(bool value = true); bool liesOnFacet() const; @@ -53,7 +52,6 @@ namespace storm { private: std::vector coordinates; - bool paretoOptimal; bool onFacet; }; @@ -114,27 +112,11 @@ namespace storm { /*! * Creates a polytope that captures all points that lie 'under' the facet */ - Polytope const& getInducedSimplex(Pointset const& pointset, std::vector const& referenceCoordinates); - - + Polytope const& getInducedPolytope(Pointset const& pointset, std::vector const& referenceCoordinates); private: storm::storage::geometry::Halfspace halfspace; - std::vector paretoPointsOnFacet; - Polytope inducedSimplex; - }; - - struct FacetAnalysisContext { - FacetAnalysisContext(Facet& f); - - Facet& facet; - std::set collectedPoints; - std::unique_ptr smtSolver; - std::shared_ptr expressionManager; - - // Variables that encode two points that lie in the induced simplex of the analyzed facet - // xMinusEps = (x_1-eps, x_m-eps) - std::vector x, xMinusEps; + std::vector pointsOnFacet; }; @@ -170,7 +152,7 @@ namespace storm { /*! * Gets reference coordinates used to subdividing the downwardclosure */ - std::vector getReferenceCoordinates() const; + std::vector getReferenceCoordinates(Environment const& env) const; /*! * Processes the given facet @@ -194,6 +176,8 @@ namespace storm { std::vector unachievableAreas; std::shared_ptr> lpChecker; + std::vector> objectiveHelper; + std::shared_ptr const& model; uint64_t originalModelInitialState; std::vector> const& objectives;