polytope adapter for hypro

Former-commit-id: c0972ad8ac

src/adapters/HyproAdapter.h

@@ -6,9 +6,10 @@
 
 #ifdef STORM_HAVE_HYPRO
 
-#include </Users/tim/hypro/src/lib/datastructures/Halfspace.h>
-//#include <lib/types.h>
-#include <lib/representations/Polytope/Polytope.h>
+#include <lib/datastructures/Halfspace.h>
+#include <lib/typedefs.h>
+#include <lib/representations/conversion/Converter.h>
+#include <lib/representations/Polytopes/HPolytope/HPolytope.h>
 
 #include "src/adapters/CarlAdapter.h"
 #include "src/storage/geometry/HalfSpace.h"
@@ -33,12 +34,14 @@ namespace storm {
         
         template <typename T>
         hypro::Halfspace<T> toHypro(storm::storage::geometry::Halfspace<T> const& h){
-            return hypro::Halfspace<T>(toHypro(h.normalVector()), h.offset());
+            T offset = h.offset();
+            return hypro::Halfspace<T>(toHypro(h.normalVector()), std::move(offset));
         }
         
         template <typename T>
-        hypro::Halfspace<T> fromHypro(hypro::Halfspace<T> const& h){
-            return storm::storage::geometry::Halfspace<T>(fromHypro(h.normal()), h.offset());
+        storm::storage::geometry::Halfspace<T> fromHypro(hypro::Halfspace<T> const& h){
+            T offset = h.offset();
+            return storm::storage::geometry::Halfspace<T>(fromHypro(h.normal()), std::move(offset));
         }
         
     }

src/storage/geometry/Halfspace.h

@@ -2,6 +2,8 @@
 #define STORM_STORAGE_GEOMETRY_HALFSPACE_H_
 
 #include <iostream>
+#include <iomanip>
+#include "src/utility/constants.h"
 #include "src/utility/vector.h"
 
 namespace storm {
@@ -25,18 +27,29 @@ namespace storm {
                     //Intentionally left empty
                 }
                 
+                /*
+                 * Returns true iff the given point is contained in this halfspace, i.e., normalVector*point <= offset holds.
+                 */
                 bool contains(std::vector<ValueType> const& point) {
-                    return storm::utility::vector::multiplyVectors(point, normalVector()) <= offset();
+                    return storm::utility::vector::dotProduct(point, normalVector()) <= offset();
                 }
 
-                std::string toString() {
+                /*
+                 * Returns a string representation of this Halfspace.
+                 * If the given flag is true, the occurring numbers are converted to double before printing to increase readability
+                 */
+                std::string toString(bool numbersAsDouble = false) const {
                     std::stringstream stream;
                     stream << "(";
                     for(auto it = normalVector().begin(); it != normalVector().end(); ++it){
                         if(it != normalVector().begin()){
                             stream << ", ";
                         }
-                        stream << *it;
+                        if(numbersAsDouble) {
+                            stream << std::setw(10) << storm::utility::convertNumber<double>(*it);
+                        } else {
+                            stream << std::setw(10) << *it;
+                        }
                     }
                     stream << ") * x <= " << offset();
                     return stream.str();

src/storage/geometry/Hyperrectangle.h

@@ -0,0 +1,77 @@
+#ifndef STORM_STORAGE_GEOMETRY_HYPERRECTANGLE_H_
+#define STORM_STORAGE_GEOMETRY_HYPERRECTANGLE_H_
+
+#include <iostream>
+#include <iomanip>
+
+#include "src/utility/macros.h"
+#include "src/storage/geometry/Polytope.h"
+#include "src/storage/geometry/Halfspace.h"
+#include "src/exceptions/InvalidArgumentException"
+
+namespace storm {
+    namespace storage {
+        namespace geometry {
+            
+            /* 
+             * This class represents a hyperrectangle, i.e., the intersection of finitely many intervals
+             */
+             
+            template <typename ValueType>
+            class Hyperrectangle {
+                
+            public:
+                
+                Hyperrectangle(std::vector<ValueType> const& lowerBounds, std::vector<ValueType> const& upperBounds) : mLowerBounds(lowerBounds), mUpperBounds(upperBounds) {
+                    STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a hyperrectangle but the number of given lower bounds does not equal the number of given upper bounds.");
+                }
+                
+                Hyperrectangle(std::vector<ValueType>&& lowerBounds, std::vector<ValueType>&& upperBounds) : mLowerBounds(lowerBounds), mUpperBounds(upperBounds) {
+                    STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a hyperrectangle but the number of given lower bounds does not equal the number of given upper bounds.");
+                }
+                
+                std::vector<ValueType> const& lowerBounds() const {
+                    return mLowerBounds;
+                }
+                
+                std::vector<ValueType>& lowerBounds(){
+                    return mLowerBounds;
+                }
+                
+                std::vector<ValueType> const& upperBounds() const {
+                    return mUpperBounds;
+                }
+                
+                std::vector<ValueType>& upperBounds(){
+                    return mUpperBounds;
+                }
+                
+                std::shared_ptr<Polytope<ValueType>> asPolytope() const {
+                    STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a polytope form a hyperrectangle but the numbers of given lower and upper bounds do not match.");
+                    std::vector<Halfspace<ValueType>> halfspaces;
+                    halfspaces.reserve(2*lowerBounds.size());
+                    for(uint_fast64_t i = 0; i<lowerBounds.size(); ++i) {
+                        std::vector<ValueType> direction(lowerBounds.size(), storm::utility::zero<ValueType>());
+                        direction[i] = -storm::utility::one<ValueType>();
+                        ValueType offset = -lowerBounds()[i];
+                        halfspaces.emplace_back(std::move(direction), std::move(offset));
+                        
+                        direction = std::vector<ValueType>(lowerBounds.size(), storm::utility::zero<ValueType>());
+                        direction[i] = storm::utility::one<ValueType>();
+                        offset = upperBounds()[i];
+                        halfspaces.emplace_back(std::move(direction), std::move(offset));
+                    }
+                    return Polytope<ValueType>::create(halfspaces);
+                }
+                
+            private:
+                
+                std::vector<ValueType> mLowerBounds;
+                std::vector<ValueType> mUpperBounds;
+                
+            };
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_GEOMETRY_HYPERRECTANGLE_H_ */

src/storage/geometry/HyproPolytope.cpp

@@ -0,0 +1,195 @@
+#include "src/storage/geometry/HyproPolytope.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/UnexpectedException.h"
+
+namespace storm {
+    namespace storage {
+        namespace geometry {
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::HyproPolytope(std::vector<Halfspace<ValueType>> const& halfspaces) {
+                if(halfspaces.empty()){
+                    internPolytope = HyproPolytopeType();
+                } else {
+                    std::vector<hypro::Halfspace<ValueType>> hyproHalfspaces;
+                    hyproHalfspaces.reserve(halfspaces.size());
+                    for(auto& h : halfspaces) {
+                        hyproHalfspaces.emplace_back(storm::adapters::toHypro(h));
+                    }
+                    internPolytope = HyproPolytopeType(std::move(hyproHalfspaces));
+                }
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::HyproPolytope(std::vector<Point> const& points) {
+                if(points.empty()){
+                    internPolytope = HyproPolytopeType::Empty();
+                } else {
+                    std::vector<hypro::Point<ValueType>> hyproPoints;
+                    hyproPoints.reserve(points.size());
+                    for(auto const& p : points){
+                        hyproPoints.emplace_back(storm::adapters::toHypro(p));
+                    }
+                    internPolytope = HyproPolytopeType(std::move(hyproPoints));
+                }
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
+                                                                             boost::optional<std::vector<Point>> const& points) {
+                if(halfspaces) {
+                    STORM_LOG_WARN_COND(!points, "Creating a HyproPolytope where halfspaces AND points are given. The points will be ignored.");
+                    return std::make_shared<HyproPolytope<ValueType>>(*halfspaces);
+                } else if(points) {
+                    return std::make_shared<HyproPolytope<ValueType>>(*points);
+                }
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Creating a HyproPolytope but no representation was given.");
+                return nullptr;
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::HyproPolytope(HyproPolytope<ValueType> const& other) : internPolytope(other.internPolytope) {
+                // Intentionally left empty
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::HyproPolytope(HyproPolytope<ValueType>&& other) : internPolytope(std::move(other.internPolytope)) {
+                // Intentionally left empty
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::HyproPolytope(HyproPolytopeType const& p) : internPolytope(p) {
+                // Intentionally left empty
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::HyproPolytope(HyproPolytopeType&& p) : internPolytope(p) {
+                // Intentionally left empty
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>::~HyproPolytope() {
+                // Intentionally left empty
+            }
+            
+            template <typename ValueType>
+            std::vector<typename Polytope<ValueType>::Point> HyproPolytope<ValueType>::getVertices() const {
+                std::vector<hypro::Point<ValueType>> hyproVertices = internPolytope.vertices();
+                std::vector<Point> result;
+                result.reserve(hyproVertices.size());
+                for(auto const& p : hyproVertices) {
+                    result.push_back(storm::adapters::fromHypro(p.rawCoordinates()));
+                }
+                return result;
+            }
+            
+            template <typename ValueType>
+            std::vector<Halfspace<ValueType>> HyproPolytope<ValueType>::getHalfspaces() const {
+                std::vector<hypro::Halfspace<ValueType>> hyproHalfspaces = internPolytope.constraints();
+                std::vector<Halfspace<ValueType>> result;
+                result.reserve(hyproHalfspaces.size());
+                for(auto const& h : hyproHalfspaces) {
+                    result.push_back(storm::adapters::fromHypro(h));
+                }
+                return result;
+            }
+            
+            template <typename ValueType>
+            bool HyproPolytope<ValueType>::isEmpty() const {
+                return internPolytope.empty();
+            }
+            
+            template <typename ValueType>
+            bool HyproPolytope<ValueType>::isUniversal() const {
+                return internPolytope.constraints().empty();
+            }
+            
+            template <typename ValueType>
+            bool HyproPolytope<ValueType>::contains(Point const& point) const{
+                return internPolytope.contains(storm::adapters::toHypro(point));
+            }
+            
+            template <typename ValueType>
+            bool HyproPolytope<ValueType>::contains(std::shared_ptr<Polytope<ValueType>> const& other) const {
+                STORM_LOG_THROW(other->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported");
+                return internPolytope.contains(other->asHyproPolytope().internPolytope);
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
+                STORM_LOG_THROW(rhs->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported");
+                return std::make_shared<HyproPolytope<ValueType>>(internPolytope.intersect(rhs->asHyproPolytope().internPolytope));
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::intersection(Halfspace<ValueType> const& halfspace) const{
+                HyproPolytopeType result(internPolytope);
+                result.insert(storm::adapters::toHypro(halfspace));
+                return std::make_shared<HyproPolytope<ValueType>>(std::move(result));
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
+                STORM_LOG_THROW(rhs->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported");
+                return std::make_shared<HyproPolytope<ValueType>>(internPolytope.unite(rhs->asHyproPolytope().internPolytope));
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
+                STORM_LOG_THROW(rhs->isHyproPolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a HyproPolytope and a different polytope implementation. This is not supported");
+                return std::make_shared<HyproPolytope<ValueType>>(internPolytope.minkowskiSum(rhs->asHyproPolytope().internPolytope));
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::downwardClosure(boost::optional<Point> const& upperBounds) const {
+                if(this->isUniversal() || this->isEmpty()) {
+                    // In these cases, the polytope does not change, i.e., we return a copy of this
+                    return std::make_shared<HyproPolytope<ValueType>>(internPolytope);
+                }
+                // Only keep the halfspaces where all entries of the normal vector are non-negative
+                std::vector<hypro::Halfspace<ValueType>> halfspaces;
+                for(auto& h : internPolytope.constraints()){
+                    if((h.normal().array() >= storm::utility::zero<ValueType>()).all()){
+                        halfspaces.push_back(h);
+                    }
+                }
+                // Add Halfspaces to bound the polytope in each (positive) direction
+                for(uint_fast64_t dim = 0; dim < internPolytope.dimension(); ++dim){
+                    hypro::vector_t<ValueType> direction = hypro::vector_t<ValueType>::Zero(dim);
+                    direction(dim) = storm::utility::one<ValueType>();
+                    if(upperBounds){
+                        ValueType upperBound = (*upperBounds)[dim];
+                        halfspaces.emplace_back(std::move(direction), std::move(upperBound));
+                    } else {
+                        // Compute max{x_dim | x \in P }
+                        hypro::EvaluationResult<ValueType> evalRes = internPolytope.evaluate(direction);
+                        switch (evalRes.errorCode) {
+                            case hypro::SOLUTION::FEAS:
+                                halfspaces.emplace_back(std::move(direction), std::move(evalRes.supportValue));
+                                break;
+                            case hypro::SOLUTION::INFTY:
+                                // if this polytope is not bounded in the current direction, no halfspace needs to be added
+                                break;
+                            default:
+                                // there should never be an infeasible solution as we already excluded the empty polytope.
+                                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected eror code for Polytope evaluation");
+                                break;
+                        }
+                    }
+                }
+                return std::make_shared<HyproPolytope<ValueType>>(HyproPolytopeType(std::move(halfspaces)));
+            }
+            
+            template <typename ValueType>
+            bool HyproPolytope<ValueType>::isHyproPolytope() const {
+                return true;
+            }
+            
+#ifdef STORM_HAVE_CARL
+            template class HyproPolytope<storm::RationalNumber>;
+#endif
+        }
+    }
+}

src/storage/geometry/HyproPolytope.h

@@ -0,0 +1,124 @@
+#ifndef STORM_STORAGE_GEOMETRY_HYPROPOLYTOPE_H_
+#define STORM_STORAGE_GEOMETRY_HYPROPOLYTOPE_H_
+
+#include "src/storage/geometry/Polytope.h"
+#include "src/adapters/HyproAdapter.h"
+
+#ifdef STORM_HAVE_HYPRO
+
+namespace storm {
+    namespace storage {
+        namespace geometry {
+            
+            template <typename ValueType>
+            class HyproPolytope : public Polytope<ValueType> {
+            public:
+                
+                typedef typename Polytope<ValueType>::Point Point;
+                typedef hypro::HPolytope<ValueType> HyproPolytopeType;
+                
+                /*!
+                 * Creates a HyproPolytope from the given halfspaces or points.
+                 * If both representations are given, one of them might be ignored
+                 */
+                static std::shared_ptr<Polytope<ValueType>> create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
+                                                                   boost::optional<std::vector<Point>> const& points);
+                
+                /*!
+                 * Creates a HyproPolytope from the given halfspaces
+                 * The resulting polytope is defined as the intersection of the halfspaces.
+                 */
+                HyproPolytope(std::vector<Halfspace<ValueType>> const& halfspaces);
+                
+                /*!
+                 * Creates a HyproPolytope from the given points.
+                 * The resulting polytope is defined as the convex hull of the points'
+                 */
+                HyproPolytope(std::vector<Point> const& points);
+                
+                /*!
+                 * Copy and move constructors
+                 */
+                HyproPolytope(HyproPolytope<ValueType> const& other);
+                HyproPolytope(HyproPolytope<ValueType>&& other);
+                
+                /*!
+                 * Construction from a plain hypro polytope
+                 */
+                HyproPolytope(HyproPolytopeType const& polytope);
+                HyproPolytope(HyproPolytopeType&& polytope);
+                
+                ~HyproPolytope();
+
+                /*!
+                 * Returns the vertices of this polytope.
+                 */
+                virtual std::vector<Point> getVertices() const override;
+                
+                /*!
+                 * Returns the halfspaces of this polytope.
+                 */
+                virtual std::vector<Halfspace<ValueType>> getHalfspaces() const override;
+                
+                
+                /*!
+                 * Returns whether this polytope is the empty set.
+                 */
+                virtual bool isEmpty() const override;
+                
+                /*!
+                 * Returns whether this polytope is universal (i.e., equals R^n).
+                 */
+                virtual bool isUniversal() const override;
+                
+                /*!
+                 * Returns true iff the given point is inside of the polytope.
+                 */
+                virtual bool contains(Point const& point) const override;
+                
+                /*!
+                 * Returns true iff the given polytope is a subset of this polytope.
+                 */
+                virtual bool contains(std::shared_ptr<Polytope<ValueType>> const& other) const override;
+                
+                /*!
+                 * Intersects this polytope with rhs and returns the result.
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
+                virtual std::shared_ptr<Polytope<ValueType>> intersection(Halfspace<ValueType> const& halfspace) const override;
+                
+                /*!
+                 * Returns the convex union of this polytope and rhs.
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
+                
+                /*!
+                 * Returns the minkowskiSum of this polytope and rhs.
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
+                
+                /*!
+                 * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope.
+                 * Put differently, the resulting polytope corresponds to this polytope, where
+                 * 1. a vector y with y_i=max{x_i | x \in P} is computed and for each i, a halfspace with offset y_i and
+                 *    normal vector n (where n_i = 1 and the remaining entries are 0) is inserted.
+                 * 2. all halfspaces where the normal vector has at least one negative entry are removed
+                 *
+                 * @param upperBounds If given, this vector is considered for y (hence, max{x_i | x i \in P does not need to be computed)
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> downwardClosure(boost::optional<Point> const& upperBounds = boost::none) const override;
+            
+                virtual bool isHyproPolytope() const override;
+                
+            private:
+                
+                HyproPolytopeType internPolytope;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_HAVE_HYPRO */
+
+#endif /* STORM_STORAGE_GEOMETRY_HYPROPOLYTOPE_H_ */

src/storage/geometry/Polytope.cpp

@@ -1,7 +1,10 @@
 #include "src/storage/geometry/Polytope.h"
 
-#include "src/utility/macros.h"
+#include <iostream>
+
 #include "src/adapters/HyproAdapter.h"
+#include "src/storage/geometry/HyproPolytope.h"
+#include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
@@ -9,83 +12,128 @@ namespace storm {
         namespace geometry {
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(std::vector<storm::storage::geometry::Halfspace<ValueType>> const& halfspaces){
-                return create(halfspaces, boost::none, false);
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(std::vector<storm::storage::geometry::Halfspace<ValueType>> const& halfspaces) {
+                return create(halfspaces, boost::none);
             }
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(std::vector<Point> const& points){
-                return create(boost::none, points, false);
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(std::vector<Point> const& points) {
+                return create(boost::none, points);
             }
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::createDownwardClosure(std::vector<Halfspace<ValueType>> const& halfspaces){
-                return create(halfspaces, boost::none, false);
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
+                                                                             boost::optional<std::vector<Point>> const& points) {
+#ifdef STORM_HAVE_HYPRO
+                return HyproPolytope<ValueType>::create(halfspaces, points);
+#endif
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified.");
+                return nullptr;
             }
             
+            //Protected  default constructor
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::createDownwardClosure(std::vector<Point> const& points){
-                return create(boost::none, points, true);
+            Polytope<ValueType>::Polytope() {
+                // Intentionally left empty
             }
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
-                                                                             boost::optional<std::vector<Point>> const& points,
-                                                                             bool downwardClosure) {
-                
-#ifdef STORM_HAVE_HYPRO
-                std::cout << "HyPro available!!" << std::endl;
-                // return std::make_shared(HyproPolytope<ValueType>(halfspaces, points, downwardClosure));
-#endif
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified.");
-                return nullptr;
+            Polytope<ValueType>::~Polytope() {
+                // Intentionally left empty
             }
             
             template <typename ValueType>
-            std::vector<typename Polytope<ValueType>::Point> Polytope<ValueType>::getVertices(){
+            std::vector<typename Polytope<ValueType>::Point> Polytope<ValueType>::getVertices() const{
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return std::vector<Point>();
             }
             
             template <typename ValueType>
-            std::vector<Halfspace<ValueType>> Polytope<ValueType>::getHalfspaces(){
+            std::vector<Halfspace<ValueType>> Polytope<ValueType>::getHalfspaces() const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return std::vector<Halfspace<ValueType>>();
             }
             
             template <typename ValueType>
-            bool Polytope<ValueType>::contains(Point const& point) const{
+            bool Polytope<ValueType>::isEmpty() const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return false;
             }
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::intersect(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
+            bool Polytope<ValueType>::isUniversal() const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return false;
             }
+            
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::intersect(Halfspace<ValueType> const& rhs) const{
+            bool Polytope<ValueType>::contains(Point const& point) const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return false;
             }
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
+            bool Polytope<ValueType>::contains(std::shared_ptr<Polytope<ValueType>> const& other) const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return false;
             }
+            
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::convexUnion(Point const& rhs) const{
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return nullptr;
             }
             
             template <typename ValueType>
-            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::bloat(Point const& point1, Point const& point2) const{
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::intersection(Halfspace<ValueType> const& halfspace) const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return nullptr;
             }
             
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return nullptr;
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return nullptr;
+            }
             
             template <typename ValueType>
-            std::string Polytope<ValueType>::toString() const{
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::downwardClosure(boost::optional<Point> const& upperBounds) const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return nullptr;
+            }
+            
+            template <typename ValueType>
+            std::string Polytope<ValueType>::toString(bool numbersAsDouble) const {
+                auto halfspaces = this->getHalfspaces();
+                std::stringstream stream;
+                stream << "Polytope with " << halfspaces.size() << " Halfspaces" << (halfspaces.empty() ? "" : ":") << std::endl;
+                for (auto const& h : halfspaces) {
+                    stream << "|   " << h.toString(numbersAsDouble) << std::endl;
+                }
+                return stream.str();
+            }
+            
+            template <typename ValueType>
+            bool Polytope<ValueType>::isHyproPolytope() const {
+                return false;
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType> const& Polytope<ValueType>::asHyproPolytope() const {
+                return dynamic_cast<HyproPolytope<ValueType> const&>(*this);
+            }
+            
+            template <typename ValueType>
+            HyproPolytope<ValueType>& Polytope<ValueType>::asHyproPolytope() {
+                return dynamic_cast<HyproPolytope<ValueType>&>(*this);
             }
             
-            template class Polytope<double>;
 #ifdef STORM_HAVE_CARL
             template class Polytope<storm::RationalNumber>;
 #endif

src/storage/geometry/Polytope.h

@@ -11,17 +11,21 @@ namespace storm {
     namespace storage {
         namespace geometry {
             
+            // Forward declaration
+            template <typename ValueType>
+            class HyproPolytope;
+            
             template <typename ValueType>
             class Polytope {
             public:
                 
                 typedef std::vector<ValueType> Point;
-                
-                Polytope() = delete; //Use create methods to assemble a polytope
+            
+                ~Polytope();
                 
                 /*!
                  * Creates a polytope from the given halfspaces.
-                 * If the given vector of halfspaces is empty, the resulting polytope is universal (i.e., equals |R^n).
+                 * If the given vector of halfspaces is empty, the resulting polytope is universal (i.e., equals R^n).
                  */
                 static std::shared_ptr<Polytope<ValueType>> create(std::vector<Halfspace<ValueType>> const& halfspaces);
                 
@@ -32,71 +36,85 @@ namespace storm {
                 static std::shared_ptr<Polytope<ValueType>> create(std::vector<Point> const& points);
                 
                 /*!
-                 * Creates a polytope P from the given halfspaces
-                 * and returns the downward closure of P, i.e., the set { x | ex. y \in P: x<=y}
-                 * If the vector of halfspaces is empty, the resulting polytope will be universal.
+                 * Returns the vertices of this polytope.
                  */
-                static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<Halfspace<ValueType>> const& halfspaces);
+                virtual std::vector<Point> getVertices() const;
                 
                 /*!
-                 * Creates a polytope P from the given points (i.e., the convex hull of the points)
-                 * and returns the downward closure of P, i.e., the set { x | ex. y \in P: x<=y}
-                 * If the vector of points is empty, the resulting polytope be empty.
+                 * Returns the halfspaces of this polytope.
                  */
-                static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<Point> const& points);
-
+                virtual std::vector<Halfspace<ValueType>> getHalfspaces() const;
+                
                 /*!
-                 * Returns the vertices of this polytope.
+                 * Returns whether this polytope is the empty set.
                  */
-                virtual std::vector<Point> getVertices();
+                virtual bool isEmpty() const;
                 
                 /*!
-                 * Returns the halfspaces of this polytope.
+                 * Returns whether this polytope is universal (i.e., equals R^n).
                  */
-                virtual std::vector<Halfspace<ValueType>> getHalfspaces();
+                virtual bool isUniversal() const;
                 
                 /*!
                  * Returns true iff the given point is inside of the polytope.
                  */
                 virtual bool contains(Point const& point) const;
                 
+                /*!
+                 * Returns true iff the given polytope is a subset of this polytope.
+                 */
+                virtual bool contains(std::shared_ptr<Polytope<ValueType>> const& other) const;
+                
                 /*!
                  * Intersects this polytope with rhs and returns the result.
                  */
-                virtual std::shared_ptr<Polytope<ValueType>> intersect(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
-                virtual std::shared_ptr<Polytope<ValueType>> intersect(Halfspace<ValueType> const& rhs) const;
+                virtual std::shared_ptr<Polytope<ValueType>> intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
+                virtual std::shared_ptr<Polytope<ValueType>> intersection(Halfspace<ValueType> const& halfspace) const;
                 
                 /*!
                  * Returns the convex union of this polytope and rhs.
                  */
                 virtual std::shared_ptr<Polytope<ValueType>> convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
-                virtual std::shared_ptr<Polytope<ValueType>> convexUnion(Point const& rhs) const;
+        
+                /*!
+                 * Returns the minkowskiSum of this polytope and rhs.
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
                 
                 /*!
-                 * Bloats the polytope
-                 * The resulting polytope is (possibly an overapproximation of) the minkowski sum of this polytope and the 
-                 * hyperrectangle given by point1 and point2.
+                 * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope.
+                 * Put differently, the resulting polytope corresponds to this polytope, where
+                 * 1. a vector y with y_i=max{x_i | x \in P} is computed and for each i, a halfspace with offset y_i and
+                 *    normal vector n (where n_i = 1 and the remaining entries are 0) is inserted.
+                 * 2. all halfspaces where the normal vector has at least one negative entry are removed
+                 *
+                 * @param upperBounds If given, this vector is considered for y (hence, max{x_i | x i \in P does not need to be computed)
                  */
-                virtual std::shared_ptr<Polytope<ValueType>> bloat(Point const& point1, Point const& point2) const;
-
+                virtual std::shared_ptr<Polytope<ValueType>> downwardClosure(boost::optional<Point> const& upperBounds = boost::none) const;
                 
                 /*
                  * Returns a string representation of this polytope.
+                 * If the given flag is true, the occurring numbers are converted to double before printing to increase readability
                  */
-                virtual std::string toString() const;
+                virtual std::string toString(bool numbersAsDouble = false) const;
                
+                
+                virtual bool isHyproPolytope() const;
+                
+                HyproPolytope<ValueType>& asHyproPolytope();
+                HyproPolytope<ValueType> const& asHyproPolytope() const;
+                
+            protected:
+                
+                Polytope();
+                
             private:
                 /*!
                  * Creates a polytope from the given halfspaces or vertices.
-                 * if the given flag is true, the downward closure will be created.
                  */
                 static std::shared_ptr<Polytope<ValueType>> create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
-                                                                   boost::optional<std::vector<Point>> const& points,
-                                                                   bool downwardClosure);
+                                                                   boost::optional<std::vector<Point>> const& points);
                 
-                Polytope(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
-                                 boost::optional<std::vector<Point>> const& points,
-                                 bool downwardClosure);
                 
             };