Merge branch 'master' into deterministicScheds

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();
     }
 }

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;
     };
 }
 

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>;

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();
+    }
+}
+    
+

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;
+    };
+}
+

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;
+    }
+}

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;
+        
+    };
+}
+

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;
                     }

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));

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;
                     }

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);

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

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

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).