From 76cabb828710f73b1a33251f477d63890cbd7e92 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Apr 2019 12:18:42 +0200 Subject: [PATCH 1/4] geometry: Fixed a merge issue. --- src/storm/storage/geometry/NativePolytope.h | 2 ++ src/storm/storage/geometry/Polytope.h | 30 ++++++++++++++++++++- 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/geometry/NativePolytope.h b/src/storm/storage/geometry/NativePolytope.h index abf147bda..324d5b1fb 100644 --- a/src/storm/storage/geometry/NativePolytope.h +++ b/src/storm/storage/geometry/NativePolytope.h @@ -1,8 +1,10 @@ #ifndef STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPE_H_ #define STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPE_H_ +#include #include "storm/storage/geometry/Polytope.h" #include "storm/adapters/EigenAdapter.h" +#include "storm/storage/expressions/Expression.h" namespace storm { namespace storage { diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h index 590057215..daef5aa7e 100644 --- a/src/storm/storage/geometry/Polytope.h +++ b/src/storm/storage/geometry/Polytope.h @@ -6,6 +6,8 @@ #include #include "storm/storage/geometry/Halfspace.h" +#include "storm/storage/BitVector.h" +#include "storm/storage/expressions/Expressions.h" namespace storm { namespace storage { @@ -43,10 +45,17 @@ namespace storm { /*! * Creates the downward closure of the given points (i.e., the set { x | ex. y \in conv(points) : x<=y } - * If the vector of points is empty, the resulting polytope be empty. + * If the vector of points is empty, the resulting polytope is empty. */ static std::shared_ptr> createDownwardClosure(std::vector const& points); + /*! + * Creates the downward closure of the given points but only with respect to the selected dimensions, + * (i.e., the set { x | ex. y \in conv(points) : (x_i<=y_i if i in selectedDim) and (x_i==y_i if i not in selectedDim } + * If the vector of points is empty, the resulting polytope is empty. + */ + static std::shared_ptr> createSelectiveDownwardClosure(std::vector const& points, storm::storage::BitVector const& selectedDimensions); + /*! * Returns the vertices of this polytope. */ @@ -108,6 +117,13 @@ namespace storm { */ virtual std::shared_ptr> affineTransformation(std::vector const& matrix, Point const& vector) const = 0; + /*! + * Returns the Polytope described by the set {x+b | x \in this} + * + * @param b the transformation offset + */ + std::shared_ptr> shift(Point const& b) const; + /*! * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope. */ @@ -130,6 +146,18 @@ namespace storm { */ virtual std::pair optimize(Point const& direction) const = 0; + /*! + * Declares one variable for each dimension and returns the obtained variables. + * @param manager The expression manager that keeps track of the variables + * @param namePrefix The prefix that is prepanded to the variable index + */ + virtual std::vector declareVariables(storm::expressions::ExpressionManager& manager, std::string const& namePrefix) const; + + /*! + * Returns the constrains defined by this polytope as an expression over the given variables + */ + virtual std::vector getConstraints(storm::expressions::ExpressionManager const& manager, std::vector const& variables) const; + /*! * converts the intern number representation of the polytope to the given target type */ From c72b97dfca57271fea8991430c81e77f2bd5a016 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 26 Apr 2019 15:58:54 +0200 Subject: [PATCH 2/4] Cleared unused variable warning. --- src/storm/storage/geometry/Polytope.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp index 1839e636f..3db106719 100644 --- a/src/storm/storage/geometry/Polytope.cpp +++ b/src/storm/storage/geometry/Polytope.cpp @@ -66,7 +66,6 @@ namespace storm { return create(points); } assert(points.front().size() == selectedDimensions.size()); - uint64_t dimensions = selectedDimensions.size(); std::vector> halfspaces; // We build the convex hull of the given points. From 4322d00034f9579eef946aaed7982adad24cbc3b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 07:24:09 +0200 Subject: [PATCH 3/4] FilteredRewardModel: added create method that works without a checkout. --- src/storm/utility/FilteredRewardModel.h | 26 ++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/src/storm/utility/FilteredRewardModel.h b/src/storm/utility/FilteredRewardModel.h index 32dc13521..5280cfd98 100644 --- a/src/storm/utility/FilteredRewardModel.h +++ b/src/storm/utility/FilteredRewardModel.h @@ -8,9 +8,8 @@ namespace storm { namespace utility { - /* - * This class wraps around a + * This class wraps around a Reward model where certain reward types are disabled. */ template class FilteredRewardModel { @@ -45,20 +44,25 @@ namespace storm { RewardModelType const* rewardModel; }; - template - FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { - auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); - if (checkTask.getFormula().hasRewardAccumulation()) { - auto const& acc = checkTask.getFormula().getRewardAccumulation(); - STORM_LOG_THROW(model.isDiscreteTimeModel() || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); + template + FilteredRewardModel createFilteredRewardModel(RewardModelType const& baseRewardModel, bool isDiscreteTimeModel, FormulaType const& formula) { + if (formula.hasRewardAccumulation()) { + auto const& acc = formula.getRewardAccumulation(); + STORM_LOG_THROW(isDiscreteTimeModel || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); // Check which of the available reward types are allowed. - bool hasStateRewards = model.isDiscreteTimeModel() ? acc.isExitSet() : acc.isTimeSet(); + bool hasStateRewards = isDiscreteTimeModel ? acc.isExitSet() : acc.isTimeSet(); bool hasStateActionRewards = acc.isStepsSet(); bool hasTransitionRewards = acc.isStepsSet(); - return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); + return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); } else { - return FilteredRewardModel(baseRewardModel, true, true, true); + return FilteredRewardModel(baseRewardModel, true, true, true); } } + + template + FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { + auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); + return createFilteredRewardModel(baseRewardModel, model.isDiscreteTimeModel(), checkTask.getFormula()); + } } } \ No newline at end of file From 160c6a67f4be4fb688f218ba8578cd6f28441003 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 07:24:30 +0200 Subject: [PATCH 4/4] Added missing method in case z3 lp solver is not available. --- src/storm/solver/Z3LpSolver.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index c152a9d20..16c04bd57 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -393,6 +393,11 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } + template + void Z3LpSolver::writeModelToFile(std::string const& filename) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } + template void Z3LpSolver::push() { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support.";