multi objective settings

Former-commit-id: d43af99080

src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp

@@ -5,6 +5,9 @@
 #include "src/models/sparse/StandardRewardModel.h"
 #include "src/utility/constants.h"
 #include "src/utility/vector.h"
+#include "src/settings//SettingsManager.h"
+#include "src/settings/modules/MultiObjectiveSettings.h"
+
 
 #include "src/exceptions/UnexpectedException.h"
 
@@ -12,6 +15,17 @@ namespace storm {
     namespace modelchecker {
         namespace helper {
             
+            template <class SparseModelType, typename RationalNumberType>
+            SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::SparseMultiObjectiveModelCheckerHelper(Information& info) : info(info), weightedObjectivesChecker(info), numIterations(0) {
+                overApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
+                underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
+            }
+            
+            template <class SparseModelType, typename RationalNumberType>
+            SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::~SparseMultiObjectiveModelCheckerHelper() {
+                // Intentionally left empty
+            }
+            
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::check(Information & info) {
                 SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType> helper(info);
@@ -21,7 +35,6 @@ namespace storm {
                         ++numOfObjectivesWithoutThreshold;
                     }
                 }
-                
                 if(numOfObjectivesWithoutThreshold == 0) {
                     helper.achievabilityQuery();
                 } else if (numOfObjectivesWithoutThreshold == 1) {
@@ -33,17 +46,6 @@ namespace storm {
                 }
             }
             
-            template <class SparseModelType, typename RationalNumberType>
-            SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::SparseMultiObjectiveModelCheckerHelper(Information& info) : info(info), weightedObjectivesChecker(info) {
-                overApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
-                underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
-            }
-            
-            template <class SparseModelType, typename RationalNumberType>
-            SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::~SparseMultiObjectiveModelCheckerHelper() {
-                // Intentionally left empty
-            }
-            
             template <class SparseModelType, typename RationalNumberType>
             void SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::achievabilityQuery() {
                 Point thresholds;
@@ -56,18 +58,22 @@ namespace storm {
                 }
                 
                 storm::storage::BitVector individualObjectivesToBeChecked(info.objectives.size(), true);
-                while(true) { //TODO introduce convergence criterion? (like max num of iterations)
+                bool converged=false;
+                do {
                     WeightVector separatingVector = findSeparatingVector(thresholds, individualObjectivesToBeChecked);
                     refineSolution(separatingVector);
+                    ++numIterations;
+                    // Check for convergence
                     if(!checkIfThresholdsAreSatisfied(overApproximation, thresholds, strictThresholds)){
                         std::cout << "PROPERTY VIOLATED" << std::endl;
-                        return;
+                        converged=true;
                     }
                     if(checkIfThresholdsAreSatisfied(underApproximation, thresholds, strictThresholds)){
                         std::cout << "PROPERTY SATISFIED" << std::endl;
-                        return;
-                    }
+                        converged=true;
                     }
+                    converged |= (storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxIterationsSet() && numIterations >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxIterations());
+                } while(!converged);
             }
             
             template <class SparseModelType, typename RationalNumberType>
@@ -129,8 +135,7 @@ namespace storm {
                     if(optimizationRes.second) {
                         RationalNumberType upperBoundOnOptimum = optimizationRes.first[optimizingObjIndex];
                         STORM_LOG_DEBUG("Solution can be improved by at most " << storm::utility::convertNumber<double>(upperBoundOnOptimum - thresholds[optimizingObjIndex]));
-                        if(storm::utility::convertNumber<double>(upperBoundOnOptimum - thresholds[optimizingObjIndex]) < 0.0001) { //TODO get this value from settings
-                            std::cout << "Found Optimum: " << storm::utility::convertNumber<double>(thresholds[optimizingObjIndex]) << "." << std::endl;
+                        if(storm::utility::convertNumber<double>(upperBoundOnOptimum - thresholds[optimizingObjIndex]) < storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()) {                            std::cout << "Found Optimum: " << storm::utility::convertNumber<double>(thresholds[optimizingObjIndex]) << "." << std::endl;
                             if(!checkIfThresholdsAreSatisfied(underApproximation, thresholds, strictThresholds)) {
                                 std::cout << "Optimum is only the supremum" << std::endl;
                             }
@@ -169,7 +174,7 @@ namespace storm {
                         }
                     }
                     STORM_LOG_DEBUG("Farest distance between under- and overApproximation is " << storm::utility::convertNumber<double>(farestDistance));
-                    if(storm::utility::convertNumber<double>(farestDistance) > -0.0001) { //todo take this value from settings
+                    if(-storm::utility::convertNumber<double>(farestDistance) < storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()) {
                         std::cout << "DONE computing the pareto curve" << std::endl;
                         return;
                     }

src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h

@@ -67,6 +67,8 @@ namespace storm {
                 std::map<Point, std::vector<WeightVector>> paretoOptimalPoints;
                 std::unordered_map<storm::storage::TotalScheduler, typename std::map<Point, std::vector<WeightVector>>::iterator> schedulers;
                 
+                uint_fast64_t numIterations;
+                
                 std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> overApproximation;
                 std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> underApproximation;
             };

src/settings/SettingsManager.cpp

@@ -29,6 +29,7 @@
 #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
 #include "src/settings/modules/ExplorationSettings.h"
+#include "src/settings/modules/MultiObjectiveSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -516,6 +517,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::ParametricSettings>();
             storm::settings::addModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>();
             storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
+            storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
         }
 
     }

src/settings/modules/MultiObjectiveSettings.cpp

@@ -0,0 +1,49 @@
+#include "src/settings/modules/MultiObjectiveSettings.h"
+
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string MultiObjectiveSettings::moduleName = "multiobjective";
+            const std::string MultiObjectiveSettings::exportResultFileOptionName = "resultfile";
+            const std::string MultiObjectiveSettings::precisionOptionName = "precision";
+            const std::string MultiObjectiveSettings::maxIterationsOptionName = "maxiterations";
+            
+            MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportResultFileOptionName, true, "Saves the result as LaTeX document.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "A path to a file where the result should be saved.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.")
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision. Default is 1e-04.").setDefaultValueDouble(1e-04).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maxIterationsOptionName, true, "Aborts the computation after the given number of iterations (= computed pareto optimal points).")
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of iterations to be performed.").build()).build());
+            }
+            
+            bool MultiObjectiveSettings::exportResultToFile() const {
+                return this->getOption(exportResultFileOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string MultiObjectiveSettings::exportResultPath() const {
+                return this->getOption(exportResultFileOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            double MultiObjectiveSettings::getPrecision() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+            }
+            
+            bool MultiObjectiveSettings::isMaxIterationsSet() const {
+                return this->getOption(maxIterationsOptionName).getHasOptionBeenSet();
+            }
+            
+            uint_fast64_t MultiObjectiveSettings::getMaxIterations() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
+            }
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/settings/modules/MultiObjectiveSettings.h

@@ -0,0 +1,67 @@
+#ifndef STORM_SETTINGS_MODULES_MULTIOBJECTIVESETTINGS_H_
+#define STORM_SETTINGS_MODULES_MULTIOBJECTIVESETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for multi-objective model checking.
+             */
+            class MultiObjectiveSettings : public ModuleSettings {
+            public:
+                
+                /*!
+                 * Creates a new set of multi-objective model checking settings.
+                 */
+                MultiObjectiveSettings();
+				
+				/**
+				 * Retrieves whether the model checking result should be exported to a file.
+                 * @return  True iff the result should be exported to a file.
+                 */
+				bool exportResultToFile() const;
+				
+				/**
+				 * The path to a file location which should contain the model checking result.
+                 * @return A path to a file location.
+                 */
+				std::string exportResultPath() const;
+				
+				/**
+				 * Retrieves the desired precision for numerical- and pareto queries.
+                 * @return the desired precision for numerical- and pareto queries.
+				 */
+				double getPrecision() const;
+				
+                /*!
+                 * Retrieves whether or not a threshold for the number of performed iterations is given.
+                 *
+                 * @return True if a threshold for the number of performed iterations is given.
+                 */
+                bool isMaxIterationsSet() const;
+                
+                
+                /*!
+                 * Retrieves The maximum number of iterations that should be performed (if given).
+                 *
+                 * @return the maximum number of iterations that should be performed (if given).
+                 */
+                uint_fast64_t getMaxIterations() const;
+                
+                
+                const static std::string moduleName;
+                
+            private:
+				const static std::string exportResultFileOptionName;
+				const static std::string precisionOptionName;
+				const static std::string maxIterationsOptionName;
+            };
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_MULTIOBJECTIVESETTINGS_H_ */