Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Polytope.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/optional.hpp>
4#include <memory>
5#include <vector>
6
10
11namespace storm {
12namespace storage {
13namespace geometry {
14
15template<typename ValueType>
16class Polytope {
17 public:
18 typedef std::vector<ValueType> Point;
19
20 virtual ~Polytope();
21
26 static std::shared_ptr<Polytope<ValueType>> create(std::vector<Halfspace<ValueType>> const& halfspaces);
27
32 static std::shared_ptr<Polytope<ValueType>> create(std::vector<Point> const& points);
33
37 static std::shared_ptr<Polytope<ValueType>> createUniversalPolytope();
38
42 static std::shared_ptr<Polytope<ValueType>> createEmptyPolytope();
43
48 static std::shared_ptr<Polytope<ValueType>> createDownwardClosure(std::vector<Point> const& points);
49
55 static std::shared_ptr<Polytope<ValueType>> createSelectiveDownwardClosure(std::vector<Point> const& points,
56 storm::storage::BitVector const& selectedDimensions);
57
61 virtual std::vector<Point> getVertices() const = 0;
62
67 virtual std::vector<Point> getVerticesInClockwiseOrder() const;
68
72 virtual std::vector<Halfspace<ValueType>> getHalfspaces() const = 0;
73
77 virtual bool isEmpty() const = 0;
78
82 virtual bool isUniversal() const = 0;
83
87 virtual bool contains(Point const& point) const = 0;
88
92 virtual bool contains(std::shared_ptr<Polytope<ValueType>> const& other) const = 0;
93
97 virtual std::shared_ptr<Polytope<ValueType>> intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const = 0;
98 virtual std::shared_ptr<Polytope<ValueType>> intersection(Halfspace<ValueType> const& halfspace) const = 0;
99
103 virtual std::shared_ptr<Polytope<ValueType>> convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const = 0;
104
108 virtual std::shared_ptr<Polytope<ValueType>> minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const = 0;
109
117 virtual std::shared_ptr<Polytope<ValueType>> affineTransformation(std::vector<Point> const& matrix, Point const& vector) const = 0;
118
124 std::shared_ptr<Polytope<ValueType>> shift(Point const& b) const;
125
129 virtual std::shared_ptr<Polytope<ValueType>> downwardClosure() const;
130
137 std::vector<std::shared_ptr<Polytope<ValueType>>> setMinus(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
138
146 virtual std::pair<Point, bool> optimize(Point const& direction) const = 0;
147
153 virtual std::vector<storm::expressions::Variable> declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const;
154
158 virtual std::vector<storm::expressions::Expression> getConstraints(storm::expressions::ExpressionManager const& manager,
159 std::vector<storm::expressions::Variable> const& variables) const;
160
164 template<typename TargetType>
165 std::shared_ptr<Polytope<TargetType>> convertNumberRepresentation() const;
166
170 virtual std::shared_ptr<Polytope<ValueType>> clean();
171
172 /*
173 * Returns a string representation of this polytope.
174 * @param numbersAsDouble If true, the occurring numbers are converted to double before printing to increase readability.
175 */
176 virtual std::string toString(bool numbersAsDouble = false) const;
177
178 virtual bool isNativePolytope() const;
179
180 protected:
182
183 private:
187 static std::shared_ptr<Polytope<ValueType>> create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
188 boost::optional<std::vector<Point>> const& points);
189};
190
191} // namespace geometry
192} // namespace storage
193} // namespace storm
This class is responsible for managing a set of typed variables and all expressions using these varia...
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
virtual std::shared_ptr< Polytope< ValueType > > affineTransformation(std::vector< Point > const &matrix, Point const &vector) const =0
Returns the affine transformation of this polytope P w.r.t.
static std::shared_ptr< Polytope< ValueType > > createDownwardClosure(std::vector< Point > const &points)
Creates the downward closure of the given points (i.e., the set { x | ex.
Definition Polytope.cpp:40
virtual bool contains(std::shared_ptr< Polytope< ValueType > > const &other) const =0
Returns true iff the given polytope is a subset of this polytope.
virtual std::vector< Point > getVerticesInClockwiseOrder() const
Returns the vertices of this 2D-polytope in clockwise order.
Definition Polytope.cpp:155
virtual std::pair< Point, bool > optimize(Point const &direction) const =0
Finds an optimal point inside this polytope w.r.t.
virtual std::shared_ptr< Polytope< ValueType > > minkowskiSum(std::shared_ptr< Polytope< ValueType > > const &rhs) const =0
Returns the minkowskiSum of this polytope and rhs.
std::vector< std::shared_ptr< Polytope< ValueType > > > setMinus(std::shared_ptr< Polytope< ValueType > > const &rhs) const
Computes the set {x \in this | x \notin rhs}.
Definition Polytope.cpp:173
static std::shared_ptr< Polytope< ValueType > > create(std::vector< Halfspace< ValueType > > const &halfspaces)
Creates a polytope from the given halfspaces.
virtual std::vector< storm::expressions::Expression > getConstraints(storm::expressions::ExpressionManager const &manager, std::vector< storm::expressions::Variable > const &variables) const
Returns the constrains defined by this polytope as an expression over the given variables.
Definition Polytope.cpp:205
virtual std::shared_ptr< Polytope< ValueType > > intersection(Halfspace< ValueType > const &halfspace) const =0
virtual std::shared_ptr< Polytope< ValueType > > downwardClosure() const
Returns the downward closure of this, i.e., the set { x | ex.
Definition Polytope.cpp:192
static std::shared_ptr< Polytope< ValueType > > create(std::vector< Point > const &points)
Creates a polytope from the given points (i.e., the convex hull of the points).
Definition Polytope.cpp:19
virtual bool isNativePolytope() const
Definition Polytope.cpp:241
virtual std::shared_ptr< Polytope< ValueType > > clean()
Performs cleaning operations, e.g., deleting redundant halfspaces.
Definition Polytope.cpp:246
static std::shared_ptr< Polytope< ValueType > > createUniversalPolytope()
Creates the universal polytope (i.e., the set R^n).
Definition Polytope.cpp:24
virtual std::string toString(bool numbersAsDouble=false) const
Definition Polytope.cpp:230
std::shared_ptr< Polytope< TargetType > > convertNumberRepresentation() const
converts the intern number representation of the polytope to the given target type
Definition Polytope.cpp:214
virtual bool isUniversal() const =0
Returns whether this polytope is universal (i.e., equals R^n).
virtual bool isEmpty() const =0
Returns whether this polytope is the empty set.
virtual std::shared_ptr< Polytope< ValueType > > convexUnion(std::shared_ptr< Polytope< ValueType > > const &rhs) const =0
Returns the convex union of this polytope and rhs.
virtual std::vector< Halfspace< ValueType > > getHalfspaces() const =0
Returns the halfspaces of this polytope.
virtual bool contains(Point const &point) const =0
Returns true iff the given point is inside of the polytope.
virtual std::vector< Point > getVertices() const =0
Returns the vertices of this polytope.
static std::shared_ptr< Polytope< ValueType > > createEmptyPolytope()
Creates the empty polytope (i.e., emptyset).
Definition Polytope.cpp:29
virtual std::shared_ptr< Polytope< ValueType > > intersection(std::shared_ptr< Polytope< ValueType > > const &rhs) const =0
Intersects this polytope with rhs and returns the result.
static std::shared_ptr< Polytope< ValueType > > createSelectiveDownwardClosure(std::vector< Point > const &points, storm::storage::BitVector const &selectedDimensions)
Creates the downward closure of the given points but only with respect to the selected dimensions,...
Definition Polytope.cpp:51
std::shared_ptr< Polytope< ValueType > > shift(Point const &b) const
Returns the Polytope described by the set {x+b | x \in this}.
Definition Polytope.cpp:163
virtual std::vector< storm::expressions::Variable > declareVariables(storm::expressions::ExpressionManager &manager, std::string const &namePrefix) const
Declares one variable for each dimension and returns the obtained variables.
Definition Polytope.cpp:197