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

DetScheds: 'better' reference point plus clean up

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
cd3290cb7d
commit
658f4a6898
4 changed files with 40 additions and 98 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. 11
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
  2. 5
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
  3. 94
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
  4. 28
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h

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

@ -9,9 +9,8 @@ namespace storm {
namespace multiobjective {
template <typename ModelType, typename GeometryValueType>
DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) : model(model) {
DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper) {
swInit.start();
initializeObjectiveHelper(objectives);
initializeLpModel(env);
swInit.stop();
}
@ -97,14 +96,6 @@ namespace storm {
return {foundPoints, infeasableAreas};
}
template <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initializeObjectiveHelper(std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) {
objectiveHelper.reserve(objectives.size());
for (auto const& obj : objectives) {
objectiveHelper.emplace_back(model, obj);
}
}
template <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initializeLpModel(Environment const& env) {
uint64_t numStates = model.getNumberOfStates();

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

@ -24,7 +24,7 @@ namespace storm {
typedef typename std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> Polytope;
typedef typename std::vector<GeometryValueType> Point;
DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper);
~DeterministicSchedsLpChecker();
/*!
@ -45,13 +45,12 @@ namespace storm {
std::pair<std::vector<Point>, std::vector<Polytope>> check(storm::Environment const& env, storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps);
private:
void initializeObjectiveHelper(std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
void initializeLpModel(Environment const& env);
void checkRecursive(storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas);
ModelType const& model;
std::vector<DeterministicSchedsObjectiveHelper<ModelType>> objectiveHelper;
std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper;
std::unique_ptr<storm::solver::LpSolver<ValueType>> lpModel;
std::vector<storm::expressions::Expression> initialStateResults;

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

@ -23,12 +23,12 @@ namespace storm {
namespace multiobjective {
template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType> const& coordinates) : coordinates(coordinates), paretoOptimal(false), onFacet(false) {
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType> const& coordinates) : coordinates(coordinates), onFacet(false) {
STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported");
}
template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType>&& coordinates) : coordinates(std::move(coordinates)), paretoOptimal(false), onFacet(false) {
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::Point(std::vector<GeometryValueType>&& 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 <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>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point::setOnFacet(bool value) {
onFacet = value;
@ -123,19 +113,6 @@ namespace storm {
return out.str();
}
// template <class SparseModelType, typename GeometryValueType>
// bool operator<(typename DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Point const& lhs, typename DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::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 <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::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<double>(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 <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::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 <class SparseModelType, typename GeometryValueType>
std::vector<typename DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::PointId> const& DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Facet::getPoints() const {
return paretoPointsOnFacet;
return pointsOnFacet;
}
template <class SparseModelType, typename GeometryValueType>
uint64_t DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Facet::getNumberOfPoints() const {
return paretoPointsOnFacet.size();
return pointsOnFacet.size();
}
template <class SparseModelType, typename GeometryValueType>
typename DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Polytope const& DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Facet::getInducedSimplex(Pointset const& pointset, std::vector<GeometryValueType> const& referenceCoordinates) {
if (!inducedSimplex) {
std::vector<std::vector<GeometryValueType>> 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<GeometryValueType>::create(vertices);
} else {
inducedSimplex = storm::storage::geometry::Polytope<GeometryValueType>::createSelectiveDownwardClosure(vertices, dimensionsForDownwardClosure);
}
typename DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Polytope const& DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::Facet::getInducedPolytope(Pointset const& pointset, std::vector<GeometryValueType> const& referenceCoordinates) {
std::vector<std::vector<GeometryValueType>> 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<GeometryValueType>::create(vertices);
} else {
return storm::storage::geometry::Polytope<GeometryValueType>::createSelectiveDownwardClosure(vertices, dimensionsForDownwardClosure);
}
return inducedSimplex;
}
template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::FacetAnalysisContext::FacetAnalysisContext(Facet& f) : facet(f) {
// Intentionally left empty
}
template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) {
originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin();
lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(env, *model, objectives);
objectiveHelper.reserve(objectives.size());
for (auto const& obj : objectives) {
objectiveHelper.emplace_back(*model, obj);
}
lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(env, *model, objectiveHelper);
}
template <class SparseModelType, typename GeometryValueType>
@ -444,11 +408,15 @@ namespace storm {
}
template <class SparseModelType, typename GeometryValueType>
std::vector<GeometryValueType> DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::getReferenceCoordinates() const {
std::vector<GeometryValueType> DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::getReferenceCoordinates(Environment const& env) const {
std::vector<GeometryValueType> 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<GeometryValueType>(value));
}
return result;
@ -466,7 +434,7 @@ namespace storm {
GeometryValueType eps = storm::utility::convertNumber<GeometryValueType>(env.modelchecker().multi().getPrecision());
eps += eps; // The unknown area (box) can actually have size 2*eps
storm::storage::geometry::PolytopeTree<GeometryValueType> polytopeTree(f.getInducedSimplex(pointset, getReferenceCoordinates()));
storm::storage::geometry::PolytopeTree<GeometryValueType> polytopeTree(f.getInducedPolytope(pointset, getReferenceCoordinates(env)));
for (auto const& point : pointset) {
polytopeTree.substractDownwardClosure(point.second.get(), eps);
if (polytopeTree.isEmpty()) {

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

@ -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<GeometryValueType> 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<GeometryValueType> const& referenceCoordinates);
Polytope const& getInducedPolytope(Pointset const& pointset, std::vector<GeometryValueType> const& referenceCoordinates);
private:
storm::storage::geometry::Halfspace<GeometryValueType> halfspace;
std::vector<PointId> paretoPointsOnFacet;
Polytope inducedSimplex;
};
struct FacetAnalysisContext {
FacetAnalysisContext(Facet& f);
Facet& facet;
std::set<PointId> collectedPoints;
std::unique_ptr<storm::solver::SmtSolver> smtSolver;
std::shared_ptr<storm::expressions::ExpressionManager> 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<storm::expressions::Variable> x, xMinusEps;
std::vector<PointId> pointsOnFacet;
};
@ -170,7 +152,7 @@ namespace storm {
/*!
* Gets reference coordinates used to subdividing the downwardclosure
*/
std::vector<GeometryValueType> getReferenceCoordinates() const;
std::vector<GeometryValueType> getReferenceCoordinates(Environment const& env) const;
/*!
* Processes the given facet
@ -194,6 +176,8 @@ namespace storm {
std::vector<Polytope> unachievableAreas;
std::shared_ptr<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>> lpChecker;
std::vector<DeterministicSchedsObjectiveHelper<SparseModelType>> objectiveHelper;
std::shared_ptr<SparseModelType> const& model;
uint64_t originalModelInitialState;
std::vector<Objective<ModelValueType>> const& objectives;

Write Preview
Loading…
Cancel
Save