From d5f1e6d5e77dd1b7ad3bc6d3768ad9005214ed3a Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 12 Jun 2016 19:51:05 +0200 Subject: [PATCH] multi objective settings Former-commit-id: d43af990806b6bdb7d00a544dd8ed65bb5244722 --- ...SparseMultiObjectiveModelCheckerHelper.cpp | 43 ++++++------ .../SparseMultiObjectiveModelCheckerHelper.h | 2 + src/settings/SettingsManager.cpp | 2 + .../modules/MultiObjectiveSettings.cpp | 49 ++++++++++++++ src/settings/modules/MultiObjectiveSettings.h | 67 +++++++++++++++++++ 5 files changed, 144 insertions(+), 19 deletions(-) create mode 100644 src/settings/modules/MultiObjectiveSettings.cpp create mode 100644 src/settings/modules/MultiObjectiveSettings.h diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp index 07c0a2012..677c2fb11 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp +++ b/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 + SparseMultiObjectiveModelCheckerHelper::SparseMultiObjectiveModelCheckerHelper(Information& info) : info(info), weightedObjectivesChecker(info), numIterations(0) { + overApproximation = storm::storage::geometry::Polytope::createUniversalPolytope(); + underApproximation = storm::storage::geometry::Polytope::createEmptyPolytope(); + } + + template + SparseMultiObjectiveModelCheckerHelper::~SparseMultiObjectiveModelCheckerHelper() { + // Intentionally left empty + } + template void SparseMultiObjectiveModelCheckerHelper::check(Information & info) { SparseMultiObjectiveModelCheckerHelper 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 - SparseMultiObjectiveModelCheckerHelper::SparseMultiObjectiveModelCheckerHelper(Information& info) : info(info), weightedObjectivesChecker(info) { - overApproximation = storm::storage::geometry::Polytope::createUniversalPolytope(); - underApproximation = storm::storage::geometry::Polytope::createEmptyPolytope(); - } - - template - SparseMultiObjectiveModelCheckerHelper::~SparseMultiObjectiveModelCheckerHelper() { - // Intentionally left empty - } - template void SparseMultiObjectiveModelCheckerHelper::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().isMaxIterationsSet() && numIterations >= storm::settings::getModule().getMaxIterations()); + } while(!converged); } template @@ -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(upperBoundOnOptimum - thresholds[optimizingObjIndex])); - if(storm::utility::convertNumber(upperBoundOnOptimum - thresholds[optimizingObjIndex]) < 0.0001) { //TODO get this value from settings - std::cout << "Found Optimum: " << storm::utility::convertNumber(thresholds[optimizingObjIndex]) << "." << std::endl; + if(storm::utility::convertNumber(upperBoundOnOptimum - thresholds[optimizingObjIndex]) < storm::settings::getModule().getPrecision()) { std::cout << "Found Optimum: " << storm::utility::convertNumber(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(farestDistance)); - if(storm::utility::convertNumber(farestDistance) > -0.0001) { //todo take this value from settings + if(-storm::utility::convertNumber(farestDistance) < storm::settings::getModule().getPrecision()) { std::cout << "DONE computing the pareto curve" << std::endl; return; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h index 5de54b95a..b8c32ea9d 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h @@ -67,6 +67,8 @@ namespace storm { std::map> paretoOptimalPoints; std::unordered_map>::iterator> schedulers; + uint_fast64_t numIterations; + std::shared_ptr> overApproximation; std::shared_ptr> underApproximation; }; diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 8e79c5457..94169f534 100644 --- a/src/settings/SettingsManager.cpp +++ b/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::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } } diff --git a/src/settings/modules/MultiObjectiveSettings.cpp b/src/settings/modules/MultiObjectiveSettings.cpp new file mode 100644 index 000000000..d37eaec3b --- /dev/null +++ b/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 diff --git a/src/settings/modules/MultiObjectiveSettings.h b/src/settings/modules/MultiObjectiveSettings.h new file mode 100644 index 000000000..207d9fb8a --- /dev/null +++ b/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_ */