more polytopes, hyproadapter

Former-commit-id: 389c65ba75

src/adapters/HyproAdapter.h

@@ -0,0 +1,48 @@
+#ifndef STORM_ADAPTERS_HYPROADAPTER_H_
+#define STORM_ADAPTERS_HYPROADAPTER_H_
+
+// Include config to know whether HyPro is available or not.
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_HYPRO
+
+#include </Users/tim/hypro/src/lib/datastructures/Halfspace.h>
+//#include <lib/types.h>
+#include <lib/representations/Polytope/Polytope.h>
+
+#include "src/adapters/CarlAdapter.h"
+#include "src/storage/geometry/HalfSpace.h"
+
+namespace storm {
+    namespace adapters {
+        
+            
+        template <typename T>
+        std::vector<T> fromHypro(hypro::vector_t<T> const& v) {
+            return std::vector<T>(v.data(), v.data() + v.rows());
+        }
+            
+        template <typename T>
+        hypro::vector_t<T> toHypro(std::vector<T> const& v) {
+            hypro::vector_t<T> res(v.size());
+            for ( auto const& value : v){
+                res << value;
+            }
+            return res;
+        }
+        
+        template <typename T>
+        hypro::Halfspace<T> toHypro(storm::storage::geometry::Halfspace<T> const& h){
+            return hypro::Halfspace<T>(toHypro(h.normalVector()), h.offset());
+        }
+        
+        template <typename T>
+        hypro::Halfspace<T> fromHypro(hypro::Halfspace<T> const& h){
+            return storm::storage::geometry::Halfspace<T>(fromHypro(h.normal()), h.offset());
+        }
+        
+    }
+}
+#endif //STORM_HAVE_HYPRO
+        
+#endif /* STORM_ADAPTERS_HYPROADAPTER_H_ */

src/storage/geometry/Halfspace.h

@@ -13,37 +13,57 @@ namespace storm {
              */
              
             template <typename ValueType>
-            struct HalfSpace {
+            class Halfspace {
                 
-                HalfSpace(std::vector<ValueType> const& normalVector, ValueType const& offset) : normalVector(normalVector), offset(offset)  {
+            public:
+                
+                Halfspace(std::vector<ValueType> const& normalVector, ValueType const& offset) : mNormalVector(normalVector), mOffset(offset)  {
                     //Intentionally left empty
                 }
                 
-                HalfSpace(std::vector<ValueType>&& normalVector, ValueType&& offset) : normalVector(normalVector), offset(offset) {
+                Halfspace(std::vector<ValueType>&& normalVector, ValueType&& offset) : mNormalVector(normalVector), mOffset(offset) {
                     //Intentionally left empty
                 }
                 
                 bool contains(std::vector<ValueType> const& point) {
-                    return storm::utility::vector::multiplyVectors(point, normalVector) <= offset;
+                    return storm::utility::vector::multiplyVectors(point, normalVector()) <= offset();
                 }
 
-                std::vector<ValueType> normalVector;
-                ValueType offset;
-                
                 std::string toString() {
                     std::stringstream stream;
                     stream << "(";
-                    for(auto it = normalVector.begin(); it != normalVector.end(); ++it){
-                        if(it != normalVector.begin()){
+                    for(auto it = normalVector().begin(); it != normalVector().end(); ++it){
+                        if(it != normalVector().begin()){
                             stream << ", ";
                         }
                         stream << *it;
                     }
-                    stream << ") * x <= " << offset;
+                    stream << ") * x <= " << offset();
                     return stream.str();
                 }
                 
+                std::vector<ValueType> const& normalVector() const {
+                    return mNormalVector;
+                }
+                
+                std::vector<ValueType>& normalVector(){
+                    return mNormalVector;
+                }
+                
+                ValueType const& offset() const {
+                    return mOffset;
                 }
+                
+                ValueType& offset(){
+                    return mOffset;
+                }
+                
+            private:
+                
+                std::vector<ValueType> mNormalVector;
+                ValueType mOffset;
+                
+            };
         }
     }
 }

src/storage/geometry/Polytope.cpp

@@ -1,18 +1,94 @@
-#ifndef STORM_STORAGE_GEOMETRY_POLYTOPE_H_
-#define STORM_STORAGE_GEOMETRY_POLYTOPE_H_
+#include "src/storage/geometry/Polytope.h"
 
-#include <vector>
-#include <memory>
+#include "src/utility/macros.h"
+#include "src/adapters/HyproAdapter.h"
+#include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace storage {
         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);
+            }
             
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(std::vector<Point> const& points){
+                return create(boost::none, points, false);
+            }
             
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::createDownwardClosure(std::vector<Halfspace<ValueType>> const& halfspaces){
+                return create(halfspaces, boost::none, false);
+            }
             
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::createDownwardClosure(std::vector<Point> const& points){
+                return create(boost::none, points, true);
             }
+            
+            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;
+            }
+            
+            template <typename ValueType>
+            std::vector<typename Polytope<ValueType>::Point> Polytope<ValueType>::getVertices(){
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            
+            template <typename ValueType>
+            std::vector<Halfspace<ValueType>> Polytope<ValueType>::getHalfspaces(){
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            
+            template <typename ValueType>
+            bool Polytope<ValueType>::contains(Point const& point) const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::intersect(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::intersect(Halfspace<ValueType> const& rhs) const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            
+            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.");
+            }
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::convexUnion(Point const& rhs) const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::bloat(Point const& point1, Point const& point2) const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
             }
-}
             
