diff --git a/src/adapters/HyproAdapter.h b/src/adapters/HyproAdapter.h new file mode 100644 index 000000000..d63553583 --- /dev/null +++ b/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 +//#include +#include + +#include "src/adapters/CarlAdapter.h" +#include "src/storage/geometry/HalfSpace.h" + +namespace storm { + namespace adapters { + + + template + std::vector fromHypro(hypro::vector_t const& v) { + return std::vector(v.data(), v.data() + v.rows()); + } + + template + hypro::vector_t toHypro(std::vector const& v) { + hypro::vector_t res(v.size()); + for ( auto const& value : v){ + res << value; + } + return res; + } + + template + hypro::Halfspace toHypro(storm::storage::geometry::Halfspace const& h){ + return hypro::Halfspace(toHypro(h.normalVector()), h.offset()); + } + + template + hypro::Halfspace fromHypro(hypro::Halfspace const& h){ + return storm::storage::geometry::Halfspace(fromHypro(h.normal()), h.offset()); + } + + } +} +#endif //STORM_HAVE_HYPRO + +#endif /* STORM_ADAPTERS_HYPROADAPTER_H_ */ diff --git a/src/storage/geometry/Halfspace.h b/src/storage/geometry/Halfspace.h index 40aa6140e..4317df726 100644 --- a/src/storage/geometry/Halfspace.h +++ b/src/storage/geometry/Halfspace.h @@ -13,37 +13,57 @@ namespace storm { */ template - struct HalfSpace { + class Halfspace { - HalfSpace(std::vector const& normalVector, ValueType const& offset) : normalVector(normalVector), offset(offset) { + public: + + Halfspace(std::vector const& normalVector, ValueType const& offset) : mNormalVector(normalVector), mOffset(offset) { //Intentionally left empty } - HalfSpace(std::vector&& normalVector, ValueType&& offset) : normalVector(normalVector), offset(offset) { + Halfspace(std::vector&& normalVector, ValueType&& offset) : mNormalVector(normalVector), mOffset(offset) { //Intentionally left empty } bool contains(std::vector const& point) { - return storm::utility::vector::multiplyVectors(point, normalVector) <= offset; + return storm::utility::vector::multiplyVectors(point, normalVector()) <= offset(); } - std::vector 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 const& normalVector() const { + return mNormalVector; + } + + std::vector& normalVector(){ + return mNormalVector; + } + + ValueType const& offset() const { + return mOffset; + } + + ValueType& offset(){ + return mOffset; + } + + private: + + std::vector mNormalVector; + ValueType mOffset; + + }; } } } diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp index bf3d4d136..aaac1507d 100644 --- a/src/storage/geometry/Polytope.cpp +++ b/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 -#include +#include "src/utility/macros.h" +#include "src/adapters/HyproAdapter.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace storage { namespace geometry { + template + std::shared_ptr> Polytope::create(std::vector> const& halfspaces){ + return create(halfspaces, boost::none, false); + } + + template + std::shared_ptr> Polytope::create(std::vector const& points){ + return create(boost::none, points, false); + } + + template + std::shared_ptr> Polytope::createDownwardClosure(std::vector> const& halfspaces){ + return create(halfspaces, boost::none, false); + } + + template + std::shared_ptr> Polytope::createDownwardClosure(std::vector const& points){ + return create(boost::none, points, true); + } + + template + std::shared_ptr> Polytope::create(boost::optional>> const& halfspaces, + boost::optional> const& points, + bool downwardClosure) { - +#ifdef STORM_HAVE_HYPRO + std::cout << "HyPro available!!" << std::endl; + // return std::make_shared(HyproPolytope(halfspaces, points, downwardClosure)); +#endif + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified."); + return nullptr; + } + + template + std::vector::Point> Polytope::getVertices(){ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + + template + std::vector> Polytope::getHalfspaces(){ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + + template + bool Polytope::contains(Point const& point) const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + template + std::shared_ptr> Polytope::intersect(std::shared_ptr> const& rhs) const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + template + std::shared_ptr> Polytope::intersect(Halfspace const& rhs) const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + + template + std::shared_ptr> Polytope::convexUnion(std::shared_ptr> const& rhs) const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + template + std::shared_ptr> Polytope::convexUnion(Point const& rhs) const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + + template + std::shared_ptr> Polytope::bloat(Point const& point1, Point const& point2) const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + + + template + std::string Polytope::toString() const{ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + } + + template class Polytope; +#ifdef STORM_HAVE_CARL + template class Polytope; +#endif } } } - -#endif /* STORM_STORAGE_GEOMETRY_POLYTOPE_H_ */ diff --git a/src/storage/geometry/Polytope.h b/src/storage/geometry/Polytope.h index bc7c17f03..6e082dd0f 100644 --- a/src/storage/geometry/Polytope.h +++ b/src/storage/geometry/Polytope.h @@ -3,42 +3,52 @@ #include #include +#include -#include "src/storage/geometry/HalfSpace.h" +#include "src/storage/geometry/Halfspace.h" namespace storm { namespace storage { namespace geometry { + template class Polytope { public: - typedef std::vector point_t; - typedef HalfSpace halfspace_t; + typedef std::vector 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> create(std::vector> 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> create(std::vector const& points); + static std::shared_ptr> create(std::vector 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> create(std::vector> const& halfspaces); + static std::shared_ptr> createDownwardClosure(std::vector> 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> createDownwardClosure(std::vector const& points); + static std::shared_ptr> createDownwardClosure(std::vector const& points); /*! * Returns the vertices of this polytope. */ - virtual std::vector getVertices(); + virtual std::vector 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> intersect(std::shared_ptr> const& rhs) const; - virtual unstd::shared_ptr> intersect(Halfspace const& rhs) const; + virtual std::shared_ptr> intersect(std::shared_ptr> const& rhs) const; + virtual std::shared_ptr> intersect(Halfspace const& rhs) const; /*! * Returns the convex union of this polytope and rhs. */ virtual std::shared_ptr> convexUnion(std::shared_ptr> const& rhs) const; - virtual std::shared_ptr> convexUnion(point_t const& rhs) const; + virtual std::shared_ptr> 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> bloat(point_t const& point1, point_t const& point2) const; + virtual std::shared_ptr> bloat(Point const& point1, Point const& point2) const; + /* + * Returns a string representation of this polytope. + */ + virtual std::string toString() 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. + * 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 const& points); + static std::shared_ptr> create(boost::optional>> const& halfspaces, + boost::optional> const& points, + bool downwardClosure); - /*! - * 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). - */ - virtual Polytope(std::vector> const& halfspaces); + Polytope(boost::optional>> const& halfspaces, + boost::optional> const& points, + bool downwardClosure); };