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> solverEnvironment;
+ SubEnvironment<ModelCheckerEnvironment> 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> solverEnvironment;
+ SubEnvironment<InternalEnvironment> 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<memory>
+#include <memory>
+
+#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<InternalEnvironment>;
+
+ template class SubEnvironment<MultiObjectiveModelCheckerEnvironment>;
+ template class SubEnvironment<ModelCheckerEnvironment>;
+
template class SubEnvironment<SolverEnvironment>;
template class SubEnvironment<EigenSolverEnvironment>;
template class SubEnvironment<GmmxxSolverEnvironment>;
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 <memory>
+#include <boost/optional.hpp>
+
+#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> 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<storm::settings::modules::MultiObjectiveSettings>();
+ 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<storm::RationalNumber>(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<std::string> MultiObjectiveModelCheckerEnvironment::getPlotPathUnderApproximation() const {
+ return plotPathUnderApprox;
+ }
+
+ void MultiObjectiveModelCheckerEnvironment::setPlotPathUnderApproximation(std::string const& path) {
+ plotPathUnderApprox = path;
+ }
+
+ void MultiObjectiveModelCheckerEnvironment::unsetPlotPathUnderApproximation() {
+ plotPathUnderApprox = boost::none;
+ }
+
+ boost::optional<std::string> MultiObjectiveModelCheckerEnvironment::getPlotPathOverApproximation() const {
+ return plotPathOverApprox;
+ }
+
+ void MultiObjectiveModelCheckerEnvironment::setPlotPathOverApproximation(std::string const& path) {
+ plotPathOverApprox = path;
+ }
+
+ void MultiObjectiveModelCheckerEnvironment::unsetPlotPathOverApproximation() {
+ plotPathOverApprox = boost::none;
+ }
+
+ boost::optional<std::string> 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 <string>
+
+#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<std::string> getPlotPathUnderApproximation() const;
+ void setPlotPathUnderApproximation(std::string const& path);
+ void unsetPlotPathUnderApproximation();
+ boost::optional<std::string> getPlotPathOverApproximation() const;
+ void setPlotPathOverApproximation(std::string const& path);
+ void unsetPlotPathOverApproximation();
+ boost::optional<std::string> 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<std::string> plotPathUnderApprox, plotPathOverApprox, plotPathParetoPoints;
+ storm::RationalNumber precision;
+ boost::optional<uint64_t> 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<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) {
- query->exportPlotOfCurrentApproximation(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().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 <class SparseModelType, typename GeometryValueType>
bool SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::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 <class SparseModelType, typename GeometryValueType>
SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto, "Invalid query Type");
+ }
+
+ template <class SparseModelType, typename GeometryValueType>
+ std::unique_ptr<CheckResult> SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::check(Environment const& env) {
// Set the precision of the weight vector checker
- typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber<typename SparseModelType::ValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
+ typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber<typename SparseModelType::ValueType>(env.modelchecker().multi().getPrecision());
weightedPrecision /= storm::utility::sqrt(storm::utility::convertNumber<typename SparseModelType::ValueType, uint_fast64_t>(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<typename SparseModelType::ValueType>(0.9);
this->weightVectorChecker->setWeightedPrecision(weightedPrecision);
-
- }
-
- template <class SparseModelType, typename GeometryValueType>
- std::unique_ptr<CheckResult> SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::check(Environment const& env) {
-
+
// refine the approximation
exploreSetOfAchievablePoints(env);
@@ -55,13 +51,13 @@ namespace storm {
void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchievablePoints(Environment const& env) {
//First consider the objectives individually
- for(uint_fast64_t objIndex = 0; objIndex<this->objectives.size() && !this->maxStepsPerformed(); ++objIndex) {
+ for(uint_fast64_t objIndex = 0; objIndex<this->objectives.size() && !this->maxStepsPerformed(env); ++objIndex) {
WeightVector direction(this->objectives.size(), storm::utility::zero<GeometryValueType>());
direction[objIndex] = storm::utility::one<GeometryValueType>();
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<storm::storage::geometry::Halfspace<GeometryValueType>> underApproxHalfspaces = this->underApproximation->getHalfspaces();
std::vector<Point> overApproxVertices = this->overApproximation->getVertices();
@@ -76,7 +72,7 @@ namespace storm {
}
}
}
- if(farestDistance < storm::utility::convertNumber<GeometryValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision())) {
+ if(farestDistance < storm::utility::convertNumber<GeometryValueType>(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<GeometryValueType>();
- 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<typename SparseModelType::ValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()));
+ this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(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<GeometryValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision())) {
+ if (precisionOfResult < storm::utility::convertNumber<GeometryValueType>(env.modelchecker().multi().getPrecision())) {
// Goal precision reached!
return result;
} else {
@@ -176,7 +174,7 @@ namespace storm {
thresholds[indexOfOptimizingObjective] = result + storm::utility::one<GeometryValueType>();
}
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 <class SparseModelType, typename GeometryValueType>
- void SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::updateWeightedPrecisionInImprovingPhase(WeightVector const& weights) {
+ void SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::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<GeometryValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
+ GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber<GeometryValueType>(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<GeometryValueType>(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 <class SparseModelType, typename GeometryValueType>
- bool SparsePcaaQuery<SparseModelType, GeometryValueType>::maxStepsPerformed() const {
- return storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet() &&
- this->refinementSteps.size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxSteps();
+ bool SparsePcaaQuery<SparseModelType, GeometryValueType>::maxStepsPerformed(Environment const& env) const {
+ return env.modelchecker().multi().isMaxStepsSet() &&
+ this->refinementSteps.size() >= env.modelchecker().multi().getMaxSteps();
}
@@ -191,7 +190,7 @@ namespace storm {
}
template<typename SparseModelType, typename GeometryValueType>
- void SparsePcaaQuery<SparseModelType, GeometryValueType>::exportPlotOfCurrentApproximation(std::string const& destinationDir) const {
+ 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.");
@@ -223,35 +222,33 @@ namespace storm {
std::vector<std::string> columnHeaders = {"x", "y"};
std::vector<std::vector<double>> pointsForPlotting;
- underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
- pointsForPlotting.reserve(underApproxVertices.size());
- for(auto const& v : underApproxVertices) {
- pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
- }
- storm::utility::exportDataToCSVFile<double, std::string>(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<double>(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<double>(v));
+ }
+ storm::utility::exportDataToCSVFile<double, std::string>(env.modelchecker().multi().getPlotPathUnderApproximation().get(), pointsForPlotting, columnHeaders);
}
- storm::utility::exportDataToCSVFile<double, std::string>(destinationDir + "overapproximation.csv", pointsForPlotting, columnHeaders);
- pointsForPlotting.clear();
- pointsForPlotting.reserve(paretoPoints.size());
- for(auto const& v : paretoPoints) {
- pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(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<double>(v));
+ }
+ storm::utility::exportDataToCSVFile<double, std::string>(env.modelchecker().multi().getPlotPathOverApproximation().get(), pointsForPlotting, columnHeaders);
}
- storm::utility::exportDataToCSVFile<double, std::string>(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<double>(v));
+ if (env.modelchecker().multi().getPlotPathParetoPoints()) {
+ pointsForPlotting.clear();
+ pointsForPlotting.reserve(paretoPoints.size());
+ for(auto const& v : paretoPoints) {
+ pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+ }
+ storm::utility::exportDataToCSVFile<double, std::string>(env.modelchecker().multi().getPlotPathParetoPoints().get(), pointsForPlotting, columnHeaders);
}
- storm::utility::exportDataToCSVFile<double, std::string>(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).