From f01e48644efb74e88016ab1d06e88e4eafb320a4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Feb 2017 22:19:21 +0100 Subject: [PATCH] fixes for nativepolytopes --- src/storm/adapters/Z3ExpressionAdapter.cpp | 2 +- src/storm/storage/geometry/NativePolytope.cpp | 90 ++++++++++----- src/storm/storage/geometry/NativePolytope.h | 2 +- .../HyperplaneEnumeration.cpp | 4 +- .../nativepolytopeconversion/QuickHull.cpp | 109 ++++++++---------- .../nativepolytopeconversion/QuickHull.h | 5 +- .../SparseMaPcaaModelCheckerTest.cpp | 7 +- .../SparseMdpPcaaModelCheckerTest.cpp | 4 +- 8 files changed, 116 insertions(+), 107 deletions(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index 17740476d..d51da9888 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -125,7 +125,7 @@ namespace storm { if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { return manager.rational(storm::utility::convertNumber(num) / storm::utility::convertNumber(den)); } else { - manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); + return manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); } } case Z3_OP_UNINTERPRETED: diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index b148b5454..29f7b594f 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -116,10 +116,12 @@ namespace storm { template bool NativePolytope::isEmpty() const { if(emptyStatus == EmptyStatus::Unknown) { - storm::expressions::ExpressionManager manager; - std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create(manager); - storm::expressions::Expression constraints = getConstraints(manager, declareVariables(manager, "x")); - solver->add(constraints); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create(*manager); + std::vector 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 bool NativePolytope::contains(std::shared_ptr> 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 solver = storm::utility::solver::SmtSolverFactory().create(manager); - storm::expressions::Expression constraintsThis = this->getConstraints(manager, declareVariables(manager, "x")); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create(*manager); + std::vector variables = declareVariables(*manager, "x"); + std::vector 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 const&>(*other).getConstraints(manager, declareVariables(manager, "y")); - solver->add(constraintsOther); - + constraints = dynamic_cast 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 std::shared_ptr> NativePolytope::intersection(std::shared_ptr> 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 std::shared_ptr> NativePolytope::intersection(Halfspace 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>(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 std::pair::Point, bool> NativePolytope::optimize(Point const& direction) const { + if(isUniversal()) { + return std::make_pair(Point(), false); + } + storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector 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 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 std::pair::EigenVector, bool> NativePolytope::optimize(EigenVector const& direction) const { + if(isUniversal()) { + return std::make_pair(EigenVector(), false); + } storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector 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 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 - storm::expressions::Expression NativePolytope::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const { - storm::expressions::Expression result = manager.boolean(true); + std::vector NativePolytope::getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const { + std::vector 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; } diff --git a/src/storm/storage/geometry/NativePolytope.h b/src/storm/storage/geometry/NativePolytope.h index 55df8cbe6..28add2cf6 100644 --- a/src/storm/storage/geometry/NativePolytope.h +++ b/src/storm/storage/geometry/NativePolytope.h @@ -140,7 +140,7 @@ namespace storm { std::vector 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 const& variables) const; + std::vector getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const; //Stores whether the polytope is empty or not diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp index 4a10ba0a6..52dbad648 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp @@ -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); diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index ee90e3e08..f2dbbef36 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -28,8 +28,7 @@ namespace storm { } else { // Generate initial set of d+1 affine independent points (if such a set exists) std::vector 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 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 - bool QuickHull::findInitialVertices(std::vector& points, std::vector& verticesOfInitialPolytope, uint_fast64_t& minMaxVertices) const{ + bool QuickHull::findInitialVertices(std::vector& points, std::vector& 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 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> subsetEnum(points.size(), dimension+1, points, affineFilter); @@ -295,10 +278,10 @@ namespace storm { void QuickHull::computeNormalAndOffsetOfFacet(std::vector 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 void QuickHull::extendMesh(std::vector& points, - storm::storage::BitVector& consideredPoints, std::vector& 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 visibleSet = getVisibleSet(facets, facetCount, points[farAwayPointIndex]); std::set invisibleSet = getInvisibleNeighbors(facets, visibleSet); diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h index 337db40c6..f0cb8d5db 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.h @@ -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& points, std::vector& verticesOfInitialPolytope, uint_fast64_t& minMaxVertices) const; + bool findInitialVertices(std::vector& points, std::vector& 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& points, - storm::storage::BitVector& consideredPoints, std::vector& facets, storm::storage::BitVector& currentFacets, EigenVector& insidePoint) const; diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index edd02b2e4..5f03c77a1 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -95,7 +95,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { std::vector 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::createDownwardClosure( + auto expectedAchievableValues = storm::storage::geometry::Polytope::create( std::vector>({storm::utility::vector::convertNumericVector(j12), storm::utility::vector::convertNumericVector(j13), storm::utility::vector::convertNumericVector(j23)})); @@ -104,9 +104,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { std::vector lb(3,-eps), ub(3,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); - EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); - } TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { @@ -170,7 +168,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { std::vector 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::createDownwardClosure( + auto expectedAchievableValues = storm::storage::geometry::Polytope::create( std::vector>({storm::utility::vector::convertNumericVector(j12), storm::utility::vector::convertNumericVector(j13), storm::utility::vector::convertNumericVector(j23)})); @@ -179,7 +177,6 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { std::vector lb(2,-eps), ub(2,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); - EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } diff --git a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp index 1116997c9..52960434d 100644 --- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp @@ -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 */