sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

using new post processing class for the 'old' implementation.

main
TimQu 7 years ago
parent
80a66603fb
commit
a638104adb
3 changed files with 10 additions and 73 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
  2. 68
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
  3. 7
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h

8
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
View File

@ -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<Point> vertices = this->underApproximation->getVertices();
paretoOptimalPoints.reserve(vertices.size());
for(auto const& vertex : vertices) {
paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(this->transformPointToOriginalModel(vertex)));
paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(transformObjectiveValuesToOriginal(this->objectives, vertex)));
}
return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>(this->originalModel.getInitialStates().getNextSetIndex(0),
std::move(paretoOptimalPoints),
this->transformPolytopeToOriginalModel(this->underApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>(),
this->transformPolytopeToOriginalModel(this->overApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>()));
transformObjectivePolytopeToOriginal(this->objectives, this->underApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>(),
transformObjectivePolytopeToOriginal(this->objectives, this->overApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>()));
}

68
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
View File

@ -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 SparseModelType, typename GeometryValueType>
typename SparsePcaaQuery<SparseModelType, GeometryValueType>::Point SparsePcaaQuery<SparseModelType, GeometryValueType>::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<GeometryValueType>() - point[objIndex]);
} else {
result.push_back(point[objIndex]);
}
} else {
if (obj.considersComplementaryEvent) {
result.push_back(storm::utility::one<GeometryValueType>() + point[objIndex]);
} else {
result.push_back(-point[objIndex]);
}
}
}
return result;
}
template<typename SparseModelType, typename GeometryValueType>
std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> SparsePcaaQuery<SparseModelType, GeometryValueType>::transformPolytopeToOriginalModel(std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> const& polytope) const {
if(polytope->isEmpty()) {
return storm::storage::geometry::Polytope<GeometryValueType>::createEmptyPolytope();
}
if(polytope->isUniversal()) {
return storm::storage::geometry::Polytope<GeometryValueType>::createUniversalPolytope();
}
uint_fast64_t numObjectives = this->objectives.size();
std::vector<std::vector<GeometryValueType>> transformationMatrix(numObjectives, std::vector<GeometryValueType>(numObjectives, storm::utility::zero<GeometryValueType>()));
std::vector<GeometryValueType> 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<GeometryValueType>();
transformationVector.push_back(storm::utility::one<GeometryValueType>());
} else {
transformationMatrix[objIndex][objIndex] = storm::utility::one<GeometryValueType>();
transformationVector.push_back(storm::utility::zero<GeometryValueType>());
}
} else {
if (obj.considersComplementaryEvent) {
transformationMatrix[objIndex][objIndex] = storm::utility::one<GeometryValueType>();
transformationVector.push_back(storm::utility::one<GeometryValueType>());
} else {
transformationMatrix[objIndex][objIndex] = -storm::utility::one<GeometryValueType>();
transformationVector.push_back(storm::utility::zero<GeometryValueType>());
}
}
}
return polytope->affineTransformation(transformationMatrix, transformationVector);
}
template<typename SparseModelType, typename GeometryValueType>
void SparsePcaaQuery<SparseModelType, GeometryValueType>::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<GeometryValueType> boundaries(std::vector<GeometryValueType>(objectives.size(), storm::utility::zero<GeometryValueType>()), std::vector<GeometryValueType>(objectives.size(), storm::utility::zero<GeometryValueType>()));
std::vector<std::vector<GeometryValueType>> 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();

7
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
View File

@ -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<storm::storage::geometry::Polytope<GeometryValueType>> transformPolytopeToOriginalModel(std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> const& polytope) const;
SparseModelType const& originalModel;
storm::logic::MultiObjectiveFormula const& originalFormula;

Write Preview
Loading…
Cancel
Save