-#endif /* STORM_STORAGE_GEOMETRY_POLYTOPE_H_ */
+            
+            template <typename ValueType>
+            std::string Polytope<ValueType>::toString() const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+            }
+            
+            template class Polytope<double>;
+#ifdef STORM_HAVE_CARL
+            template class Polytope<storm::RationalNumber>;
+#endif
+        }
+    }
+}

src/storage/geometry/Polytope.h

@@ -3,42 +3,52 @@
 
 #include <vector>
 #include <memory>
+#include <boost/optional.hpp>
 
-#include "src/storage/geometry/HalfSpace.h"
+#include "src/storage/geometry/Halfspace.h"
 
 namespace storm {
     namespace storage {
         namespace geometry {
+            
             template <typename ValueType>
             class Polytope {
             public:
                 
-                typedef std::vector<ValueType> point_t;
-                typedef HalfSpace<ValueType> halfspace_t;
+                typedef std::vector<ValueType> Point;
+                
+                Polytope() = delete; //Use create methods to assemble a 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).
+                 */
+                static std::shared_ptr<Polytope<ValueType>> create(std::vector<Halfspace<ValueType>> const& halfspaces);
                 
                 /*!
                  * Creates a polytope from the given points (i.e., the convex hull of the points).
                  * If the vector of points is empty, the resulting polytope be empty.
                  */
-                static std::shared_ptr<Polytope<ValueType>> create(std::vector<point_t> const& points);
+                static std::shared_ptr<Polytope<ValueType>> create(std::vector<Point> const& points);
                 
                 /*!
-                 * 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).
+                 * 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.
                  */
-                static std::shared_ptr<Polytope<ValueType>> create(std::vector<Halfspace<ValueType>> const& halfspaces);
+                static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<Halfspace<ValueType>> const& halfspaces);
                 
                 /*!
                  * 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.
                  */
-                static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<point_t> const& points);
+                static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<Point> const& points);
 
                 /*!
                  * Returns the vertices of this polytope.
                  */
-                virtual std::vector<point_t> getVertices();
+                virtual std::vector<Point> getVertices();
                 
                 /*!
                  * Returns the halfspaces of this polytope.
@@ -48,46 +58,45 @@ namespace storm {
                 /*!
                  * Returns true iff the given point is inside of the polytope.
                  */
-                virtual bool contains(point_t const& point) const;
+                virtual bool contains(Point const& point) const;
                 
                 /*!
                  * Intersects this polytope with rhs and returns the result.
                  */
-                virtual unstd::shared_ptr<Polytope<ValueType>> intersect(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
-                virtual unstd::shared_ptr<Polytope<ValueType>> intersect(Halfspace<ValueType> const& rhs) const;
+                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;
                 
                 /*!
                  * 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_t const& rhs) const;
+                virtual std::shared_ptr<Polytope<ValueType>> convexUnion(Point const& rhs) const;
                 
                 /*!
                  * Bloats the polytope
-                 * The resulting polytope is an overapproximation of the minkowski sum of this polytope and the hyperrectangle given by point1
-                 * and point2 but does not introduce new halfspaces.
-                 * In more detail, let P={ x | A*x<=b} be the current polytope and R be the smallest hyperrectangle containing the two points.
-                 * The result is the smallest polytope P' with 
-                 * 1. P'={ x | A*x<=b'}
-                 * 2. For each p \in P and r \in R it holds that (p+r) \in P'
+                 * The resulting polytope is (possibly an overapproximation of) the minkowski sum of this polytope and the 
+                 * hyperrectangle given by point1 and point2.
                  */
-                virtual std::shared_ptr<Polytope<ValueType>> bloat(point_t const& point1, point_t const& point2) const;
-
+                virtual std::shared_ptr<Polytope<ValueType>> bloat(Point const& point1, Point const& point2) const;
 
-            private:
-                virtual Polytope();
                 
-                /*!
-                 * Creates a polytope from the given points (i.e., the convex hull of the points).
-                 * If the vector of points is empty, the resulting polytope be empty.
+                /*
+                 * Returns a string representation of this polytope.
                  */
-                virtual Polytope(std::vector<point_t> const& points);
+                virtual std::string toString() const;
                
+            private:
                 /*!
-                 * 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).
+                 * Creates a polytope from the given halfspaces or vertices.
+                 * if the given flag is true, the downward closure will be created.
                  */
-                virtual Polytope(std::vector<Halfspace<ValueType>> const& halfspaces);
+                static std::shared_ptr<Polytope<ValueType>> create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
+                                                                   boost::optional<std::vector<Point>> const& points,
+                                                                   bool downwardClosure);
+                
+                Polytope(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
+                                 boost::optional<std::vector<Point>> const& points,
+                                 bool downwardClosure);
                 
             };