Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NativePolytope.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
7
8namespace storm {
9namespace storage {
10namespace geometry {
11
12template<typename ValueType>
13class NativePolytope : public Polytope<ValueType> {
14 public:
15 typedef Eigen::Matrix<ValueType, Eigen::Dynamic, Eigen::Dynamic> EigenMatrix;
16 typedef Eigen::Matrix<ValueType, Eigen::Dynamic, 1> EigenVector;
17
18 enum class EmptyStatus {
19 Unknown, // It is unknown whether the polytope is empty or not
20 Empty, // The polytope is empty
21 Nonempty // the polytope is not empty
22 };
23
25
30 static std::shared_ptr<Polytope<ValueType>> create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
31 boost::optional<std::vector<Point>> const& points);
32
37 NativePolytope(std::vector<Halfspace<ValueType>> const& halfspaces);
38
43 NativePolytope(std::vector<Point> const& points);
44
50
54 NativePolytope(EmptyStatus const& emptyStatus, EigenMatrix const& halfspaceMatrix, EigenVector const& halfspaceVector);
55 NativePolytope(EmptyStatus&& emptyStatus, EigenMatrix&& halfspaceMatrix, EigenVector&& halfspaceVector);
56
57 virtual ~NativePolytope();
58
62 virtual std::vector<Point> getVertices() const override;
63
67 virtual std::vector<Halfspace<ValueType>> getHalfspaces() const override;
68
72 virtual bool isEmpty() const override;
73
77 virtual bool isUniversal() const override;
78
82 virtual bool contains(Point const& point) const override;
83
87 virtual bool contains(std::shared_ptr<Polytope<ValueType>> const& other) const override;
88
92 virtual std::shared_ptr<Polytope<ValueType>> intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
93 virtual std::shared_ptr<Polytope<ValueType>> intersection(Halfspace<ValueType> const& halfspace) const override;
94
98 virtual std::shared_ptr<Polytope<ValueType>> convexUnion(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
99
103 virtual std::shared_ptr<Polytope<ValueType>> minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
104
112 virtual std::shared_ptr<Polytope<ValueType>> affineTransformation(std::vector<Point> const& matrix, Point const& vector) const override;
113
121 virtual std::pair<Point, bool> optimize(Point const& direction) const override;
122
128 virtual std::vector<storm::expressions::Variable> declareVariables(storm::expressions::ExpressionManager& manager,
129 std::string const& namePrefix) const override;
130
134 virtual std::vector<storm::expressions::Expression> getConstraints(storm::expressions::ExpressionManager const& manager,
135 std::vector<storm::expressions::Variable> const& variables) const override;
136
137 virtual bool isNativePolytope() const override;
138
139 virtual std::shared_ptr<Polytope<ValueType>> clean() override;
140
141 private:
142 // returns the vertices of this polytope as EigenVectors
143 std::vector<EigenVector> getEigenVertices() const;
144
145 // As optimize(..) but with EigenVectors
146 std::pair<EigenVector, bool> optimize(EigenVector const& direction) const;
147
148 // Stores whether the polytope is empty or not
149 mutable EmptyStatus emptyStatus;
150
151 // Intern representation of the polytope as { x | Ax<=b }
152 EigenMatrix A;
153 EigenVector b;
154};
155
156} // namespace geometry
157} // namespace storage
158} // namespace storm
This class is responsible for managing a set of typed variables and all expressions using these varia...
virtual bool contains(Point const &point) const override
Returns true iff the given point is inside of the polytope.
NativePolytope(std::vector< Halfspace< ValueType > > const &halfspaces)
Creates a NativePolytope from the given halfspaces The resulting polytope is defined as the intersect...
Eigen::Matrix< ValueType, Eigen::Dynamic, Eigen::Dynamic > EigenMatrix
virtual std::vector< storm::expressions::Variable > declareVariables(storm::expressions::ExpressionManager &manager, std::string const &namePrefix) const override
declares one variable for each dimension and returns the obtained variables.
virtual std::pair< Point, bool > optimize(Point const &direction) const override
Finds an optimal point inside this polytope w.r.t.
virtual std::shared_ptr< Polytope< ValueType > > clean() override
Performs cleaning operations, e.g., deleting redundant halfspaces.
virtual std::shared_ptr< Polytope< ValueType > > affineTransformation(std::vector< Point > const &matrix, Point const &vector) const override
Returns the affine transformation of this polytope P w.r.t.
virtual bool isNativePolytope() const override
Polytope< ValueType >::Point Point
virtual std::vector< Point > getVertices() const override
Returns the vertices of this polytope.
Eigen::Matrix< ValueType, Eigen::Dynamic, 1 > EigenVector
virtual bool isUniversal() const override
Returns whether this polytope is universal (i.e., equals R^n).
virtual std::shared_ptr< Polytope< ValueType > > intersection(std::shared_ptr< Polytope< ValueType > > const &rhs) const override
Intersects this polytope with rhs and returns the result.
virtual std::shared_ptr< Polytope< ValueType > > minkowskiSum(std::shared_ptr< Polytope< ValueType > > const &rhs) const override
Returns the minkowskiSum of this polytope and rhs.
static std::shared_ptr< Polytope< ValueType > > create(boost::optional< std::vector< Halfspace< ValueType > > > const &halfspaces, boost::optional< std::vector< Point > > const &points)
Creates a NativePolytope from the given halfspaces or points.
virtual bool isEmpty() const override
Returns whether this polytope is the empty set.
virtual std::vector< storm::expressions::Expression > getConstraints(storm::expressions::ExpressionManager const &manager, std::vector< storm::expressions::Variable > const &variables) const override
returns the constrains defined by this polytope as an expression over the given variables
virtual std::vector< Halfspace< ValueType > > getHalfspaces() const override
Returns the halfspaces of this polytope.
virtual std::shared_ptr< Polytope< ValueType > > convexUnion(std::shared_ptr< Polytope< ValueType > > const &rhs) const override
Returns the convex union of this polytope and rhs.
std::vector< ValueType > Point
Definition Polytope.h:18