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

DeterministicSchedsParetoExplorer: Use StandardWeightVectorChecker for corner points.

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
9648d1a762
commit
2fe11c5165
2 changed files with 56 additions and 34 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 83
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
  2. 7
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h

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

@ -23,12 +23,12 @@ namespace storm {
namespace multiobjective { namespace multiobjective {
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType> const& coordinates) : coordinates(coordinates), onFacet(false) {
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType> const& coordinates) : coordinates(coordinates), onFacet(false), paretoOptimal(false) {
STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported"); STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported");
} }
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType>&& coordinates) : coordinates(std::move(coordinates)), onFacet(false) {
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType>&& coordinates) : coordinates(std::move(coordinates)), onFacet(false), paretoOptimal(false) {
STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported"); STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported");
} }
@ -94,6 +94,16 @@ namespace storm {
return onFacet; return onFacet;
} }
template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::setParetoOptimal(bool value) {
paretoOptimal = value;
}
template <class SparseModelType, typename GeometryValueType>
bool DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::isParetoOptimal() const {
return paretoOptimal;
}
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
std::string DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::toString(bool convertToDouble) const { std::string DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::toString(bool convertToDouble) const {
std::stringstream out; std::stringstream out;
@ -131,7 +141,8 @@ namespace storm {
break; break;
case Point::DominanceResult::Dominates: case Point::DominanceResult::Dominates:
if (pointsIt->second.liesOnFacet()) { if (pointsIt->second.liesOnFacet()) {
// Do not erase points that lie on a facet
// Do not erase points that lie on a facet. But flag it as non-optimal.
pointsIt->second.setParetoOptimal(false);
++pointsIt; ++pointsIt;
} else { } else {
pointsIt = points.erase(pointsIt); pointsIt = points.erase(pointsIt);
@ -147,11 +158,12 @@ namespace storm {
return pointsIt->first; return pointsIt->first;
} }
} }
// This point is not dominated by some other (known) point.
point.setParetoOptimal(true);
if (env.modelchecker().multi().isPrintResultsSet()) { if (env.modelchecker().multi().isPrintResultsSet()) {
std::cout << "## achievable point: [" << point.toString(true) << "]" << std::endl; std::cout << "## achievable point: [" << point.toString(true) << "]" << std::endl;
} }
points.emplace_hint(points.end(), currId, std::move(point)); points.emplace_hint(points.end(), currId, std::move(point));
return currId++; return currId++;
} }
@ -270,6 +282,7 @@ namespace storm {
objectiveHelper.emplace_back(*model, obj); objectiveHelper.emplace_back(*model, obj);
} }
lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(env, *model, objectiveHelper); lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(env, *model, objectiveHelper);
wvChecker = storm::modelchecker::multiobjective::WeightVectorCheckerFactory<SparseModelType>::create(preprocessorResult);
} }
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
@ -285,7 +298,9 @@ namespace storm {
std::vector<std::vector<ModelValueType>>paretoPoints; std::vector<std::vector<ModelValueType>>paretoPoints;
paretoPoints.reserve(pointset.size()); paretoPoints.reserve(pointset.size());
for (auto const& p : pointset) { for (auto const& p : pointset) {
paretoPoints.push_back(storm::utility::vector::convertNumericVector<ModelValueType>(transformObjectiveValuesToOriginal(objectives, p.second.get())));
if (p.second.isParetoOptimal()) {
paretoPoints.push_back(storm::utility::vector::convertNumericVector<ModelValueType>(transformObjectiveValuesToOriginal(objectives, p.second.get())));
}
} }
return std::make_unique<storm::modelchecker::ExplicitParetoCurveCheckResult<ModelValueType>>(originalModelInitialState, std::move(paretoPoints), nullptr, nullptr); return std::make_unique<storm::modelchecker::ExplicitParetoCurveCheckResult<ModelValueType>>(originalModelInitialState, std::move(paretoPoints), nullptr, nullptr);
} }
@ -301,7 +316,7 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::addHalfspaceToOverApproximation(Environment const& env, std::vector<GeometryValueType> const& normalVector, GeometryValueType const& offset) { void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::addHalfspaceToOverApproximation(Environment const& env, std::vector<GeometryValueType> const& normalVector, GeometryValueType const& offset) {
if (env.modelchecker().multi().isPrintResultsSet()) { if (env.modelchecker().multi().isPrintResultsSet()) {
std::cout << "## unachievable halfspace: [";
std::cout << "## overapproximation halfspace: [";
bool first = true; bool first = true;
for (auto const& xi : normalVector) { for (auto const& xi : normalVector) {
if (first) { if (first) {
@ -356,7 +371,7 @@ namespace storm {
std::vector<GeometryValueType> zeroRow(objectives.size(), storm::utility::zero<GeometryValueType>()); std::vector<GeometryValueType> zeroRow(objectives.size(), storm::utility::zero<GeometryValueType>());
std::vector<std::vector<GeometryValueType>> transformationMatrix(objectives.size(), zeroRow); std::vector<std::vector<GeometryValueType>> transformationMatrix(objectives.size(), zeroRow);
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
if (objectiveHelper[objIndex].minimizing()) {
transformationMatrix[objIndex][objIndex] = -storm::utility::one<GeometryValueType>(); transformationMatrix[objIndex][objIndex] = -storm::utility::one<GeometryValueType>();
} else { } else {
transformationMatrix[objIndex][objIndex] = storm::utility::one<GeometryValueType>(); transformationMatrix[objIndex][objIndex] = storm::utility::one<GeometryValueType>();
@ -368,7 +383,7 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::negateMinObjectives(std::vector<GeometryValueType>& vector) const { void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::negateMinObjectives(std::vector<GeometryValueType>& vector) const {
for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
if (objectiveHelper[objIndex].minimizing()) {
vector[objIndex] *= -storm::utility::one<ModelValueType>(); vector[objIndex] *= -storm::utility::one<ModelValueType>();
} }
} }
@ -379,13 +394,15 @@ namespace storm {
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
std::vector<GeometryValueType> weightVector(objectives.size(), storm::utility::zero<ModelValueType>()); std::vector<GeometryValueType> weightVector(objectives.size(), storm::utility::zero<ModelValueType>());
weightVector[objIndex] = storm::utility::one<GeometryValueType>(); weightVector[objIndex] = storm::utility::one<GeometryValueType>();
negateMinObjectives(weightVector);
lpChecker->setCurrentWeightVector(weightVector);
auto point = lpChecker->check(env, negateMinObjectives(this->overApproximation));
STORM_LOG_THROW(point.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation.");
negateMinObjectives(weightVector);
negateMinObjectives(point.get());
Point p(point.get());
//negateMinObjectives(weightVector);
wvChecker->check(env, storm::utility::vector::convertNumericVector<ModelValueType>(weightVector));
auto point = storm::utility::vector::convertNumericVector<GeometryValueType>(wvChecker->getUnderApproximationOfInitialStateResults());
//lpChecker->setCurrentWeightVector(weightVector);
//auto point = lpChecker->check(env, negateMinObjectives(this->overApproximation));
//STORM_LOG_THROW(point.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation.");
//negateMinObjectives(weightVector);
negateMinObjectives(point);
Point p(point);
p.setOnFacet(); p.setOnFacet();
// Adapt the overapproximation // Adapt the overapproximation
GeometryValueType offset = storm::utility::vector::dotProduct(weightVector, p.get()); GeometryValueType offset = storm::utility::vector::dotProduct(weightVector, p.get());
@ -412,7 +429,7 @@ namespace storm {
std::vector<GeometryValueType> result; std::vector<GeometryValueType> result;
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
ModelValueType value; ModelValueType value;
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
if (objectiveHelper[objIndex].minimizing()) {
value = -objectiveHelper[objIndex].getUpperValueBoundAtState(env, *model->getInitialStates().begin()); value = -objectiveHelper[objIndex].getUpperValueBoundAtState(env, *model->getInitialStates().begin());
} else { } else {
value = objectiveHelper[objIndex].getLowerValueBoundAtState(env, *model->getInitialStates().begin()); value = objectiveHelper[objIndex].getLowerValueBoundAtState(env, *model->getInitialStates().begin());
@ -424,10 +441,6 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType> template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::processFacet(Environment const& env, Facet& f) { void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::processFacet(Environment const& env, Facet& f) {
std::vector<GeometryValueType> weightVector = f.getHalfspace().normalVector();
negateMinObjectives(weightVector);
lpChecker->setCurrentWeightVector(weightVector);
if (optimizeAndSplitFacet(env,f)) { if (optimizeAndSplitFacet(env,f)) {
return; return;
} }
@ -442,12 +455,12 @@ namespace storm {
} }
} }
if (!polytopeTree.isEmpty()) { if (!polytopeTree.isEmpty()) {
lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector());
auto res = lpChecker->check(env, polytopeTree, eps); auto res = lpChecker->check(env, polytopeTree, eps);
for (auto const& infeasableArea : res.second) { for (auto const& infeasableArea : res.second) {
addUnachievableArea(env, negateMinObjectives(infeasableArea));
addUnachievableArea(env, infeasableArea);
} }
for (auto& achievablePoint : res.first) { for (auto& achievablePoint : res.first) {
negateMinObjectives(achievablePoint);
pointset.addPoint(env, Point(std::move(achievablePoint))); pointset.addPoint(env, Point(std::move(achievablePoint)));
} }
} }
@ -458,18 +471,20 @@ namespace storm {
// Invoke optimization and insert the explored points // Invoke optimization and insert the explored points
boost::optional<PointId> optPointId; boost::optional<PointId> optPointId;
auto currentArea = negateMinObjectives(overApproximation->intersection(f.getHalfspace().invert()));
auto point = lpChecker->check(env, currentArea);
if (point.is_initialized()) {
negateMinObjectives(point.get());
Point p(point.get());
p.setOnFacet();
GeometryValueType offset = storm::utility::vector::dotProduct(f.getHalfspace().normalVector(), p.get());
addHalfspaceToOverApproximation(env, f.getHalfspace().normalVector(), offset);
optPointId = pointset.addPoint(env, std::move(p));
} else {
addHalfspaceToOverApproximation(env, f.getHalfspace().normalVector(), f.getHalfspace().offset());
}
wvChecker->check(env, storm::utility::vector::convertNumericVector<ModelValueType>(f.getHalfspace().normalVector()));
auto point = storm::utility::vector::convertNumericVector<GeometryValueType>(wvChecker->getUnderApproximationOfInitialStateResults());
//auto currentArea = negateMinObjectives(overApproximation->intersection(f.getHalfspace().invert()));
//auto point = lpChecker->check(env, currentArea);
// if (point.is_initialized()) {
negateMinObjectives(point);
Point p(point);
p.setOnFacet();
GeometryValueType offset = storm::utility::vector::dotProduct(f.getHalfspace().normalVector(), p.get());
addHalfspaceToOverApproximation(env, f.getHalfspace().normalVector(), offset);
optPointId = pointset.addPoint(env, std::move(p));
//} else {
// addHalfspaceToOverApproximation(env, f.getHalfspace().normalVector(), f.getHalfspace().offset());
//}
// Potentially generate new facets // Potentially generate new facets
if (optPointId) { if (optPointId) {

7
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h
View File

@ -6,6 +6,7 @@
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h" #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h"
#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h" #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/storage/geometry/Polytope.h" #include "storm/storage/geometry/Polytope.h"
#include "storm/storage/geometry/Halfspace.h" #include "storm/storage/geometry/Halfspace.h"
@ -47,12 +48,17 @@ namespace storm {
void setOnFacet(bool value = true); void setOnFacet(bool value = true);
bool liesOnFacet() const; bool liesOnFacet() const;
void setParetoOptimal(bool value = true);
bool isParetoOptimal() const;
std::string toString(bool convertToDouble = false) const; std::string toString(bool convertToDouble = false) const;
private: private:
std::vector<GeometryValueType> coordinates; std::vector<GeometryValueType> coordinates;
bool onFacet; bool onFacet;
bool paretoOptimal;
}; };
@ -176,6 +182,7 @@ namespace storm {
std::vector<Polytope> unachievableAreas; std::vector<Polytope> unachievableAreas;
std::shared_ptr<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>> lpChecker; std::shared_ptr<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>> lpChecker;
std::unique_ptr<PcaaWeightVectorChecker<SparseModelType>> wvChecker;
std::vector<DeterministicSchedsObjectiveHelper<SparseModelType>> objectiveHelper; std::vector<DeterministicSchedsObjectiveHelper<SparseModelType>> objectiveHelper;
std::shared_ptr<SparseModelType> const& model; std::shared_ptr<SparseModelType> const& model;

Write Preview
Loading…
Cancel
Save