diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 48eca36b2..993f26248 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -47,6 +47,7 @@ file(GLOB STORM_STORAGE_DFT_ELEMENTS_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_GEOMETRY_FILES ${PROJECT_SOURCE_DIR}/src/storage/geometry/*.h ${PROJECT_SOURCE_DIR}/src/storage/geometry/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) @@ -106,6 +107,7 @@ source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) source_group(storage\\dft FILES ${STORM_STORAGE_DFT_FILES}) source_group(storage\\dft\\elements FILES ${STORM_STORAGE_DFT_ELEMENTS_FILES}) +source_group(storage\\geometry FILES ${STORM_STORAGE_GEOMETRY_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) # Add custom additional include or link directories diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp index 935e4ecba..7b438cba2 100644 --- a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp @@ -195,7 +195,6 @@ namespace storm { if(info.negatedRewardsConsidered){ storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); } - std::cout << objectiveRewards.size() << "==" << info.model.getTransitionMatrix().getRowCount() << "!=" << info.model.getNumberOfStates() << std::endl; info.model.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); } diff --git a/src/storage/geometry/Halfspace.h b/src/storage/geometry/Halfspace.h new file mode 100644 index 000000000..40aa6140e --- /dev/null +++ b/src/storage/geometry/Halfspace.h @@ -0,0 +1,51 @@ +#ifndef STORM_STORAGE_GEOMETRY_HALFSPACE_H_ +#define STORM_STORAGE_GEOMETRY_HALFSPACE_H_ + +#include +#include "src/utility/vector.h" + +namespace storm { + namespace storage { + namespace geometry { + + /* + * This class represents a closed Halfspace, i.e., the set { x | a*x<=c } for a normalVector a and an offset c + */ + + template + struct HalfSpace { + + HalfSpace(std::vector const& normalVector, ValueType const& offset) : normalVector(normalVector), offset(offset) { + //Intentionally left empty + } + + HalfSpace(std::vector&& normalVector, ValueType&& offset) : normalVector(normalVector), offset(offset) { + //Intentionally left empty + } + + bool contains(std::vector const& point) { + 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()){ + stream << ", "; + } + stream << *it; + } + stream << ") * x <= " << offset; + return stream.str(); + } + + } + } + } +} + +#endif /* STORM_STORAGE_GEOMETRY_HALFSPACE_H_ */ diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp new file mode 100644 index 000000000..bf3d4d136 --- /dev/null +++ b/src/storage/geometry/Polytope.cpp @@ -0,0 +1,18 @@ +#ifndef STORM_STORAGE_GEOMETRY_POLYTOPE_H_ +#define STORM_STORAGE_GEOMETRY_POLYTOPE_H_ + +#include +#include + +namespace storm { + namespace storage { + namespace geometry { + + + + + } + } +} + +#endif /* STORM_STORAGE_GEOMETRY_POLYTOPE_H_ */ diff --git a/src/storage/geometry/Polytope.h b/src/storage/geometry/Polytope.h new file mode 100644 index 000000000..bc7c17f03 --- /dev/null +++ b/src/storage/geometry/Polytope.h @@ -0,0 +1,98 @@ +#ifndef STORM_STORAGE_GEOMETRY_POLYTOPE_H_ +#define STORM_STORAGE_GEOMETRY_POLYTOPE_H_ + +#include +#include + +#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; + + /*! + * 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); + + /*! + * 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 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); + + /*! + * Returns the vertices of this polytope. + */ + virtual std::vector getVertices(); + + /*! + * Returns the halfspaces of this polytope. + */ + virtual std::vector> getHalfspaces(); + + /*! + * Returns true iff the given point is inside of the polytope. + */ + virtual bool contains(point_t 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; + + /*! + * 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; + + /*! + * 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' + */ + virtual std::shared_ptr> bloat(point_t const& point1, point_t const& point2) 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. + */ + virtual Polytope(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). + */ + virtual Polytope(std::vector> const& halfspaces); + + }; + + } + } +} + +#endif /* STORM_STORAGE_GEOMETRY_POLYTOPE_H_ */ diff --git a/src/utility/vector.h b/src/utility/vector.h index d632a7b4a..0403f86f7 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -346,6 +346,35 @@ namespace storm { applyPointwise(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; }); } + /*! + * Converts the numbers in the given vector to the target representation + * + * @param target The target vector in which the resulting numbers are written. + * @param source The source vector whose numbers are converted + */ + template + void convertVector(std::vector const& source, std::vector& target) { + applyPointwise(source, target, [&] (SourceType const& argument) -> TargetType { return convertNumber(argument); }); + } + + /*! + * Multiplies the two given vectors (scalar product) and returns the result + * + * @param firstOperand The first operand. + * @param secondOperand The second operand + * @return firstOperand*secondOperand + */ + template + T multiplyVectors(std::vector const& firstOperand, std::vector const& secondOperand) { + T res = storm::utility::zero(); + auto it1 = firstOperand.begin(); + auto it2 = secondOperand.begin(); + for(; it1