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

fixes for nativepolytopes

tempestpy_adaptions
TimQu 8 years ago
parent
4642ed23be
commit
f01e48644e
8 changed files with 116 additions and 107 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. 2
      src/storm/adapters/Z3ExpressionAdapter.cpp
  2. 90
      src/storm/storage/geometry/NativePolytope.cpp
  3. 2
      src/storm/storage/geometry/NativePolytope.h
  4. 4
      src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp
  5. 109
      src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp
  6. 5
      src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h
  7. 7
      src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
  8. 4
      src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

2
src/storm/adapters/Z3ExpressionAdapter.cpp
View File

@ -125,7 +125,7 @@ namespace storm {
if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) {
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(num) / storm::utility::convertNumber<storm::RationalNumber>(den));
} else {
manager.rational(storm::utility::convertNumber<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr))));
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr))));
}
}
case Z3_OP_UNINTERPRETED:

90
src/storm/storage/geometry/NativePolytope.cpp
View File

@ -116,10 +116,12 @@ namespace storm {
template <typename ValueType>
bool NativePolytope<ValueType>::isEmpty() const {
if(emptyStatus == EmptyStatus::Unknown) {
storm::expressions::ExpressionManager manager;
std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(manager);
storm::expressions::Expression constraints = getConstraints(manager, declareVariables(manager, "x"));
solver->add(constraints);
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(*manager);
std::vector<storm::expressions::Expression> constraints = getConstraints(*manager, declareVariables(*manager, "x"));
for (auto const& constraint : constraints) {
solver->add(constraint);
}
switch(solver->check()) {
case storm::solver::SmtSolver::CheckResult::Sat:
emptyStatus = EmptyStatus::Nonempty;
@ -154,25 +156,37 @@ namespace storm {
template <typename ValueType>
bool NativePolytope<ValueType>::contains(std::shared_ptr<Polytope<ValueType>> const& other) const {
STORM_LOG_THROW(other->isNativePolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a NativePolytope and a different polytope implementation. This is not supported");
if (this->isUniversal()) {
return true;
} else if (other->isUniversal()) {
return false;
} else {
// Check whether there is one point in other that is not in this
storm::expressions::ExpressionManager manager;
std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(manager);
storm::expressions::Expression constraintsThis = this->getConstraints(manager, declareVariables(manager, "x"));
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
std::unique_ptr<storm::solver::SmtSolver> solver = storm::utility::solver::SmtSolverFactory().create(*manager);
std::vector<storm::expressions::Variable> variables = declareVariables(*manager, "x");
std::vector<storm::expressions::Expression> constraints = getConstraints(*manager, variables);
storm::expressions::Expression constraintsThis = manager->boolean(true);
for (auto const& constraint : constraints) {
constraintsThis = constraintsThis && constraint;
}
solver->add(!constraintsThis);
storm::expressions::Expression constraintsOther = dynamic_cast<NativePolytope<ValueType> const&>(*other).getConstraints(manager, declareVariables(manager, "y"));
solver->add(constraintsOther);
constraints = dynamic_cast<NativePolytope<ValueType> const&>(*other).getConstraints(*manager, variables);
for (auto const& constraint : constraints) {
solver->add(constraint);
}
switch(solver->check()) {
case storm::solver::SmtSolver::CheckResult::Sat:
return false;
case storm::solver::SmtSolver::CheckResult::Unsat:
return true;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected result of SMT solver during containment check of two polytopes.");
return false;
case storm::solver::SmtSolver::CheckResult::Sat:
return false;
case storm::solver::SmtSolver::CheckResult::Unsat:
return true;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected result of SMT solver during containment check of two polytopes.");
return false;
}
}
}
template <typename ValueType>
std::shared_ptr<Polytope<ValueType>> NativePolytope<ValueType>::intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
STORM_LOG_THROW(rhs->isNativePolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a NativePolytope and a different polytope implementation. This is not supported");
@ -188,8 +202,15 @@ namespace storm {
template <typename ValueType>
std::shared_ptr<Polytope<ValueType>> NativePolytope<ValueType>::intersection(Halfspace<ValueType> const& halfspace) const{
if(A.rows() == 0) {
// No constraints yet
EigenMatrix resultA = storm::adapters::EigenAdapter::toEigenVector(halfspace.normalVector()).transpose();
EigenVector resultb(1);
resultb(0) = halfspace.offset();
return std::make_shared<NativePolytope<ValueType>>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb));
}
EigenMatrix resultA(A.rows() + 1, A.cols());
resultA << A, storm::adapters::EigenAdapter::toEigenVector(halfspace.normalVector());
resultA << A, storm::adapters::EigenAdapter::toEigenVector(halfspace.normalVector()).transpose();
EigenVector resultb(resultA.rows());
resultb << b,
halfspace.offset();
@ -280,13 +301,20 @@ namespace storm {
template <typename ValueType>
std::pair<typename NativePolytope<ValueType>::Point, bool> NativePolytope<ValueType>::optimize(Point const& direction) const {
if(isUniversal()) {
return std::make_pair(Point(), false);
}
storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize);
std::vector<storm::expressions::Variable> variables;
variables.reserve(A.rows());
for (uint_fast64_t i = 0; i < A.rows(); ++i) {
variables.reserve(A.cols());
for (uint_fast64_t i = 0; i < A.cols(); ++i) {
variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction[i]));
}
solver.addConstraint("", getConstraints(solver.getManager(), variables));
std::vector<storm::expressions::Expression> constraints = getConstraints(solver.getManager(), variables);
for (auto const& constraint : constraints) {
solver.addConstraint("", constraint);
}
solver.update();
solver.optimize();
if (solver.isOptimal()) {
@ -304,14 +332,20 @@ namespace storm {
template <typename ValueType>
std::pair<typename NativePolytope<ValueType>::EigenVector, bool> NativePolytope<ValueType>::optimize(EigenVector const& direction) const {
if(isUniversal()) {
return std::make_pair(EigenVector(), false);
}
storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize);
std::vector<storm::expressions::Variable> variables;
variables.reserve(A.rows());
for (uint_fast64_t i = 0; i < A.rows(); ++i) {
variables.reserve(A.cols());
for (uint_fast64_t i = 0; i < A.cols(); ++i) {
variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction(i)));
}
solver.addConstraint("", getConstraints(solver.getManager(), variables));
std::vector<storm::expressions::Expression> constraints = getConstraints(solver.getManager(), variables);
for (auto const& constraint: constraints) {
solver.addConstraint("", constraint);
}
solver.update();
solver.optimize();
if (solver.isOptimal()) {
@ -348,14 +382,14 @@ namespace storm {
}
template <typename ValueType>
storm::expressions::Expression NativePolytope<ValueType>::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const {
storm::expressions::Expression result = manager.boolean(true);
std::vector<storm::expressions::Expression> NativePolytope<ValueType>::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const {
std::vector<storm::expressions::Expression> result;
for(uint_fast64_t row = 0; row < A.rows(); ++row) {
storm::expressions::Expression lhs = manager.rational(A(row,0)) * variables[0].getExpression();
for(uint_fast64_t col=1; col < A.cols(); ++col) {
lhs = lhs + manager.rational(A(row,col)) * variables[col].getExpression();
}
result = result && (lhs <= manager.rational(b(row)));
result.push_back(lhs <= manager.rational(b(row)));
}
return result;
}

2
src/storm/storage/geometry/NativePolytope.h
View File

@ -140,7 +140,7 @@ namespace storm {
std::vector<storm::expressions::Variable> declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const;
// returns the constrains defined by this polytope as an expresseion
storm::expressions::Expression getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const;
std::vector<storm::expressions::Expression> getConstraints(storm::expressions::ExpressionManager const& manager, std::vector<storm::expressions::Variable> const& variables) const;
//Stores whether the polytope is empty or not

4
src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp
View File

@ -28,9 +28,9 @@ namespace storm {
EigenMatrix subMatrix(dimension, dimension);
EigenVector subVector(dimension);
for (uint_fast64_t i : subset){
for (uint_fast64_t i = 0; i < dimension; ++i){
subMatrix.row(i) = constraintMatrix.row(subset[i]);
subVector.row(i) = constraintVector.row(subset[i]);
subVector(i) = constraintVector(subset[i]);
}
EigenVector point = subMatrix.fullPivLu().solve(subVector);

109
src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp
View File

@ -28,8 +28,7 @@ namespace storm {
} else {
// Generate initial set of d+1 affine independent points (if such a set exists)
std::vector<uint_fast64_t> vertexIndices;
uint_fast64_t minMaxVertexNumber;
if(this->findInitialVertices(points, vertexIndices, minMaxVertexNumber)) {
if(this->findInitialVertices(points, vertexIndices)) {
// compute point inside initial facet
EigenVector insidePoint(EigenVector::Zero(dimension));
for(uint_fast64_t vertexIndex : vertexIndices){
@ -40,21 +39,9 @@ namespace storm {
// Create the initial facets from the found vertices.
std::vector<Facet> facets = computeInitialFacets(points, vertexIndices, insidePoint);
// Enlarge the mesh by adding by first considering all points that are min (or max) in at least one dimension
// Enlarge the mesh
storm::storage::BitVector currentFacets(facets.size(), true);
storm::storage::BitVector consideredPoints(points.size(), false);
for(uint_fast64_t i = 0; i < minMaxVertexNumber; ++i) {
consideredPoints.set(i);
}
this->extendMesh(points, consideredPoints, facets, currentFacets, insidePoint);
for(auto & facet : facets){
facet.maxOutsidePointIndex = 0;
facet.outsideSet.clear();
}
// Now consider all points
consideredPoints = storm::storage::BitVector(points.size(), true);
this->extendMesh(points, consideredPoints, facets, currentFacets, insidePoint);
this->extendMesh(points, facets, currentFacets, insidePoint);
// Finally retrieve the resulting constrants
this->getPolytopeFromMesh(points, facets, currentFacets, generateRelevantVerticesAndVertexSets);
@ -140,10 +127,10 @@ namespace storm {
while(pointsAffineDependent) {
// get one hyperplane that holds all points
const uint_fast64_t dimension = points.front().rows();
EigenVector refPoint(points.front());
EigenVector refPoint = points.front();
EigenMatrix constraints(points.size() - 1, dimension);
for(unsigned row = 1; row < points.size(); ++row) {
constraints.row(row) = points[row] - refPoint;
constraints.row(row - 1) = points[row] - refPoint;
}
EigenVector normal = constraints.fullPivLu().kernel().col(0);
@ -162,12 +149,19 @@ namespace storm {
// Add the constraints obtained above
uint_fast64_t numOfAdditionalConstraints = additionalConstraints.size();
uint_fast64_t numOfRegularConstraints = resultMatrix.rows();
resultMatrix.resize(numOfRegularConstraints + numOfAdditionalConstraints, StormEigen::NoChange);
resultVector.resize(numOfRegularConstraints + numOfAdditionalConstraints, StormEigen::NoChange);
for(uint_fast64_t row = numOfRegularConstraints; row < numOfRegularConstraints + numOfAdditionalConstraints; ++row) {
resultMatrix.row(row) = std::move(additionalConstraints[row].first);
resultVector(row) = additionalConstraints[row].second;
EigenMatrix newA(numOfRegularConstraints + numOfAdditionalConstraints, resultMatrix.cols());
EigenVector newb(numOfRegularConstraints + numOfAdditionalConstraints);
uint_fast64_t row = 0;
for (; row < numOfRegularConstraints; ++ row) {
newA.row(row) = resultMatrix.row(row);
newb(row) = resultVector(row);
}
for(; row < numOfRegularConstraints + numOfAdditionalConstraints; ++row) {
newA.row(row) = std::move(additionalConstraints[row - numOfRegularConstraints].first);
newb(row) = additionalConstraints[row - numOfRegularConstraints].second;
}
resultMatrix = std::move(newA);
resultVector = std::move(newb);
// clear the additionally added points. Note that the order of the points might have changed
storm::storage::BitVector keptPoints(points.size(), true);
@ -199,53 +193,42 @@ namespace storm {
}
template<typename ValueType>
bool QuickHull<ValueType>::findInitialVertices(std::vector<EigenVector>& points, std::vector<uint_fast64_t>& verticesOfInitialPolytope, uint_fast64_t& minMaxVertices) const{
bool QuickHull<ValueType>::findInitialVertices(std::vector<EigenVector>& points, std::vector<uint_fast64_t>& verticesOfInitialPolytope) const{
const uint_fast64_t dimension = points.front().rows();
if(points.size() < dimension + 1){
//not enough points to obtain a (non-degenerated) polytope
return false;
}
const uint_fast64_t candidatesToFind = std::min(2*dimension, (uint_fast64_t) points.size());
uint_fast64_t candidatesFound = 0;
storm::storage::BitVector consideredPoints(points.size(), true);
while(candidatesFound < candidatesToFind && !consideredPoints.empty()) {
for(uint_fast64_t currDim=0; currDim<dimension; ++currDim) {
uint_fast64_t minIndex = *consideredPoints.begin();
uint_fast64_t maxIndex = minIndex;
for(uint_fast64_t pointIndex : consideredPoints){
//Check if the current point is a new minimum or maximum at the current dimension
if(points[minIndex](currDim) > points[pointIndex](currDim)){
// We first find some good candidates to get a (hopefully) large initial mesh.
storm::storage::BitVector notGoodCandidates(points.size(), true);
for(uint_fast64_t dim = 0; dim < dimension; ++dim) {
if(!notGoodCandidates.empty()) {
uint_fast64_t minIndex = *notGoodCandidates.begin();
uint_fast64_t maxIndex = *notGoodCandidates.begin();
for(uint_fast64_t pointIndex : notGoodCandidates) {
if(points[minIndex](dim) > points[pointIndex](dim)){
minIndex = pointIndex;
}
if(points[maxIndex](currDim) < points[pointIndex](currDim)){
if(points[maxIndex](dim) < points[pointIndex](dim)){
maxIndex = pointIndex;
}
}
consideredPoints.set(minIndex, false);
consideredPoints.set(maxIndex, false);
notGoodCandidates.set(minIndex, false);
notGoodCandidates.set(maxIndex, false);
}
//Found candidates. Now swap them to the front.
consideredPoints = ~consideredPoints;
const uint_fast64_t newNumberOfCandidates = consideredPoints.getNumberOfSetBits();
assert(newNumberOfCandidates > 0);
if(newNumberOfCandidates < points.size()){
uint_fast64_t nextPointToMove = consideredPoints.getNextSetIndex(newNumberOfCandidates);
for(uint_fast64_t indexAtFront = candidatesFound; indexAtFront < newNumberOfCandidates; ++indexAtFront){
if(!consideredPoints.get(indexAtFront)) {
assert(nextPointToMove != consideredPoints.size());
std::swap(points[indexAtFront], points[nextPointToMove]);
nextPointToMove = consideredPoints.getNextSetIndex(nextPointToMove+1);
consideredPoints.set(indexAtFront);
}
}
assert(nextPointToMove == consideredPoints.size());
}
if(candidatesFound==0){
//We are in the first iteration. It holds that the first newNumberOfCandidates points will be vertices of the final polytope
minMaxVertices = newNumberOfCandidates;
}
storm::storage::BitVector goodCandidates = ~notGoodCandidates;
//Found candidates. Now swap them to the front.
const uint_fast64_t numOfGoodCandidates = goodCandidates.getNumberOfSetBits();
for( auto const& goodCandidate : goodCandidates) {
if(goodCandidate >= numOfGoodCandidates) {
uint_fast64_t notGoodCandidate = *notGoodCandidates.begin();
assert(notGoodCandidate < numOfGoodCandidates);
std::swap(points[notGoodCandidate], points[goodCandidate]);
notGoodCandidates.set(notGoodCandidate, false);
}
candidatesFound = newNumberOfCandidates;
consideredPoints = ~consideredPoints;
}
storm::storage::geometry::SubsetEnumerator<std::vector<EigenVector>> subsetEnum(points.size(), dimension+1, points, affineFilter);
@ -295,10 +278,10 @@ namespace storm {
void QuickHull<ValueType>::computeNormalAndOffsetOfFacet(std::vector<EigenVector> const& points, EigenVector const& insidePoint, Facet& facet) const {
const uint_fast64_t dimension = points.front().rows();
assert(facet.points.size() == dimension);
EigenVector refPoint(facet.points.back());
EigenVector const& refPoint = points[facet.points.back()];
EigenMatrix constraints(dimension-1, dimension);
for(unsigned row = 0; row < dimension-1; ++row) {
constraints.row(row) = points[facet.points[row]] - refPoint;
constraints.row(row) = (points[facet.points[row]] - refPoint);
}
facet.normal = constraints.fullPivLu().kernel().col(0);
facet.offset = facet.normal.dot(refPoint);
@ -313,14 +296,13 @@ namespace storm {
template<typename ValueType>
void QuickHull<ValueType>::extendMesh(std::vector<EigenVector>& points,
storm::storage::BitVector& consideredPoints,
std::vector<Facet>& facets,
storm::storage::BitVector& currentFacets,
EigenVector& insidePoint) const {
storm::storage::BitVector currentOutsidePoints = consideredPoints;
storm::storage::BitVector currentOutsidePoints(points.size(), true);
// Compute initial outside Sets
for(uint_fast64_t facetIndex : currentFacets){
for (uint_fast64_t facetIndex : currentFacets) {
computeOutsideSetOfFacet(facets[facetIndex], currentOutsidePoints, points);
}
@ -332,7 +314,6 @@ namespace storm {
uint_fast64_t numberOfNewFacets = 0;
// Now we compute the enlarged mesh
uint_fast64_t farAwayPointIndex = facets[facetCount].maxOutsidePointIndex;
assert(consideredPoints.get(farAwayPointIndex));
// get Visible set from maxOutsidePoint of the current facet
std::set<uint_fast64_t> visibleSet = getVisibleSet(facets, facetCount, points[farAwayPointIndex]);
std::set<uint_fast64_t> invisibleSet = getInvisibleNeighbors(facets, visibleSet);

5
src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h
View File

@ -88,10 +88,9 @@ namespace storm {
*
* @param points The set of points from which vertices are picked. Note that the order of the points might be changed when calling this!!
* @param verticesOfInitialPolytope Will be set to the resulting vertices (represented by indices w.r.t. the given points)
* @param minMaxVertices after calling this, the first 'minMaxVertices' points will have an extreme value in at least one dimension
* @return true if the method was successful. False if the given points are affine dependend, i.e. the polytope is degenerated.
*/
bool findInitialVertices(std::vector<EigenVector>& points, std::vector<uint_fast64_t>& verticesOfInitialPolytope, uint_fast64_t& minMaxVertices) const;
bool findInitialVertices(std::vector<EigenVector>& points, std::vector<uint_fast64_t>& verticesOfInitialPolytope) const;
/*!
* Computes the initial facets out of the given dimension+1 initial vertices
@ -107,10 +106,8 @@ namespace storm {
* Extends the given mesh using the QuickHull-algorithm
* For optimization reasons a point thats inside of the initial polytope but on none of the facets has to be provided.
* @return true iff all consideredPoints are now contained by the mesh
*/
void extendMesh(std::vector<EigenVector>& points,
storm::storage::BitVector& consideredPoints,
std::vector<Facet>& facets,
storm::storage::BitVector& currentFacets,
EigenVector& insidePoint) const;

7
src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
View File

@ -95,7 +95,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) {
std::vector<double> j23 = {1.333333333,0.1978235137,0.1};
// we do our checks with rationals to avoid numerical issues when doing polytope computations...
auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(
auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::create(
std::vector<std::vector<storm::RationalNumber>>({storm::utility::vector::convertNumericVector<storm::RationalNumber>(j12),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j13),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j23)}));
@ -104,9 +104,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) {
std::vector<storm::RationalNumber> lb(3,-eps), ub(3,eps);
auto bloatingBox = storm::storage::geometry::Hyperrectangle<storm::RationalNumber>(lb,ub).asPolytope();
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues));
}
TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) {
@ -170,7 +168,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) {
std::vector<double> j23 = {0.3934717664, 0.01948095743};
// we do our checks with rationals to avoid numerical issues when doing polytope computations...
auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(
auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::create(
std::vector<std::vector<storm::RationalNumber>>({storm::utility::vector::convertNumericVector<storm::RationalNumber>(j12),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j13),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j23)}));
@ -179,7 +177,6 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) {
std::vector<storm::RationalNumber> lb(2,-eps), ub(2,eps);
auto bloatingBox = storm::storage::geometry::Hyperrectangle<storm::RationalNumber>(lb,ub).asPolytope();
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues));
}

4
src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp
View File

@ -1,7 +1,7 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#ifdef STORM_HAVE_HYPRO
#if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE
#include "storm/modelchecker/multiobjective/pcaa.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@ -110,4 +110,4 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) {
#endif /* STORM_HAVE_HYPRO */
#endif /* STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */
Write Preview
Loading…
Cancel
Save