From 5c38a4ef896684ddfa9a5b27629958076234f7f5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 28 May 2018 15:42:59 +0200 Subject: [PATCH] implemented environment for multiobjective settings --- src/storm/environment/Environment.cpp | 23 +++- src/storm/environment/Environment.h | 13 ++- src/storm/environment/SubEnvironment.cpp | 12 ++- .../modelchecker/ModelCheckerEnvironment.cpp | 31 ++++++ .../modelchecker/ModelCheckerEnvironment.h | 28 +++++ .../MultiObjectiveModelCheckerEnvironment.cpp | 100 ++++++++++++++++++ .../MultiObjectiveModelCheckerEnvironment.h | 48 +++++++++ .../multiObjectiveModelChecking.cpp | 6 +- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 7 +- .../pcaa/SparsePcaaParetoQuery.cpp | 24 ++--- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 18 ++-- .../pcaa/SparsePcaaQuantitativeQuery.h | 2 +- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 57 +++++----- .../multiobjective/pcaa/SparsePcaaQuery.h | 4 +- 14 files changed, 305 insertions(+), 68 deletions(-) create mode 100644 src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp create mode 100644 src/storm/environment/modelchecker/ModelCheckerEnvironment.h create mode 100644 src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp create mode 100644 src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h diff --git a/src/storm/environment/Environment.cpp b/src/storm/environment/Environment.cpp index 0836de3f7..6d5d3ca2b 100644 --- a/src/storm/environment/Environment.cpp +++ b/src/storm/environment/Environment.cpp @@ -1,6 +1,8 @@ #include "storm/environment/Environment.h" #include "storm/environment/SubEnvironment.h" #include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + namespace storm { @@ -12,11 +14,28 @@ namespace storm { // Intentionally left empty. } + Environment::Environment(Environment const& other) : internalEnv(other.internalEnv) { + // Intentionally left empty. + } + + Environment& Environment::operator=(Environment const& other) { + internalEnv = other.internalEnv; + return *this; + } + SolverEnvironment& Environment::solver() { - return solverEnvironment.get(); + return internalEnv.get().solverEnvironment.get(); } SolverEnvironment const& Environment::solver() const { - return solverEnvironment.get(); + return internalEnv.get().solverEnvironment.get(); + } + + ModelCheckerEnvironment& Environment::modelchecker() { + return internalEnv.get().modelcheckerEnvironment.get(); + } + + ModelCheckerEnvironment const& Environment::modelchecker() const { + return internalEnv.get().modelcheckerEnvironment.get(); } } \ No newline at end of file diff --git a/src/storm/environment/Environment.h b/src/storm/environment/Environment.h index 988ca34c6..30ac31803 100644 --- a/src/storm/environment/Environment.h +++ b/src/storm/environment/Environment.h @@ -6,19 +6,30 @@ namespace storm { // Forward declare sub-environments class SolverEnvironment; + class ModelCheckerEnvironment; + + // Avoid implementing ugly copy constructors for environment by using an internal environment. + struct InternalEnvironment { + SubEnvironment solverEnvironment; + SubEnvironment modelcheckerEnvironment; + }; class Environment { public: Environment(); virtual ~Environment(); + Environment(Environment const& other); + Environment& operator=(Environment const& other); SolverEnvironment& solver(); SolverEnvironment const& solver() const; + ModelCheckerEnvironment& modelchecker(); + ModelCheckerEnvironment const& modelchecker() const; private: - SubEnvironment solverEnvironment; + SubEnvironment internalEnv; }; } diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index f11b2b1bf..920a06049 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -1,4 +1,9 @@ -#include +#include + +#include "storm/environment/Environment.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" @@ -36,6 +41,11 @@ namespace storm { return *subEnv; } + template class SubEnvironment; + + template class SubEnvironment; + template class SubEnvironment; + template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp new file mode 100644 index 000000000..f0d917a28 --- /dev/null +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp @@ -0,0 +1,31 @@ +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" + +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidEnvironmentException.h" +#include "storm/exceptions/UnexpectedException.h" + + +namespace storm { + + ModelCheckerEnvironment::ModelCheckerEnvironment() { + // Intentionally left empty + } + + ModelCheckerEnvironment::~ModelCheckerEnvironment() { + // Intentionally left empty + } + + MultiObjectiveModelCheckerEnvironment& ModelCheckerEnvironment::multi() { + return multiObjectiveModelCheckerEnvironment.get(); + } + + MultiObjectiveModelCheckerEnvironment const& ModelCheckerEnvironment::multi() const { + return multiObjectiveModelCheckerEnvironment.get(); + } +} + + diff --git a/src/storm/environment/modelchecker/ModelCheckerEnvironment.h b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h new file mode 100644 index 000000000..2ec1eebd8 --- /dev/null +++ b/src/storm/environment/modelchecker/ModelCheckerEnvironment.h @@ -0,0 +1,28 @@ +#pragma once + +#include +#include + +#include "storm/environment/Environment.h" +#include "storm/environment/SubEnvironment.h" + +namespace storm { + + // Forward declare subenvironments + class MultiObjectiveModelCheckerEnvironment; + + class ModelCheckerEnvironment { + public: + + ModelCheckerEnvironment(); + ~ModelCheckerEnvironment(); + + MultiObjectiveModelCheckerEnvironment& multi(); + MultiObjectiveModelCheckerEnvironment const& multi() const; + + + private: + SubEnvironment multiObjectiveModelCheckerEnvironment; + }; +} + diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp new file mode 100644 index 000000000..92b51fde8 --- /dev/null +++ b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp @@ -0,0 +1,100 @@ +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { + + MultiObjectiveModelCheckerEnvironment::MultiObjectiveModelCheckerEnvironment() { + auto const& multiobjectiveSettings = storm::settings::getModule(); + method = multiobjectiveSettings.getMultiObjectiveMethod(); + if (multiobjectiveSettings.isExportPlotSet()) { + plotPathUnderApprox = multiobjectiveSettings.getExportPlotDirectory() + "underapproximation.csv"; + plotPathOverApprox = multiobjectiveSettings.getExportPlotDirectory() + "overapproximation.csv"; + plotPathParetoPoints = multiobjectiveSettings.getExportPlotDirectory() + "paretopoints.csv"; + } + + precision = storm::utility::convertNumber(multiobjectiveSettings.getPrecision()); + if (multiobjectiveSettings.isMaxStepsSet()) { + maxSteps = multiobjectiveSettings.getMaxSteps(); + } + } + + MultiObjectiveModelCheckerEnvironment::~MultiObjectiveModelCheckerEnvironment() { + // Intentionally left empty + } + + storm::modelchecker::multiobjective::MultiObjectiveMethod const& MultiObjectiveModelCheckerEnvironment::getMethod() const { + return this->method; + } + + void MultiObjectiveModelCheckerEnvironment::setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod value) { + this->method = value; + } + + bool MultiObjectiveModelCheckerEnvironment::isExportPlotSet() const { + return this->plotPathUnderApprox.is_initialized() || this->plotPathOverApprox.is_initialized() || this->plotPathParetoPoints.is_initialized(); + } + + boost::optional MultiObjectiveModelCheckerEnvironment::getPlotPathUnderApproximation() const { + return plotPathUnderApprox; + } + + void MultiObjectiveModelCheckerEnvironment::setPlotPathUnderApproximation(std::string const& path) { + plotPathUnderApprox = path; + } + + void MultiObjectiveModelCheckerEnvironment::unsetPlotPathUnderApproximation() { + plotPathUnderApprox = boost::none; + } + + boost::optional MultiObjectiveModelCheckerEnvironment::getPlotPathOverApproximation() const { + return plotPathOverApprox; + } + + void MultiObjectiveModelCheckerEnvironment::setPlotPathOverApproximation(std::string const& path) { + plotPathOverApprox = path; + } + + void MultiObjectiveModelCheckerEnvironment::unsetPlotPathOverApproximation() { + plotPathOverApprox = boost::none; + } + + boost::optional MultiObjectiveModelCheckerEnvironment::getPlotPathParetoPoints() const { + return plotPathParetoPoints; + } + + void MultiObjectiveModelCheckerEnvironment::setPlotPathParetoPoints(std::string const& path) { + plotPathParetoPoints = path; + } + + void MultiObjectiveModelCheckerEnvironment::unsetPlotPathParetoPoints() { + plotPathParetoPoints = boost::none; + } + + storm::RationalNumber const& MultiObjectiveModelCheckerEnvironment::getPrecision() const { + return precision; + } + + void MultiObjectiveModelCheckerEnvironment::setPrecision(storm::RationalNumber const& value) { + precision = value; + } + + bool MultiObjectiveModelCheckerEnvironment::isMaxStepsSet() const { + return maxSteps.is_initialized(); + } + + uint64_t const& MultiObjectiveModelCheckerEnvironment::getMaxSteps() const { + return maxSteps.get(); + } + + void MultiObjectiveModelCheckerEnvironment::setMaxSteps(uint64_t const& value) { + maxSteps = value; + } + + void MultiObjectiveModelCheckerEnvironment::unsetMaxSteps() { + maxSteps = boost::none; + } +} \ No newline at end of file diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h new file mode 100644 index 000000000..f1d4f0203 --- /dev/null +++ b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h @@ -0,0 +1,48 @@ +#pragma once + +#include + +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" +#include "storm/modelchecker/multiobjective/MultiObjectiveModelCheckingMethod.h" +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + + class MultiObjectiveModelCheckerEnvironment { + public: + + MultiObjectiveModelCheckerEnvironment(); + ~MultiObjectiveModelCheckerEnvironment(); + + storm::modelchecker::multiobjective::MultiObjectiveMethod const& getMethod() const; + void setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod value); + + bool isExportPlotSet() const; + boost::optional getPlotPathUnderApproximation() const; + void setPlotPathUnderApproximation(std::string const& path); + void unsetPlotPathUnderApproximation(); + boost::optional getPlotPathOverApproximation() const; + void setPlotPathOverApproximation(std::string const& path); + void unsetPlotPathOverApproximation(); + boost::optional getPlotPathParetoPoints() const; + void setPlotPathParetoPoints(std::string const& path); + void unsetPlotPathParetoPoints(); + + storm::RationalNumber const& getPrecision() const; + void setPrecision(storm::RationalNumber const& value); + + uint64_t const& getMaxSteps() const; + bool isMaxStepsSet() const; + void setMaxSteps(uint64_t const& value); + void unsetMaxSteps(); + + + private: + storm::modelchecker::multiobjective::MultiObjectiveMethod method; + boost::optional plotPathUnderApprox, plotPathOverApprox, plotPathParetoPoints; + storm::RationalNumber precision; + boost::optional maxSteps; + + }; +} + diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index 10276ffa6..bb18e9385 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/utility/macros.h" - +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -74,8 +74,8 @@ namespace storm { result = query->check(env); - if(storm::settings::getModule().isExportPlotSet()) { - query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); + if (env.modelchecker().multi().isExportPlotSet()) { + query->exportPlotOfCurrentApproximation(env); } break; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index 409bd9ba9..b8ac5fe2d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -7,9 +7,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" + #include "storm/exceptions/InvalidOperationException.h" @@ -57,7 +56,7 @@ namespace storm { template bool SparsePcaaAchievabilityQuery::checkAchievability(Environment const& env) { // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx. - while(!this->maxStepsPerformed()){ + while(!this->maxStepsPerformed(env)){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecision(separatingVector); this->performRefinementStep(env, std::move(separatingVector)); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index fe7a7b367..93c04e527 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -7,10 +7,7 @@ #include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" -#include "storm/settings/modules/GeneralSettings.h" - +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" namespace storm { namespace modelchecker { @@ -19,20 +16,19 @@ namespace storm { template SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult::QueryType::Pareto, "Invalid query Type"); + } + + template + std::unique_ptr SparsePcaaParetoQuery::check(Environment const& env) { // Set the precision of the weight vector checker - typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); + typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); weightedPrecision /= storm::utility::sqrt(storm::utility::convertNumber(this->objectives.size())); // multiobjPrecision / sqrt(numObjectives) is the largest possible value for which termination is guaranteed. // Lets be a little bit more precise to reduce the number of required iterations. weightedPrecision *= storm::utility::convertNumber(0.9); this->weightVectorChecker->setWeightedPrecision(weightedPrecision); - - } - - template - std::unique_ptr SparsePcaaParetoQuery::check(Environment const& env) { - + // refine the approximation exploreSetOfAchievablePoints(env); @@ -55,13 +51,13 @@ namespace storm { void SparsePcaaParetoQuery::exploreSetOfAchievablePoints(Environment const& env) { //First consider the objectives individually - for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(); ++objIndex) { + for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(env); ++objIndex) { WeightVector direction(this->objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); this->performRefinementStep(env, std::move(direction)); } - while(!this->maxStepsPerformed()) { + while(!this->maxStepsPerformed(env)) { // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation std::vector> underApproxHalfspaces = this->underApproximation->getHalfspaces(); std::vector overApproxVertices = this->overApproximation->getVertices(); @@ -76,7 +72,7 @@ namespace storm { } } } - if(farestDistance < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + if(farestDistance < storm::utility::convertNumber(env.modelchecker().multi().getPrecision())) { // Goal precision reached! return; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 538752ab2..4df353cdd 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -8,9 +8,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" -#include "storm/settings/modules/GeneralSettings.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/exceptions/InvalidOperationException.h" @@ -99,7 +97,7 @@ namespace storm { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); - while(!this->maxStepsPerformed()){ + while(!this->maxStepsPerformed(env)){ WeightVector separatingVector = this->findSeparatingVector(thresholds); this->updateWeightedPrecisionInAchievabilityPhase(separatingVector); this->performRefinementStep(env, std::move(separatingVector)); @@ -150,10 +148,10 @@ namespace storm { // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. GeometryValueType result = storm::utility::zero(); - while(!this->maxStepsPerformed()) { + while(!this->maxStepsPerformed(env)) { if (this->refinementSteps.empty()) { // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective). - this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(env.modelchecker().multi().getPrecision())); WeightVector separatingVector = directionOfOptimizingObjective; this->performRefinementStep(env, std::move(separatingVector)); } @@ -165,7 +163,7 @@ namespace storm { optimizationRes = this->overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); if (optimizationRes.second) { GeometryValueType precisionOfResult = optimizationRes.first[indexOfOptimizingObjective] - result; - if (precisionOfResult < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + if (precisionOfResult < storm::utility::convertNumber(env.modelchecker().multi().getPrecision())) { // Goal precision reached! return result; } else { @@ -176,7 +174,7 @@ namespace storm { thresholds[indexOfOptimizingObjective] = result + storm::utility::one(); } WeightVector separatingVector = this->findSeparatingVector(thresholds); - this->updateWeightedPrecisionInImprovingPhase(separatingVector); + this->updateWeightedPrecisionInImprovingPhase(env, separatingVector); this->performRefinementStep(env, std::move(separatingVector)); } STORM_LOG_ERROR("Could not reach the desired precision: Exceeded maximum number of refinement steps"); @@ -185,11 +183,11 @@ namespace storm { template - void SparsePcaaQuantitativeQuery::updateWeightedPrecisionInImprovingPhase(WeightVector const& weights) { + void SparsePcaaQuantitativeQuery::updateWeightedPrecisionInImprovingPhase(Environment const& env, WeightVector const& weights) { STORM_LOG_THROW(!storm::utility::isZero(weights[this->indexOfOptimizingObjective]), exceptions::UnexpectedException, "The chosen weight-vector gives zero weight for the objective that is to be optimized."); // If weighs[indexOfOptimizingObjective] is low, the computation of the weightVectorChecker needs to be more precise. // Our heuristic ensures that if p is the new vertex of the under-approximation, then max{ eps | p' = p + (0..0 eps 0..0) is in the over-approximation } <= multiobjective_precision/0.9 - GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber(storm::settings::getModule().getPrecision()); + GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); // Normalize by division with the Euclidean Norm of the weight-vector weightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weights, weights)); weightedPrecision *= storm::utility::convertNumber(0.9); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index 164a87f21..234e6f291 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h @@ -45,7 +45,7 @@ namespace storm { * Updates the precision of the weightVectorChecker w.r.t. the provided weights */ void updateWeightedPrecisionInAchievabilityPhase(WeightVector const& weights); - void updateWeightedPrecisionInImprovingPhase(WeightVector const& weights); + void updateWeightedPrecisionInImprovingPhase(Environment const& env, WeightVector const& weights); /* * Given that the thresholds are achievable, this function further refines the approximations and returns the optimized value diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 2164665e0..ef7e50d80 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -5,8 +5,7 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/multiobjective/Objective.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" @@ -126,9 +125,9 @@ namespace storm { } template - bool SparsePcaaQuery::maxStepsPerformed() const { - return storm::settings::getModule().isMaxStepsSet() && - this->refinementSteps.size() >= storm::settings::getModule().getMaxSteps(); + bool SparsePcaaQuery::maxStepsPerformed(Environment const& env) const { + return env.modelchecker().multi().isMaxStepsSet() && + this->refinementSteps.size() >= env.modelchecker().multi().getMaxSteps(); } @@ -191,7 +190,7 @@ namespace storm { } template - void SparsePcaaQuery::exportPlotOfCurrentApproximation(std::string const& destinationDir) const { + 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."); @@ -223,35 +222,33 @@ namespace storm { std::vector columnHeaders = {"x", "y"}; std::vector> pointsForPlotting; - underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(underApproxVertices.size()); - for(auto const& v : underApproxVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); - } - storm::utility::exportDataToCSVFile(destinationDir + "underapproximation.csv", pointsForPlotting, columnHeaders); - - pointsForPlotting.clear(); - overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(overApproxVertices.size()); - for(auto const& v : overApproxVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + if (env.modelchecker().multi().getPlotPathUnderApproximation()) { + underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(underApproxVertices.size()); + for(auto const& v : underApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathUnderApproximation().get(), pointsForPlotting, columnHeaders); } - storm::utility::exportDataToCSVFile(destinationDir + "overapproximation.csv", pointsForPlotting, columnHeaders); - pointsForPlotting.clear(); - pointsForPlotting.reserve(paretoPoints.size()); - for(auto const& v : paretoPoints) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + if (env.modelchecker().multi().getPlotPathOverApproximation()) { + pointsForPlotting.clear(); + overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(overApproxVertices.size()); + for(auto const& v : overApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathOverApproximation().get(), pointsForPlotting, columnHeaders); } - storm::utility::exportDataToCSVFile(destinationDir + "paretopoints.csv", pointsForPlotting, columnHeaders); - pointsForPlotting.clear(); - auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder(); - pointsForPlotting.reserve(4); - for(auto const& v : boundVertices) { - pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + if (env.modelchecker().multi().getPlotPathParetoPoints()) { + pointsForPlotting.clear(); + pointsForPlotting.reserve(paretoPoints.size()); + for(auto const& v : paretoPoints) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathParetoPoints().get(), pointsForPlotting, columnHeaders); } - storm::utility::exportDataToCSVFile(destinationDir + "boundaries.csv", pointsForPlotting, columnHeaders); } #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index d92f0ccee..630503a08 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -38,7 +38,7 @@ namespace storm { * Note that the approximations will be intersected with a (sufficiently large) hyperrectangle in order to ensure that the polytopes are bounded * This only works for 2 dimensional queries. */ - void exportPlotOfCurrentApproximation(std::string const& destinationDir) const; + void exportPlotOfCurrentApproximation(Environment const& env) const; protected: @@ -87,7 +87,7 @@ namespace storm { /* * Returns true iff the maximum number of refinement steps (as possibly specified in the settings) has been reached */ - bool maxStepsPerformed() const; + 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).