From a638104adbbca31177bfb933bf8c9bf4a76c6c55 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 21 Jun 2018 17:30:34 +0200 Subject: [PATCH] using new post processing class for the 'old' implementation. --- .../pcaa/SparsePcaaParetoQuery.cpp | 8 ++- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 68 ++----------------- .../multiobjective/pcaa/SparsePcaaQuery.h | 7 -- 3 files changed, 10 insertions(+), 73 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index efe7a42f9..423394453 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -8,6 +8,8 @@ #include "storm/utility/constants.h" #include "storm/utility/vector.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" +#include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h" + namespace storm { namespace modelchecker { @@ -37,12 +39,12 @@ namespace storm { std::vector vertices = this->underApproximation->getVertices(); paretoOptimalPoints.reserve(vertices.size()); for(auto const& vertex : vertices) { - paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector(this->transformPointToOriginalModel(vertex))); + paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector(transformObjectiveValuesToOriginal(this->objectives, vertex))); } return std::unique_ptr(new ExplicitParetoCurveCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), - this->transformPolytopeToOriginalModel(this->underApproximation)->template convertNumberRepresentation(), - this->transformPolytopeToOriginalModel(this->overApproximation)->template convertNumberRepresentation())); + transformObjectivePolytopeToOriginal(this->objectives, this->underApproximation)->template convertNumberRepresentation(), + transformObjectivePolytopeToOriginal(this->objectives, this->overApproximation)->template convertNumberRepresentation())); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 5f127579f..1adbacd9e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -1,10 +1,11 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h" -#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/utility/constants.h" @@ -130,79 +131,20 @@ namespace storm { this->refinementSteps.size() >= env.modelchecker().multi().getMaxSteps(); } - - template - typename SparsePcaaQuery::Point SparsePcaaQuery::transformPointToOriginalModel(Point const& point) const { - Point result; - result.reserve(point.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - if (storm::solver::maximize(obj.formula->getOptimalityType())) { - if (obj.considersComplementaryEvent) { - result.push_back(storm::utility::one() - point[objIndex]); - } else { - result.push_back(point[objIndex]); - } - } else { - if (obj.considersComplementaryEvent) { - result.push_back(storm::utility::one() + point[objIndex]); - } else { - result.push_back(-point[objIndex]); - } - } - } - return result; - } - - template - std::shared_ptr> SparsePcaaQuery::transformPolytopeToOriginalModel(std::shared_ptr> const& polytope) const { - if(polytope->isEmpty()) { - return storm::storage::geometry::Polytope::createEmptyPolytope(); - } - if(polytope->isUniversal()) { - return storm::storage::geometry::Polytope::createUniversalPolytope(); - } - uint_fast64_t numObjectives = this->objectives.size(); - std::vector> transformationMatrix(numObjectives, std::vector(numObjectives, storm::utility::zero())); - std::vector transformationVector; - transformationVector.reserve(numObjectives); - for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { - auto const& obj = this->objectives[objIndex]; - if (storm::solver::maximize(obj.formula->getOptimalityType())) { - if (obj.considersComplementaryEvent) { - transformationMatrix[objIndex][objIndex] = -storm::utility::one(); - transformationVector.push_back(storm::utility::one()); - } else { - transformationMatrix[objIndex][objIndex] = storm::utility::one(); - transformationVector.push_back(storm::utility::zero()); - } - } else { - if (obj.considersComplementaryEvent) { - transformationMatrix[objIndex][objIndex] = storm::utility::one(); - transformationVector.push_back(storm::utility::one()); - } else { - transformationMatrix[objIndex][objIndex] = -storm::utility::one(); - transformationVector.push_back(storm::utility::zero()); - } - } - } - return polytope->affineTransformation(transformationMatrix, transformationVector); - } - template void SparsePcaaQuery::exportPlotOfCurrentApproximation(Environment const& env) const { STORM_LOG_ERROR_COND(objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case."); - auto transformedUnderApprox = transformPolytopeToOriginalModel(underApproximation); - auto transformedOverApprox = transformPolytopeToOriginalModel(overApproximation); + auto transformedUnderApprox = transformObjectivePolytopeToOriginal(this->objectives, underApproximation); + auto transformedOverApprox = transformObjectivePolytopeToOriginal(this->objectives, overApproximation); // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded. storm::storage::geometry::Hyperrectangle boundaries(std::vector(objectives.size(), storm::utility::zero()), std::vector(objectives.size(), storm::utility::zero())); std::vector> paretoPoints; paretoPoints.reserve(refinementSteps.size()); for(auto const& step : refinementSteps) { - paretoPoints.push_back(transformPointToOriginalModel(step.lowerBoundPoint)); + paretoPoints.push_back(transformObjectiveValuesToOriginal(this->objectives, step.lowerBoundPoint)); boundaries.enlarge(paretoPoints.back()); } auto underApproxVertices = transformedUnderApprox->getVertices(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index b466241ae..b1fb9d359 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -89,13 +89,6 @@ namespace storm { */ bool maxStepsPerformed(Environment const& env) const; - /* - * Transforms the given point (or polytope) to values w.r.t. the original model/formula (e.g. negates values for minimizing objectives). - */ - Point transformPointToOriginalModel(Point const& polytope) const; - std::shared_ptr> transformPolytopeToOriginalModel(std::shared_ptr> const& polytope) const; - - SparseModelType const& originalModel; storm::logic::MultiObjectiveFormula const& originalFormula;