linear transformation for polytopes

Former-commit-id: 62428c8209

src/storage/geometry/HyproPolytope.cpp

@@ -144,6 +144,16 @@ namespace storm {
                 return std::make_shared<HyproPolytope<ValueType>>(internPolytope.minkowskiSum(dynamic_cast<HyproPolytope<ValueType> const&>(*rhs).internPolytope));
             }
             
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::linearTransformation(std::vector<Point> const& matrix, Point const& vector) const{
+                STORM_LOG_THROW(!matrix.empty(), storm::exceptions::InvalidArgumentException, "Invoked linear transformation with a matrix without rows.");
+                hypro::matrix_t<ValueType> hyproMatrix(matrix.size(), matrix.front().size());
+                for(uint_fast64_t row = 0; row < matrix.size(); ++row) {
+                    hyproMatrix.row(row) = storm::adapters::toHypro(matrix[row]);
+                }
+                return std::make_shared<HyproPolytope<ValueType>>(internPolytope.linearTransformation(std::move(hyproMatrix), storm::adapters::toHypro(vector)));
+            }
+            
             template <typename ValueType>
             std::shared_ptr<Polytope<ValueType>> HyproPolytope<ValueType>::downwardClosure(boost::optional<Point> const& upperBounds) const {
                 if(this->isUniversal() || this->isEmpty()) {

src/storage/geometry/HyproPolytope.h

@@ -97,6 +97,15 @@ namespace storm {
                  */
                 virtual std::shared_ptr<Polytope<ValueType>> minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const override;
                 
+                /*!
+                 * Returns the linear transformation of this polytope P w.r.t. the given matrix A and vector b.
+                 * The result is the set {A*x+b | x \in P}
+                 * 
+                 * @param matrix the transformation matrix, given as vector of rows
+                 * @param vector the transformation offset
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> linearTransformation(std::vector<Point> const& matrix, Point const& vector) const;
+                
                 /*!
                  * 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

src/storage/geometry/Polytope.cpp

@@ -122,6 +122,12 @@ namespace storm {
                 return nullptr;
             }
             
+            template <typename ValueType>
+            std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::linearTransformation(std::vector<Point> const& matrix, Point const& vector) const {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                return nullptr;
+            }
+            
             template <typename ValueType>
             std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::downwardClosure(boost::optional<Point> const& upperBounds) const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");

src/storage/geometry/Polytope.h

@@ -86,6 +86,15 @@ namespace storm {
                  * Returns the minkowskiSum of this polytope and rhs.
                  */
                 virtual std::shared_ptr<Polytope<ValueType>> minkowskiSum(std::shared_ptr<Polytope<ValueType>> const& rhs) const;
+        
+                /*!
+                 * Returns the linear transformation of this polytope P w.r.t. the given matrix A and vector b.
+                 * The result is the set {A*x+b | x \in P}
+                 *
+                 * @param matrix the transformation matrix, given as vector of rows
+                 * @param vector the transformation offset
+                 */
+                virtual std::shared_ptr<Polytope<ValueType>> linearTransformation(std::vector<Point> const& matrix, Point const& vector) const;
                 
                 /*!
                  * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope.