From d496e71169c8e417340fd252555ed9d15a3f9d0a Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 13 Jun 2016 15:20:07 +0200 Subject: [PATCH] linear transformation for polytopes Former-commit-id: 62428c82099ffbb0a7e9f98a851a01ff7142857b --- src/storage/geometry/HyproPolytope.cpp | 10 ++++++++++ src/storage/geometry/HyproPolytope.h | 9 +++++++++ src/storage/geometry/Polytope.cpp | 6 ++++++ src/storage/geometry/Polytope.h | 9 +++++++++ 4 files changed, 34 insertions(+) diff --git a/src/storage/geometry/HyproPolytope.cpp b/src/storage/geometry/HyproPolytope.cpp index 4efb965c9..79c696a64 100644 --- a/src/storage/geometry/HyproPolytope.cpp +++ b/src/storage/geometry/HyproPolytope.cpp @@ -144,6 +144,16 @@ namespace storm { return std::make_shared>(internPolytope.minkowskiSum(dynamic_cast const&>(*rhs).internPolytope)); } + template + std::shared_ptr> HyproPolytope::linearTransformation(std::vector 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 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>(internPolytope.linearTransformation(std::move(hyproMatrix), storm::adapters::toHypro(vector))); + } + template std::shared_ptr> HyproPolytope::downwardClosure(boost::optional const& upperBounds) const { if(this->isUniversal() || this->isEmpty()) { diff --git a/src/storage/geometry/HyproPolytope.h b/src/storage/geometry/HyproPolytope.h index 2f523c769..5cfc73c9d 100644 --- a/src/storage/geometry/HyproPolytope.h +++ b/src/storage/geometry/HyproPolytope.h @@ -97,6 +97,15 @@ namespace storm { */ virtual std::shared_ptr> minkowskiSum(std::shared_ptr> 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> linearTransformation(std::vector 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 diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp index f2fefa2bd..f5fc8ee6d 100644 --- a/src/storage/geometry/Polytope.cpp +++ b/src/storage/geometry/Polytope.cpp @@ -122,6 +122,12 @@ namespace storm { return nullptr; } + template + std::shared_ptr> Polytope::linearTransformation(std::vector const& matrix, Point const& vector) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); + return nullptr; + } + template std::shared_ptr> Polytope::downwardClosure(boost::optional const& upperBounds) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); diff --git a/src/storage/geometry/Polytope.h b/src/storage/geometry/Polytope.h index 8226a70e2..de08566e6 100644 --- a/src/storage/geometry/Polytope.h +++ b/src/storage/geometry/Polytope.h @@ -86,6 +86,15 @@ namespace storm { * Returns the minkowskiSum of this polytope and rhs. */ virtual std::shared_ptr> minkowskiSum(std::shared_ptr> 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> linearTransformation(std::vector 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.