diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp index 01ef9c0cf..a057e1c5e 100644 --- a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp +++ b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp @@ -5,6 +5,7 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { MultiObjectiveModelCheckerEnvironment::MultiObjectiveModelCheckerEnvironment() { @@ -17,6 +18,22 @@ namespace storm { } precision = storm::utility::convertNumber(multiobjectiveSettings.getPrecision()); + if (multiobjectiveSettings.getPrecisionAbsolute()) { + precisionType = PrecisionType::Absolute; + } else if (multiobjectiveSettings.getPrecisionRelativeToDiff()) { + precisionType = PrecisionType::RelativeToDiff; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unhandled precision type."); + } + + if (multiobjectiveSettings.isAutoEncodingSet()) { + encodingType = EncodingType::Auto; + } else if (multiobjectiveSettings.isClassicEncodingSet()) { + encodingType = EncodingType::Classic; + } else if (multiobjectiveSettings.isFlowEncodingSet()) { + encodingType = EncodingType::Flow; + } + if (multiobjectiveSettings.isMaxStepsSet()) { maxSteps = multiobjectiveSettings.getMaxSteps(); } @@ -87,6 +104,22 @@ namespace storm { precision = value; } + typename MultiObjectiveModelCheckerEnvironment::PrecisionType const& MultiObjectiveModelCheckerEnvironment::getPrecisionType() const { + return precisionType; + } + + void MultiObjectiveModelCheckerEnvironment::setPrecisionType(PrecisionType const& value) { + precisionType = value; + } + + typename MultiObjectiveModelCheckerEnvironment::EncodingType const& MultiObjectiveModelCheckerEnvironment::getEncodingType() const { + return encodingType; + } + + void MultiObjectiveModelCheckerEnvironment::setEncodingType(EncodingType const& value) { + encodingType = value; + } + bool MultiObjectiveModelCheckerEnvironment::isMaxStepsSet() const { return maxSteps.is_initialized(); } diff --git a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h index a04b6c94b..7c8df5211 100644 --- a/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h +++ b/src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h @@ -12,6 +12,17 @@ namespace storm { class MultiObjectiveModelCheckerEnvironment { public: + enum class PrecisionType { + Absolute, /// Absolute precision + RelativeToDiff /// Relative to the difference between largest and smallest objective value(s) + }; + + enum class EncodingType { + Auto, /// Pick automatically + Classic, /// The classic backwards encoding + Flow /// The encoding as a flow network + }; + MultiObjectiveModelCheckerEnvironment(); ~MultiObjectiveModelCheckerEnvironment(); @@ -31,6 +42,11 @@ namespace storm { storm::RationalNumber const& getPrecision() const; void setPrecision(storm::RationalNumber const& value); + PrecisionType const& getPrecisionType() const; + void setPrecisionType(PrecisionType const& value); + + EncodingType const& getEncodingType() const; + void setEncodingType(EncodingType const& value); bool isMaxStepsSet() const; uint64_t const& getMaxSteps() const; @@ -49,6 +65,8 @@ namespace storm { storm::modelchecker::multiobjective::MultiObjectiveMethod method; boost::optional plotPathUnderApprox, plotPathOverApprox, plotPathParetoPoints; storm::RationalNumber precision; + PrecisionType precisionType; + EncodingType encodingType; boost::optional maxSteps; boost::optional schedulerRestriction; bool printResults; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 423394453..c7be2fc7e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -22,7 +22,8 @@ namespace storm { template std::unique_ptr SparsePcaaParetoQuery::check(Environment const& env) { - + STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type."); + // Set the precision of the weight vector checker typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); weightedPrecision /= storm::utility::sqrt(storm::utility::convertNumber(this->objectives.size())); @@ -51,7 +52,8 @@ namespace storm { template void SparsePcaaParetoQuery::exploreSetOfAchievablePoints(Environment const& env) { - + STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type."); + //First consider the objectives individually for(uint_fast64_t objIndex = 0; objIndexobjectives.size() && !this->maxStepsPerformed(env); ++objIndex) { WeightVector direction(this->objectives.size(), storm::utility::zero()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index afffc1f92..d43aec7c6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -138,6 +138,7 @@ namespace storm { template GeometryValueType SparsePcaaQuantitativeQuery::improveSolution(Environment const& env) { + STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type."); this->diracWeightVectorsToBeChecked.clear(); // Only check weight vectors that can actually improve the solution WeightVector directionOfOptimizingObjective(this->objectives.size(), storm::utility::zero()); @@ -185,6 +186,7 @@ namespace storm { template 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."); + STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute, storm::exceptions::IllegalArgumentException, "Unhandled multiobjective precision type."); // 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(env.modelchecker().multi().getPrecision()); diff --git a/src/storm/settings/modules/MultiObjectiveSettings.cpp b/src/storm/settings/modules/MultiObjectiveSettings.cpp index e13d920c9..a263d030e 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.cpp +++ b/src/storm/settings/modules/MultiObjectiveSettings.cpp @@ -18,21 +18,27 @@ namespace storm { const std::string MultiObjectiveSettings::maxStepsOptionName = "maxsteps"; const std::string MultiObjectiveSettings::schedulerRestrictionOptionName = "schedrest"; const std::string MultiObjectiveSettings::printResultsOptionName = "printres"; + const std::string MultiObjectiveSettings::encodingOptionName = "encoding"; MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) { std::vector methods = {"pcaa", "constraintbased"}; this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory in which the results will be saved.").build()).build()); + std::vector precTypes = {"abs", "reldiff"}; this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.").setIsAdvanced() - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type of precision.").setDefaultValueString("abs").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(precTypes)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build()); std::vector memoryPatterns = {"positional", "goalmemory", "arbitrary"}; this->addOption(storm::settings::OptionBuilder(moduleName, schedulerRestrictionOptionName, false, "Restricts the class of considered schedulers to non-randomized schedulers with the provided memory pattern.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("memorypattern", "The Pattern of the memory.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memoryPatterns)).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("memorypattern", "The Pattern of the memory.").setDefaultValueString("positional").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memoryPatterns)).build()) .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("memorystates", "The Number of memory states (only if supported by the pattern).").setDefaultValueUnsignedInteger(0).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, printResultsOptionName, true, "Prints intermediate results of the computation to standard output.").build()); + std::vector encodingTypes = {"auto", "classic", "flow"}; + this->addOption(storm::settings::OptionBuilder(moduleName, encodingOptionName, true, "The prefered type of encoding for constraint-based methods.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type.").setDefaultValueString("auto").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(encodingTypes)).build()).build()); } storm::modelchecker::multiobjective::MultiObjectiveMethod MultiObjectiveSettings::getMultiObjectiveMethod() const { @@ -61,6 +67,14 @@ namespace storm { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } + bool MultiObjectiveSettings::getPrecisionRelativeToDiff() const { + return this->getOption(precisionOptionName).getArgumentByName("type").getValueAsString() == "reldiff"; + } + + bool MultiObjectiveSettings::getPrecisionAbsolute() const { + return this->getOption(precisionOptionName).getArgumentByName("type").getValueAsString() == "abs"; + } + bool MultiObjectiveSettings::isMaxStepsSet() const { return this->getOption(maxStepsOptionName).getHasOptionBeenSet(); } @@ -99,6 +113,18 @@ namespace storm { return this->getOption(printResultsOptionName).getHasOptionBeenSet(); } + bool MultiObjectiveSettings::isClassicEncodingSet() const { + return this->getOption(encodingOptionName).getArgumentByName("type").getValueAsString() == "classic"; + } + + bool MultiObjectiveSettings::isFlowEncodingSet() const { + return this->getOption(encodingOptionName).getArgumentByName("type").getValueAsString() == "flow"; + } + + bool MultiObjectiveSettings::isAutoEncodingSet() const { + return this->getOption(encodingOptionName).getArgumentByName("type").getValueAsString() == "auto"; + } + bool MultiObjectiveSettings::check() const { std::shared_ptr> validator = ArgumentValidatorFactory::createWritableFileValidator(); diff --git a/src/storm/settings/modules/MultiObjectiveSettings.h b/src/storm/settings/modules/MultiObjectiveSettings.h index 265c77e3e..75b9f2ecb 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.h +++ b/src/storm/settings/modules/MultiObjectiveSettings.h @@ -43,6 +43,16 @@ namespace storm { */ double getPrecision() const; + /** + * Retrieves whether the desired precision is considered to be absolute. + */ + bool getPrecisionAbsolute() const; + + /** + * Retrieves whether the desired precision is considered to be relative to the difference between highest and lowest objective value(s) + */ + bool getPrecisionRelativeToDiff() const; + /*! * Retrieves whether or not a threshold for the number of performed refinement steps is given. * @@ -74,6 +84,20 @@ namespace storm { */ bool isPrintResultsSet() const; + /*! + * Retrieves whether the classic encoding for constraint-based methods is to be preferred. + */ + bool isClassicEncodingSet() const; + + /*! + * Retrieves whether the flow encoding for constraint-based methods is to be preferred. + */ + bool isFlowEncodingSet() const; + + /*! + * Retrieves whether the encoding for constraint-based methods should be picked automatically. + */ + bool isAutoEncodingSet() const; /*! * Checks whether the settings are consistent. If they are inconsistent, an exception is thrown. @@ -92,6 +116,7 @@ namespace storm { const static std::string maxStepsOptionName; const static std::string schedulerRestrictionOptionName; const static std::string printResultsOptionName; + const static std::string encodingOptionName; }; } // namespace modules