diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index 898360c4b..f77926ec0 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/src/storm-dft/settings/modules/DFTSettings.cpp @@ -38,17 +38,17 @@ namespace storm { DFTSettings::DFTSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorIncluding(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorIncluding(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); #ifdef STORM_HAVE_Z3 diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 453528427..8a6161bc6 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -57,7 +57,11 @@ namespace storm { } template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(storm::settings::getModule().isSplitAllSet()), splitPredicates(storm::settings::getModule().isSplitPredicatesSet()), splitGuards(storm::settings::getModule().isSplitGuardsSet()), splitInitialGuards(storm::settings::getModule().isSplitInitialGuardsSet()), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(false), splitPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) { + + AbstractionSettings::SplitMode splitMode = storm::settings::getModule().getSplitMode(); + splitAll = splitMode == AbstractionSettings::SplitMode::All; + splitPredicates = splitMode == AbstractionSettings::SplitMode::NonGuard; if (storm::settings::getModule().isAddAllGuardsSet()) { std::vector guards; @@ -646,8 +650,7 @@ namespace storm { template std::vector MenuGameRefiner::preprocessPredicates(std::vector const& predicates, RefinementPredicates::Source const& source) const { - bool split = source == RefinementPredicates::Source::Guard && splitGuards; - split |= source == RefinementPredicates::Source::WeakestPrecondition && splitPredicates; + bool split = source == RefinementPredicates::Source::WeakestPrecondition && splitPredicates; split |= source == RefinementPredicates::Source::Interpolation && splitPredicates; split |= splitAll; diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 8d55cecd6..d5681ff2f 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -129,12 +129,6 @@ namespace storm { /// A flag indicating whether predicates derived from weakest preconditions shall be split before using them for refinement. bool splitPredicates; - - /// A flag indicating whether guards shall be split before using them for refinement. - bool splitGuards; - - /// A flag indicating whether the initially added guards shall be split before using them for refinement. - bool splitInitialGuards; /// A flag indicating whether all guards have been used to refine the abstraction. bool addedAllGuardsFlag; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a0f9e2999..644584740 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -63,9 +63,9 @@ namespace storm { preprocessedModel = model.asJaniModel().flattenComposition(); } - bool reuseAll = storm::settings::getModule().isReuseAllResultsSet(); - reuseQualitativeResults = reuseAll || storm::settings::getModule().isReuseQualitativeResultsSet(); - reuseQuantitativeResults = reuseAll || storm::settings::getModule().isReuseQuantitativeResultsSet(); + storm::settings::modules::AbstractionSettings::ReuseMode reuseMode = storm::settings::getModule().getReuseMode(); + reuseQualitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Qualitative; + reuseQuantitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Quantitative; } template diff --git a/src/storm/settings/Argument.cpp b/src/storm/settings/Argument.cpp index 1f4a8145d..1b7f9e1c7 100644 --- a/src/storm/settings/Argument.cpp +++ b/src/storm/settings/Argument.cpp @@ -1,5 +1,6 @@ +#include "storm/settings/Argument.h" -#include "Argument.h" +#include "storm/settings/ArgumentValidators.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/IllegalArgumentValueException.h" @@ -7,17 +8,16 @@ #include "storm/settings/ArgumentTypeInferationHelper.h" #include "storm/utility/macros.h" - namespace storm { namespace settings { template - Argument::Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) { // Intentionally left empty. } template - Argument::Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) { this->setDefaultValue(defaultValue); } @@ -51,8 +51,6 @@ namespace storm { return this->argumentType; } - - template T const& Argument::getArgumentValue() const { STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument '" << this->getName() << "', because it was neither set nor specifies a default value."); @@ -142,8 +140,8 @@ namespace storm { template bool Argument::validate(T const& value) const { bool result = true; - for (auto const& lambda : validationFunctions) { - result = result && lambda(value); + for (auto const& validator : validators) { + result &= validator->isValid(value); } return result; } diff --git a/src/storm/settings/Argument.h b/src/storm/settings/Argument.h index 6a7320a89..fb13ec7f8 100644 --- a/src/storm/settings/Argument.h +++ b/src/storm/settings/Argument.h @@ -19,40 +19,38 @@ namespace storm { - namespace settings { + namespace settings { + + template + class ArgumentValidator; /*! * This class subclasses the argument base to actually implement the pure virtual functions. This construction * is necessary so that it becomes easy to store a vector of arguments later despite variing template types, by * keeping a vector of pointers to the base class. */ - template - class Argument : public ArgumentBase { - public: - // Introduce shortcuts for validation functions. - typedef std::function userValidationFunction_t; - + template + class Argument : public ArgumentBase { + public: /*! * Creates a new argument with the given parameters. * * @param name The name of the argument. * @param description The description of the argument. - * @param validationFunctions A vector of validation functions that are to be executed upon assigning a value - * to this argument. + * @param validators A vector of validators that are to be executed upon assigning a value to this argument. * @param isOptional A flag indicating whether the argument is optional. */ - Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions); + Argument(std::string const& name, std::string const& description, std::vector>> const& validators); /*! * Creates a new argument with the given parameters. * * @param name The name of the argument. * @param description The description of the argument. - * @param validationFunctions A vector of validation functions that are to be executed upon assigning a value - * to this argument. + * @param validators A vector of validators that are to be executed upon assigning a value to this argument. * @param isOptional A flag indicating whether the argument is optional. */ - Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions, bool isOptional, T defaultValue); + Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue); virtual bool getIsOptional() const override; @@ -82,21 +80,19 @@ namespace storm { * @return The value of the argument. */ T const& getArgumentValue() const; - + virtual bool getHasDefaultValue() const override; void setFromDefaultValue() override; virtual std::string getValueAsString() const override; - + virtual int_fast64_t getValueAsInteger() const override; virtual uint_fast64_t getValueAsUnsignedInteger() const override; - virtual double getValueAsDouble() const override; - virtual bool getValueAsBoolean() const override; private: @@ -107,7 +103,7 @@ namespace storm { ArgumentType argumentType; // The validation functions that were registered for this argument. - std::vector validationFunctions; + std::vector>> validators; // A flag indicating whether this argument is optional. bool isOptional; @@ -124,7 +120,7 @@ namespace storm { * @param newDefault The new default value of the argument. */ void setDefaultValue(T const& newDefault); - + /*! * Applies all validation functions to the given value and therefore checks the validity of a value for this * argument. diff --git a/src/storm/settings/ArgumentBuilder.h b/src/storm/settings/ArgumentBuilder.h index 229bf5604..1c1e0e723 100644 --- a/src/storm/settings/ArgumentBuilder.h +++ b/src/storm/settings/ArgumentBuilder.h @@ -21,13 +21,13 @@ #include "storm/exceptions/IllegalArgumentTypeException.h" namespace storm { - namespace settings { + namespace settings { /*! * This class serves as an API for creating arguments. */ - class ArgumentBuilder { - public: + class ArgumentBuilder { + public: /*! * Creates a string argument with the given parameters. * @@ -36,8 +36,8 @@ namespace storm { * @return The builder of the argument. */ static ArgumentBuilder createStringArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::String, name, description); - return ab; + ArgumentBuilder ab(ArgumentType::String, name, description); + return ab; } /*! @@ -48,8 +48,8 @@ namespace storm { * @return The builder of the argument. */ static ArgumentBuilder createIntegerArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::Integer, name, description); - return ab; + ArgumentBuilder ab(ArgumentType::Integer, name, description); + return ab; } /*! @@ -60,8 +60,8 @@ namespace storm { * @return The builder of the argument. */ static ArgumentBuilder createUnsignedIntegerArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::UnsignedInteger, name, description); - return ab; + ArgumentBuilder ab(ArgumentType::UnsignedInteger, name, description); + return ab; } /*! @@ -72,8 +72,8 @@ namespace storm { * @return The builder of the argument. */ static ArgumentBuilder createDoubleArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::Double, name, description); - return ab; + ArgumentBuilder ab(ArgumentType::Double, name, description); + return ab; } /*! @@ -84,8 +84,8 @@ namespace storm { * @return The builder of the argument. */ static ArgumentBuilder createBooleanArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::Boolean, name, description); - return ab; + ArgumentBuilder ab(ArgumentType::Boolean, name, description); + return ab; } /*! @@ -102,19 +102,19 @@ namespace storm { #define PPCAT_NX(A, B) A ## B #define PPCAT(A, B) PPCAT_NX(A, B) -#define MACROaddValidationFunction(funcName, funcType) ArgumentBuilder& PPCAT(addValidationFunction, funcName) (storm::settings::Argument< funcType >::userValidationFunction_t userValidationFunction) { \ +#define MACROaddValidator(funcName, funcType) ArgumentBuilder& PPCAT(addValidator, funcName) (std::shared_ptr>&& validator) { \ STORM_LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type."); \ -( PPCAT(this->userValidationFunctions_, funcName) ).push_back(userValidationFunction); \ +( PPCAT(this->validators_, funcName) ).emplace_back(validator); \ return *this; \ } // Add the methods to add validation functions. - MACROaddValidationFunction(String, std::string) - MACROaddValidationFunction(Integer, int_fast64_t) - MACROaddValidationFunction(UnsignedInteger, uint_fast64_t) - MACROaddValidationFunction(Double, double) - MACROaddValidationFunction(Boolean, bool) - + MACROaddValidator(String, std::string) + MACROaddValidator(Integer, int_fast64_t) + MACROaddValidator(UnsignedInteger, uint_fast64_t) + MACROaddValidator(Double, double) + MACROaddValidator(Boolean, bool) + #define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \ STORM_LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type."); \ @@ -122,7 +122,7 @@ PPCAT(this->defaultValue_, funcName) = defaultValue; \ this->hasDefaultValue = true; \ return *this; \ } - + // Add the methods to set a default value. MACROsetDefaultValue(String, std::string) MACROsetDefaultValue(Integer, int_fast64_t) @@ -139,47 +139,47 @@ return *this; \ STORM_LOG_THROW(!this->hasBeenBuilt, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild argument with builder that was already used to build an argument."); this->hasBeenBuilt = true; switch (this->type) { - case ArgumentType::String: { + case ArgumentType::String: { if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_String, this->isOptional, this->defaultValue_String)); + return std::shared_ptr(new Argument(this->name, this->description, this->validators_String, this->isOptional, this->defaultValue_String)); } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_String)); + return std::shared_ptr(new Argument(this->name, this->description, this->validators_String)); } break; - } - case ArgumentType::Integer: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Integer)); - } - break; - case ArgumentType::UnsignedInteger: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_UnsignedInteger)); - } - break; - case ArgumentType::Double: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Double, this->isOptional, this->defaultValue_Double)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Double)); - } - break; - case ArgumentType::Boolean: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Boolean)); } - break; + case ArgumentType::Integer: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_Integer, this->isOptional, this->defaultValue_Integer)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_Integer)); + } + break; + case ArgumentType::UnsignedInteger: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_UnsignedInteger)); + } + break; + case ArgumentType::Double: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_Double, this->isOptional, this->defaultValue_Double)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_Double)); + } + break; + case ArgumentType::Boolean: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_Boolean, this->isOptional, this->defaultValue_Boolean)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->validators_Boolean)); + } + break; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException, "Argument has illegal type."); - } + } - private: + private: /*! * Creates an argument builder for an argument with the given parameters. * @@ -187,8 +187,8 @@ return *this; \ * @param name The name of the argument. * @param description The description of the argument. */ - ArgumentBuilder(ArgumentType type, std::string const& name, std::string const& description) : hasBeenBuilt(false), type(type), name(name), description(description), isOptional(false), hasDefaultValue(false), defaultValue_String(), defaultValue_Integer(), defaultValue_UnsignedInteger(), defaultValue_Double(), defaultValue_Boolean(), userValidationFunctions_String(), userValidationFunctions_Integer(), userValidationFunctions_UnsignedInteger(), userValidationFunctions_Double(), userValidationFunctions_Boolean() { - // Intentionally left empty. + ArgumentBuilder(ArgumentType type, std::string const& name, std::string const& description) : hasBeenBuilt(false), type(type), name(name), description(description), isOptional(false), hasDefaultValue(false), defaultValue_String(), defaultValue_Integer(), defaultValue_UnsignedInteger(), defaultValue_Double(), defaultValue_Boolean() { + // Intentionally left empty. } // A flag that stores whether an argument has been built using this builder. @@ -205,10 +205,10 @@ return *this; \ // A flag indicating whether the argument is optional. bool isOptional; - + // A flag that stores whether the argument has a default value. bool hasDefaultValue; - + // The default value of the argument separated by its type. std::string defaultValue_String; int_fast64_t defaultValue_Integer; @@ -217,11 +217,11 @@ return *this; \ bool defaultValue_Boolean; // The validation functions separated by their type. - std::vector::userValidationFunction_t> userValidationFunctions_String; - std::vector::userValidationFunction_t> userValidationFunctions_Integer; - std::vector::userValidationFunction_t> userValidationFunctions_UnsignedInteger; - std::vector::userValidationFunction_t> userValidationFunctions_Double; - std::vector::userValidationFunction_t> userValidationFunctions_Boolean; + std::vector>> validators_String; + std::vector>> validators_Integer; + std::vector>> validators_UnsignedInteger; + std::vector>> validators_Double; + std::vector>> validators_Boolean; }; } } diff --git a/src/storm/settings/ArgumentValidators.cpp b/src/storm/settings/ArgumentValidators.cpp new file mode 100644 index 000000000..13a1792b5 --- /dev/null +++ b/src/storm/settings/ArgumentValidators.cpp @@ -0,0 +1,186 @@ +#include "storm/settings/ArgumentValidators.h" + +#include + +#include + +#include "storm/settings/Argument.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/IllegalArgumentException.h" +#include "storm/exceptions/IllegalArgumentValueException.h" +#include "storm/exceptions/IllegalFunctionCallException.h" + + +namespace storm { + namespace settings { + + template + RangeArgumentValidator::RangeArgumentValidator(boost::optional const& lower, boost::optional const& upper, bool lowerIncluded, bool upperIncluded) : lower(lower), upper(upper), lowerIncluded(lowerIncluded), upperIncluded(upperIncluded) { + // Intentionally left empty. + } + + template + bool RangeArgumentValidator::isValid(ValueType const& value) { + bool result = true; + if (lower) { + if (lowerIncluded) { + result &= value >= lower.get(); + } else { + result &= value > lower.get(); + } + } + if (upper) { + if (upperIncluded) { + result &= value <= upper.get(); + } else { + result &= value < upper.get(); + } + } + return result; + } + + template + std::string RangeArgumentValidator::toString() const { + std::stringstream stream; + stream << "in "; + if (lower) { + if (lowerIncluded) { + stream << "["; + } else { + stream << "("; + } + stream << lower.get(); + } else { + stream << "(-inf"; + } + stream << ", "; + if (upper) { + stream << upper.get(); + if (upperIncluded) { + stream << "]"; + } else { + stream << ")"; + } + } else { + stream << "+inf)"; + } + + return stream.str(); + } + + FileValidator::FileValidator(Mode mode) : mode(mode) { + // Intentionally left empty. + } + + bool FileValidator::isValid(std::string const& filename) { + if (mode == Mode::Exists) { + // First check existence as ifstream::good apparently also returns true for directories. + struct stat info; + stat(filename.c_str(), &info); + STORM_LOG_THROW(info.st_mode & S_IFREG, storm::exceptions::IllegalArgumentValueException, "Unable to read from non-existing file '" << filename << "'."); + + // Now that we know it's a file, we can check its readability. + std::ifstream istream(filename); + STORM_LOG_THROW(istream.good(), storm::exceptions::IllegalArgumentValueException, "Unable to read from file '" << filename << "'."); + + return true; + } else if (mode == Mode::Writable) { + struct stat info; + STORM_LOG_THROW(stat (filename.c_str(), &info) != 0, storm::exceptions::IllegalArgumentValueException , "Could not open file '" << filename << "' for writing because file or directory already exists."); + + std::ofstream filestream(filename); + STORM_LOG_THROW(filestream.is_open(), storm::exceptions::IllegalArgumentValueException , "Could not open file '" << filename << "' for writing."); + filestream.close(); + std::remove(filename.c_str()); + + return true; + } + return false; + } + + std::string FileValidator::toString() const { + if (mode == Mode::Exists) { + return "existing file"; + } else { + return "writable file"; + } + } + + MultipleChoiceValidator::MultipleChoiceValidator(std::vector const& legalValues) : legalValues(legalValues) { + // Intentionally left empty. + } + + bool MultipleChoiceValidator::isValid(std::string const& value) { + for (auto const& legalValue : legalValues) { + if (legalValue == value) { + return true; + } + } + return false; + } + + std::string MultipleChoiceValidator::toString() const { + return "in {" + boost::join(legalValues, ", ") + "}"; + } + + std::shared_ptr> ArgumentValidatorFactory::createIntegerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound) { + return createRangeValidatorExcluding(lowerBound, upperBound); + } + + std::shared_ptr> ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound) { + return createRangeValidatorExcluding(lowerBound, upperBound); + } + + std::shared_ptr> ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(double lowerBound, double upperBound) { + return createRangeValidatorExcluding(lowerBound, upperBound); + } + + std::shared_ptr> ArgumentValidatorFactory::createIntegerGreaterValidator(int_fast64_t lowerBound) { + return createGreaterValidator(lowerBound, false); + } + + std::shared_ptr> ArgumentValidatorFactory::createUnsignedGreaterValidator(uint64_t lowerBound) { + return createGreaterValidator(lowerBound, false); + } + + std::shared_ptr> ArgumentValidatorFactory::createDoubleGreaterValidator(double lowerBound) { + return createGreaterValidator(lowerBound, false); + } + + std::shared_ptr> ArgumentValidatorFactory::createIntegerGreaterEqualValidator(int_fast64_t lowerBound) { + return createGreaterValidator(lowerBound, true); + } + + std::shared_ptr> ArgumentValidatorFactory::createUnsignedGreaterEqualValidator(uint64_t lowerBound) { + return createGreaterValidator(lowerBound, true); + } + + std::shared_ptr> ArgumentValidatorFactory::createDoubleGreaterEqualValidator(double lowerBound) { + return createGreaterValidator(lowerBound, true); + } + + std::shared_ptr> ArgumentValidatorFactory::createExistingFileValidator() { + return std::make_unique(FileValidator::Mode::Exists); + } + + std::shared_ptr> ArgumentValidatorFactory::createWritableFileValidator() { + return std::make_unique(FileValidator::Mode::Writable); + } + + std::shared_ptr> ArgumentValidatorFactory::createMultipleChoiceValidator(std::vector const& choices) { + return std::make_unique(choices); + } + + template + std::shared_ptr> ArgumentValidatorFactory::createRangeValidatorExcluding(ValueType lowerBound, ValueType upperBound) { + return std::make_unique>(lowerBound, upperBound, false, false); + } + + template + std::shared_ptr> ArgumentValidatorFactory::createGreaterValidator(ValueType lowerBound, bool equalAllowed) { + return std::make_unique>(lowerBound, boost::none, equalAllowed, false); + } + + } +} diff --git a/src/storm/settings/ArgumentValidators.h b/src/storm/settings/ArgumentValidators.h index 5069de7c4..bbdb861f5 100644 --- a/src/storm/settings/ArgumentValidators.h +++ b/src/storm/settings/ArgumentValidators.h @@ -1,275 +1,95 @@ -#ifndef STORM_SETTINGS_ARGUMENTVALIDATORS_H_ -#define STORM_SETTINGS_ARGUMENTVALIDATORS_H_ +#pragma once -#include -#include -#include -#include -#include -#include -#include #include +#include #include -#include - -#include "storm/settings/Argument.h" -#include "storm/utility/macros.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/IllegalArgumentException.h" -#include "storm/exceptions/IllegalArgumentValueException.h" -#include "storm/exceptions/IllegalFunctionCallException.h" -#include +#include namespace storm { - namespace settings { - class ArgumentValidators { - public: - /*! - * Creates a validation function that checks whether an integer is in the given range (including the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - static std::function integerRangeValidatorIncluding(int_fast64_t lowerBound, int_fast64_t upperBound) { - return rangeValidatorIncluding(lowerBound, upperBound); - } - - /*! - * Creates a validation function that checks whether an integer is in the given range (excluding the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - static std::function integerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound) { - return rangeValidatorExcluding(lowerBound, upperBound); - } - + namespace settings { + + template + class ArgumentValidator { + public: /*! - * Creates a validation function that checks whether an integer is greater than or equal to the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. + * Checks whether the argument passes the validation. */ - static std::function integerGreaterValidatorIncluding(int_fast64_t threshold) { - return greaterValidatorIncluding(threshold); - } + virtual bool isValid(ValueType const& value) = 0; /*! - * Creates a validation function that checks whether an integer is greater than the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - static std::function integerGreaterValidatorExcluding(int_fast64_t threshold) { - return greaterValidatorExcluding(threshold); - } + * Retrieves a string representation of the valid values. + */ + virtual std::string toString() const = 0; + }; + + template + class RangeArgumentValidator : public ArgumentValidator { + public: + RangeArgumentValidator(boost::optional const& lower, boost::optional const& upper, bool lowerIncluded, bool upperIncluded); - /*! - * Creates a validation function that checks whether an unsigned integer is in the given range (including the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - static std::function unsignedIntegerRangeValidatorIncluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) { - return rangeValidatorIncluding(lowerBound, upperBound); - } + virtual bool isValid(ValueType const& value) override; + virtual std::string toString() const override; - /*! - * Creates a validation function that checks whether an unsigned integer is in the given range (excluding the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - static std::function unsignedIntegerRangeValidatorExcluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) { - return rangeValidatorExcluding(lowerBound, upperBound); - } + private: + boost::optional lower; + boost::optional upper; + bool lowerIncluded; + bool upperIncluded; + }; + + class FileValidator : public ArgumentValidator { + public: + enum class Mode { + Exists, Writable + }; - /*! - * Creates a validation function that checks whether an unsigned integer is greater than or equal to the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - static std::function unsignedIntegerGreaterValidatorIncluding(uint_fast64_t threshold) { - return greaterValidatorIncluding(threshold); - } + FileValidator(Mode mode); - /*! - * Creates a validation function that checks whether an unsigned integer is greater than the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - static std::function unsignedIntegerGreaterValidatorExcluding(uint_fast64_t threshold) { - return greaterValidatorExcluding(threshold); - } - - /*! - * Creates a validation function that checks whether a double is in the given range (including the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - static std::function doubleRangeValidatorIncluding(double lowerBound, double upperBound) { - return rangeValidatorIncluding(lowerBound, upperBound); - } + virtual bool isValid(std::string const& value) override; + virtual std::string toString() const override; - /*! - * Creates a validation function that checks whether a double is in the given range (excluding the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - static std::function doubleRangeValidatorExcluding(double lowerBound, double upperBound) { - return rangeValidatorExcluding(lowerBound, upperBound); - } + private: + Mode mode; + }; + + class MultipleChoiceValidator : public ArgumentValidator { + public: + MultipleChoiceValidator(std::vector const& legalValues); - /*! - * Creates a validation function that checks whether a double is greater than or equal to the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - static std::function doubleGreaterValidatorIncluding(double threshold) { - return greaterValidatorIncluding(threshold); - } + virtual bool isValid(std::string const& value) override; + virtual std::string toString() const override; - /*! - * Creates a validation function that checks whether a double is greater than the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - static std::function doubleGreaterValidatorExcluding(double threshold) { - return greaterValidatorExcluding(threshold); - } - - /*! - * Creates a validation function that checks whether a given string corresponds to an existing and readable - * file. - * - * @return The resulting validation function. - */ - static std::function existingReadableFileValidator() { - return [] (std::string const fileName) -> bool { - // First check existence as ifstream::good apparently als returns true for directories. - struct stat info; - stat(fileName.c_str(), &info); - STORM_LOG_THROW(info.st_mode & S_IFREG, storm::exceptions::IllegalArgumentValueException, "Unable to read from non-existing file '" << fileName << "'."); - - // Now that we know it's a file, we can check its readability. - std::ifstream istream(fileName); - STORM_LOG_THROW(istream.good(), storm::exceptions::IllegalArgumentValueException, "Unable to read from file '" << fileName << "'."); - - return true; - }; - } - - /*! - * Creates a validation function that checks whether a given string corresponds to a path to non-existing file in which we can write - * - * @return The resulting validation function. - */ - static std::function writableFileValidator() { - return [] (std::string const fileName) -> bool { - struct stat info; - STORM_LOG_THROW(stat (fileName.c_str(), &info) != 0, storm::exceptions::IllegalArgumentValueException , "Could not open file '" << fileName << "' for writing because file or directory already exists."); - - std::ofstream filestream(fileName); - STORM_LOG_THROW(filestream.is_open(), storm::exceptions::IllegalArgumentValueException , "Could not open file '" << fileName << "' for writing."); - filestream.close(); - std::remove(fileName.c_str()); - - return true; - }; - } - - /*! - * Creates a validation function that checks whether a given string is in a provided list of strings. - * - * @param list The list of valid strings. - * @return The resulting validation function. - */ - static std::function stringInListValidator(std::vector const& list) { - return [list] (std::string const& inputString) -> bool { - for (auto const& validString : list) { - if (inputString == validString) { - return true; - } - } - - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value '" << inputString << "' does not match any entry in the list of valid items."); - return false; - }; - } + private: + std::vector legalValues; + }; + + class ArgumentValidatorFactory { + public: + static std::shared_ptr> createIntegerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound); + static std::shared_ptr> createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound); + static std::shared_ptr> createDoubleRangeValidatorExcluding(double lowerBound, double upperBound); - private: - /*! - * Creates a validation function that checks whether its argument is in a given range (including the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - template - static std::function rangeValidatorIncluding(T lowerBound, T upperBound) { - return std::bind([](T lowerBound, T upperBound, T value) -> bool { - STORM_LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range."); - return true; - }, lowerBound, upperBound, std::placeholders::_1); - } + static std::shared_ptr> createIntegerGreaterValidator(int_fast64_t lowerBound); + static std::shared_ptr> createUnsignedGreaterValidator(uint64_t lowerBound); + static std::shared_ptr> createDoubleGreaterValidator(double lowerBound); - /*! - * Creates a validation function that checks whether its argument is in a given range (excluding the bounds). - * - * @param lowerBound The lower bound of the valid range. - * @param upperBound The upper bound of the valid range. - * @return The resulting validation function. - */ - template - static std::function rangeValidatorExcluding(T lowerBound, T upperBound) { - return std::bind([](T lowerBound, T upperBound, T value) -> bool { - STORM_LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range."); - return true; - }, lowerBound, upperBound, std::placeholders::_1); - } + static std::shared_ptr> createIntegerGreaterEqualValidator(int_fast64_t lowerBound); + static std::shared_ptr> createUnsignedGreaterEqualValidator(uint64_t lowerBound); + static std::shared_ptr> createDoubleGreaterEqualValidator(double lowerBound); - /*! - * Creates a validation function that checks whether its argument is greater than the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - template - static std::function greaterValidatorExcluding(T threshold) { - return std::bind([](T threshold, T value) -> bool { - STORM_LOG_THROW(threshold < value, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range."); - return true; - }, threshold, std::placeholders::_1); - } + static std::shared_ptr> createExistingFileValidator(); + static std::shared_ptr> createWritableFileValidator(); - /*! - * Creates a validation function that checks whether its argument is greater than or equal to the given threshold. - * - * @param threshold The threshold. - * @return The resulting validation function. - */ - template - static std::function greaterValidatorIncluding(T threshold) { - return std::bind([](T threshold, T value) -> bool { - STORM_LOG_THROW(threshold <= value, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range."); - return true; - }, threshold, std::placeholders::_1); - } - }; - } + static std::shared_ptr> createMultipleChoiceValidator(std::vector const& choices); + + private: + template + static std::shared_ptr> createRangeValidatorExcluding(ValueType lowerBound, ValueType upperBound); + + template + static std::shared_ptr> createGreaterValidator(ValueType lowerBound, bool equalAllowed); + }; + + } } - -#endif // STORM_SETTINGS_ARGUMENTVALIDATORS_H_ diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index e26cb3112..048c6225b 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -5,66 +5,83 @@ #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { - + const std::string AbstractionSettings::moduleName = "abstraction"; + const std::string AbstractionSettings::useDecompositionOptionName = "decomposition"; + const std::string AbstractionSettings::splitModeOptionName = "split"; const std::string AbstractionSettings::addAllGuardsOptionName = "all-guards"; - const std::string AbstractionSettings::splitPredicatesOptionName = "split-preds"; - const std::string AbstractionSettings::splitInitialGuardsOptionName = "split-init-guards"; - const std::string AbstractionSettings::splitGuardsOptionName = "split-guards"; const std::string AbstractionSettings::useInterpolationOptionName = "interpolation"; - const std::string AbstractionSettings::splitInterpolantsOptionName = "split-interpolants"; - const std::string AbstractionSettings::splitAllOptionName = "split-all"; const std::string AbstractionSettings::precisionOptionName = "precision"; const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic"; - const std::string AbstractionSettings::reuseQualitativeResultsOptionName = "reuse-qualitative"; - const std::string AbstractionSettings::reuseQuantitativeResultsOptionName = "reuse-quantitative"; - const std::string AbstractionSettings::reuseAllResultsOptionName = "reuse-all"; - const std::string AbstractionSettings::useDecompositionOptionName = "decomposition"; - + const std::string AbstractionSettings::reuseResultsOptionName = "reuse"; + AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, splitPredicatesOptionName, true, "Sets whether the predicates are split into atoms before they are added.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, splitInitialGuardsOptionName, true, "Sets whether the initial guards are split into atoms before they are added.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, splitGuardsOptionName, true, "Sets whether the guards are split into atoms before they are added.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, splitAllOptionName, true, "Sets whether all predicates are split into atoms before they are added.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - + std::vector onOff = {"on", "off"}; + + this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag ('on' or 'off').").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("on").build()) + .build()); + + std::vector splitModes = {"all", "none", "non-guard"}; + this->addOption(storm::settings::OptionBuilder(moduleName, splitModeOptionName, true, "Sets which predicates are split into atoms for the refinement.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The split mode: 'all', 'none' or 'non-guard'.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(splitModes)) + .setDefaultValueString("all").build()) + .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag ('on' or 'off').").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("on").build()) + .build()); + + + this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag ('on' or 'off').").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("on").build()) + .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + std::vector pivotHeuristic = {"nearest-max-dev", "most-prob-path", "max-weighted-dev"}; this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(pivotHeuristic)).setDefaultValueString("nearest-max-dev").build()).build()); - - this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, reuseAllResultsOptionName, true, "Sets whether to reuse all results.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.").build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(pivotHeuristic)) + .setDefaultValueString("nearest-max-dev").build()).build()); + + std::vector reuseModes = {"all", "none", "qualitative", "quantitative"}; + this->addOption(storm::settings::OptionBuilder(moduleName, reuseResultsOptionName, true, "Sets whether to reuse all results.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The reuse mode: 'all', 'none', 'qualitative' or 'quantitative'.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes)) + .setDefaultValueString("all").build()) + .build()); } - bool AbstractionSettings::isAddAllGuardsSet() const { - return this->getOption(addAllGuardsOptionName).getHasOptionBeenSet(); - } - - bool AbstractionSettings::isSplitPredicatesSet() const { - return this->getOption(splitPredicatesOptionName).getHasOptionBeenSet(); - } - - bool AbstractionSettings::isSplitInitialGuardsSet() const { - return this->getOption(splitInitialGuardsOptionName).getHasOptionBeenSet(); + bool AbstractionSettings::isUseDecompositionSet() const { + return this->getOption(useDecompositionOptionName).getHasOptionBeenSet(); } - bool AbstractionSettings::isSplitGuardsSet() const { - return this->getOption(splitGuardsOptionName).getHasOptionBeenSet(); + AbstractionSettings::SplitMode AbstractionSettings::getSplitMode() const { + std::string splitModeAsString = this->getOption(splitModeOptionName).getArgumentByName("mode").getValueAsString(); + if (splitModeAsString == "all") { + return SplitMode::All; + } else if (splitModeAsString == "none") { + return SplitMode::None; + } else if (splitModeAsString == "non-guard") { + return SplitMode::NonGuard; + } + return SplitMode::All; } - bool AbstractionSettings::isSplitAllSet() const { - return this->getOption(splitAllOptionName).getHasOptionBeenSet(); + bool AbstractionSettings::isAddAllGuardsSet() const { + return this->getOption(addAllGuardsOptionName).getArgumentByName("value").getValueAsString() == "on"; } bool AbstractionSettings::isUseInterpolationSet() const { - return this->getOption(useInterpolationOptionName).getHasOptionBeenSet(); + return this->getOption(useInterpolationOptionName).getArgumentByName("value").getValueAsString() == "on"; } double AbstractionSettings::getPrecision() const { @@ -83,22 +100,20 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown pivot selection heuristic '" << heuristicName << "'."); } - bool AbstractionSettings::isReuseQualitativeResultsSet() const { - return this->getOption(reuseQualitativeResultsOptionName).getHasOptionBeenSet(); - } - - bool AbstractionSettings::isReuseQuantitativeResultsSet() const { - return this->getOption(reuseQuantitativeResultsOptionName).getHasOptionBeenSet(); - } - - bool AbstractionSettings::isReuseAllResultsSet() const { - return this->getOption(reuseAllResultsOptionName).getHasOptionBeenSet(); + AbstractionSettings::ReuseMode AbstractionSettings::getReuseMode() const { + std::string reuseModeAsString = this->getOption(splitModeOptionName).getArgumentByName("mode").getValueAsString(); + if (reuseModeAsString == "all") { + return ReuseMode::All; + } else if (reuseModeAsString == "none") { + return ReuseMode::None; + } else if (reuseModeAsString == "qualitative") { + return ReuseMode::Qualitative; + } else if (reuseModeAsString == "quantitative") { + return ReuseMode::Quantitative; + } + return ReuseMode::All; } - bool AbstractionSettings::isUseDecompositionSet() const { - return this->getOption(useDecompositionOptionName).getHasOptionBeenSet(); - } - } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index c6d2effb8..187eaf387 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -15,45 +15,39 @@ namespace storm { NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation }; + enum class SplitMode { + All, None, NonGuard + }; + + enum class ReuseMode { + All, None, Qualitative, Quantitative + }; + /*! * Creates a new set of abstraction settings. */ AbstractionSettings(); /*! - * Retrieves whether the option to add all guards was set. - * - * @return True iff the option was set. - */ - bool isAddAllGuardsSet() const; - - /*! - * Retrieves whether the option to split predicates to atoms was set. - * - * @return True iff the option was set. - */ - bool isSplitPredicatesSet() const; - - /*! - * Retrieves whether the option to split the initially added guards to atoms was set. + * Retrieves whether the option to use the decomposition was set. * * @return True iff the option was set. */ - bool isSplitInitialGuardsSet() const; - + bool isUseDecompositionSet() const; + /*! - * Retrieves whether the option to split guards derived later to atoms was set. + * Retrieves the selected split mode. * - * @return True iff the option was set. + * @return The selected split mode. */ - bool isSplitGuardsSet() const; - + SplitMode getSplitMode() const; + /*! - * Retrieves whether the option to split all predicates to atoms was set. + * Retrieves whether the option to add all guards was set. * * @return True iff the option was set. */ - bool isSplitAllSet() const; + bool isAddAllGuardsSet() const; /*! * Retrieves whether the option to use interpolation was set. @@ -75,51 +69,24 @@ namespace storm { * @return The selected heuristic. */ PivotSelectionHeuristic getPivotSelectionHeuristic() const; - - /*! - * Retrieves whether the option to reuse the qualitative results was set. - * - * @param True iff the option was set. - */ - bool isReuseQualitativeResultsSet() const; - - /*! - * Retrieves whether the option to reuse the quantitative results was set. - * - * @param True iff the option was set. - */ - bool isReuseQuantitativeResultsSet() const; - - /*! - * Retrieves whether the option to reuse all results was set. - * - * @param True iff the option was set. - */ - bool isReuseAllResultsSet() const; /*! - * Retrieves whether the option to use the decomposition was set. + * Retrieves the selected reuse mode. * - * @return True iff the option was set. + * @return The selected reuse mode. */ - bool isUseDecompositionSet() const; + ReuseMode getReuseMode() const; const static std::string moduleName; private: + const static std::string useDecompositionOptionName; + const static std::string splitModeOptionName; const static std::string addAllGuardsOptionName; - const static std::string splitPredicatesOptionName; - const static std::string splitInitialGuardsOptionName; - const static std::string splitGuardsOptionName; const static std::string useInterpolationOptionName; - const static std::string splitInterpolantsOptionName; - const static std::string splitAllOptionName; const static std::string precisionOptionName; const static std::string pivotHeuristicOptionName; - const static std::string reuseQualitativeResultsOptionName; - const static std::string reuseQuantitativeResultsOptionName; - const static std::string reuseAllResultsOptionName; - const static std::string useDecompositionOptionName; + const static std::string reuseResultsOptionName; }; } diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 74f31429d..593049133 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -15,7 +15,7 @@ namespace storm { BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = { "strong", "weak" }; - this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used. Available are: { strong, weak }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("strong").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used. Available are: { strong, weak }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("strong").build()).build()); } bool BisimulationSettings::isStrongBisimulationSet() const { diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 2c020b27e..f34007b0e 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -10,7 +10,8 @@ #include "storm/storage/dd/DdType.h" -#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" namespace storm { namespace settings { @@ -38,22 +39,22 @@ namespace storm { std::vector engines = {"sparse", "hybrid", "dd", "expl", "abs"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, expl, abs}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, expl, abs}.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build()); std::vector linearEquationSolver = {"gmm++", "native", "eigen", "elimination"}; this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++, native, eigen, elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++, native, eigen, elimination.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); std::vector ddLibraries = {"cudd", "sylvan"}; this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(ddLibraries)).setDefaultValueString("cudd").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("cudd").build()).build()); std::vector lpSolvers = {"gurobi", "glpk"}; this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); std::vector smtSolvers = {"z3", "mathsat"}; this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtSolvers)).setDefaultValueString("z3").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtSolvers)).setDefaultValueString("z3").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA to speed up computation time.").build()); } diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp index da26e7963..2a6416298 100644 --- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp @@ -20,7 +20,7 @@ namespace storm { CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) { std::vector techniques = {"maxsat", "milp"}; this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); } diff --git a/src/storm/settings/modules/CuddSettings.cpp b/src/storm/settings/modules/CuddSettings.cpp index 6e087a6b1..ced95e7a9 100644 --- a/src/storm/settings/modules/CuddSettings.cpp +++ b/src/storm/settings/modules/CuddSettings.cpp @@ -7,6 +7,9 @@ #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { @@ -17,7 +20,7 @@ namespace storm { const std::string CuddSettings::reorderOptionName = "reorder"; CuddSettings::CuddSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build()); @@ -40,7 +43,7 @@ namespace storm { reorderingTechniques.push_back("annealing"); reorderingTechniques.push_back("genetic"); reorderingTechniques.push_back("exact"); - this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {none, random, randompivot, sift, siftconv, ssift, ssiftconv, gsift, gsiftconv, win2, win2conv, win3, win3conv, win4, win4conv, annealing, genetic, exact}.").setDefaultValueString("gsift").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reorderingTechniques)).build()).build()); } double CuddSettings::getConstantPrecision() const { diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp index 418c4172d..3bf632d7c 100644 --- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp +++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp @@ -9,6 +9,9 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/solver/SolverSelectionOptions.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { @@ -23,17 +26,17 @@ namespace storm { EigenEquationSolverSettings::EigenEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = {"sparselu", "bicgstab", "dgmres", "gmres"}; - this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the eigen solver. Available are {sparselu, bicgstab, dgmres, gmres}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("sparselu").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the eigen solver. Available are {sparselu, bicgstab, dgmres, gmres}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("sparselu").build()).build()); // Register available preconditioners. std::vector preconditioner = {"ilu", "diagonal", "none"}; - this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(preconditioner)).setDefaultValueString("ilu").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); } bool EigenEquationSolverSettings::isLinearEquationSystemMethodSet() const { diff --git a/src/storm/settings/modules/EliminationSettings.cpp b/src/storm/settings/modules/EliminationSettings.cpp index 6436e3703..752b398ef 100644 --- a/src/storm/settings/modules/EliminationSettings.cpp +++ b/src/storm/settings/modules/EliminationSettings.cpp @@ -5,6 +5,8 @@ #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" namespace storm { namespace settings { @@ -19,10 +21,10 @@ namespace storm { EliminationSettings::EliminationSettings() : ModuleSettings(moduleName) { std::vector orders = {"fw", "fwrev", "bw", "bwrev", "rand", "spen", "dpen", "regex"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen, regex}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen, regex}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(orders)).setDefaultValueString("fwrev").build()).build()); std::vector methods = {"state", "hybrid"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("state").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("state").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") diff --git a/src/storm/settings/modules/ExplorationSettings.cpp b/src/storm/settings/modules/ExplorationSettings.cpp index d3c6672de..ef4313c0d 100644 --- a/src/storm/settings/modules/ExplorationSettings.cpp +++ b/src/storm/settings/modules/ExplorationSettings.cpp @@ -6,6 +6,9 @@ #include "storm/settings/Argument.h" #include "storm/settings/SettingsManager.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { @@ -20,15 +23,15 @@ namespace storm { ExplorationSettings::ExplorationSettings() : ModuleSettings(moduleName) { std::vector types = { "local", "global" }; - this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("global").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(types)).setDefaultValueString("global").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build()); std::vector nextStateHeuristics = { "probdiffs", "prob", "unif" }; - this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision to achieve.").setShortName(precisionOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value to use to determine convergence.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value to use to determine convergence.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); } bool ExplorationSettings::isLocalPrecomputationSet() const { diff --git a/src/storm/settings/modules/GSPNSettings.cpp b/src/storm/settings/modules/GSPNSettings.cpp index d2ce22b65..9184f9137 100644 --- a/src/storm/settings/modules/GSPNSettings.cpp +++ b/src/storm/settings/modules/GSPNSettings.cpp @@ -23,9 +23,9 @@ namespace storm { GSPNSettings::GSPNSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the GSPN.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the GSPN.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, gspnToJaniOptionName, false, "Transform to JANI.").setShortName(gspnToJaniOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Capacaties as invariants for places.").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Capacaties as invariants for places.").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); } bool GSPNSettings::isGspnFileSet() const { diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp index 491f79521..6726bc9d3 100644 --- a/src/storm/settings/modules/GeneralSettings.cpp +++ b/src/storm/settings/modules/GeneralSettings.cpp @@ -44,9 +44,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, printTimeAndMemoryOptionName, false, "Prints CPU time and memory consumption at the end.").setShortName(printTimeAndMemoryOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the formulas to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula or filename", "The formula or the file containing the formulas.").build()).build()); @@ -113,6 +113,7 @@ namespace storm { } void GeneralSettings::finalize() { + // Intentionally left empty. } bool GeneralSettings::check() const { diff --git a/src/storm/settings/modules/GlpkSettings.cpp b/src/storm/settings/modules/GlpkSettings.cpp index 7d865406d..779a8c041 100644 --- a/src/storm/settings/modules/GlpkSettings.cpp +++ b/src/storm/settings/modules/GlpkSettings.cpp @@ -18,7 +18,7 @@ namespace storm { GlpkSettings::GlpkSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); } bool GlpkSettings::isOutputSet() const { diff --git a/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp b/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp index 463940446..7e194e8d6 100644 --- a/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/GmmxxEquationSolverSettings.cpp @@ -9,6 +9,9 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/solver/SolverSelectionOptions.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { @@ -24,17 +27,17 @@ namespace storm { GmmxxEquationSolverSettings::GmmxxEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = {"bicgstab", "qmr", "gmres", "jacobi"}; - this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("gmres").build()).build()); // Register available preconditioners. std::vector preconditioner = {"ilu", "diagonal", "none"}; - this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(preconditioner)).setDefaultValueString("ilu").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build()); } diff --git a/src/storm/settings/modules/GurobiSettings.cpp b/src/storm/settings/modules/GurobiSettings.cpp index d4205c2f8..4f35e085a 100644 --- a/src/storm/settings/modules/GurobiSettings.cpp +++ b/src/storm/settings/modules/GurobiSettings.cpp @@ -21,7 +21,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); } bool GurobiSettings::isIntegerToleranceSet() const { diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index c91aca05d..563b98162 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -9,6 +9,9 @@ #include "storm/exceptions/InvalidSettingsException.h" #include "storm/parser/CSVParser.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { @@ -46,12 +49,12 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); @@ -59,15 +62,15 @@ namespace storm { std::vector explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) diff --git a/src/storm/settings/modules/JaniExportSettings.cpp b/src/storm/settings/modules/JaniExportSettings.cpp index 573ad50a7..a56cbc668 100644 --- a/src/storm/settings/modules/JaniExportSettings.cpp +++ b/src/storm/settings/modules/JaniExportSettings.cpp @@ -7,8 +7,6 @@ #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" -#include "storm/exceptions/InvalidSettingsException.h" - namespace storm { namespace settings { namespace modules { diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index c02abcd20..6b7cc2863 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -21,11 +21,11 @@ namespace storm { MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration"}; this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: value-iteration (vi) and policy-iteration (pi).").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: value-iteration (vi) and policy-iteration (pi).").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("vi").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build()); } diff --git a/src/storm/settings/modules/MultiObjectiveSettings.cpp b/src/storm/settings/modules/MultiObjectiveSettings.cpp index 81f290bae..add1131ea 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.cpp +++ b/src/storm/settings/modules/MultiObjectiveSettings.cpp @@ -20,7 +20,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to a directory in which the results will 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()); + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision. Default is 1e-04.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).") .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build()); } @@ -32,6 +32,7 @@ namespace storm { std::string MultiObjectiveSettings::getExportPlotDirectory() const { return this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString(); } + double MultiObjectiveSettings::getPrecision() const { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } @@ -45,11 +46,13 @@ namespace storm { } bool MultiObjectiveSettings::check() const { + std::shared_ptr> validator = ArgumentValidatorFactory::createWritableFileValidator(); + return !isExportPlotSet() - || (ArgumentValidators::writableFileValidator()(getExportPlotDirectory() + "boundaries.csv") - && ArgumentValidators::writableFileValidator()(getExportPlotDirectory() + "overapproximation.csv") - && ArgumentValidators::writableFileValidator()(getExportPlotDirectory() + "underapproximation.csv") - && ArgumentValidators::writableFileValidator()(getExportPlotDirectory() + "paretopoints.csv")); + || (validator->isValid(getExportPlotDirectory() + "boundaries.csv") + && validator->isValid(getExportPlotDirectory() + "overapproximation.csv") + && validator->isValid(getExportPlotDirectory() + "underapproximation.csv") + && validator->isValid(getExportPlotDirectory() + "paretopoints.csv")); } } // namespace modules diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index 67f98886f..34e0daa82 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -8,6 +8,9 @@ #include "storm/settings/Argument.h" #include "storm/solver/SolverSelectionOptions.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + namespace storm { namespace settings { namespace modules { @@ -22,13 +25,13 @@ namespace storm { NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = { "jacobi", "gaussseidel", "sor" }; - this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, omegaOptionName, false, "The omega used for SOR.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value of the SOR parameter.").setDefaultValueDouble(0.9).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, omegaOptionName, false, "The omega used for SOR.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The value of the SOR parameter.").setDefaultValueDouble(0.9).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build()); } diff --git a/src/storm/settings/modules/PGCLSettings.cpp b/src/storm/settings/modules/PGCLSettings.cpp index 2a24b71fa..5035f3632 100644 --- a/src/storm/settings/modules/PGCLSettings.cpp +++ b/src/storm/settings/modules/PGCLSettings.cpp @@ -25,7 +25,7 @@ namespace storm { PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("description", "description of the variable restrictions").build()).build()); diff --git a/src/storm/settings/modules/ParametricSettings.cpp b/src/storm/settings/modules/ParametricSettings.cpp index 56e7c42dd..ba7470ac2 100644 --- a/src/storm/settings/modules/ParametricSettings.cpp +++ b/src/storm/settings/modules/ParametricSettings.cpp @@ -5,6 +5,8 @@ #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" namespace storm { namespace settings { diff --git a/src/storm/settings/modules/RegionSettings.cpp b/src/storm/settings/modules/RegionSettings.cpp index 189bf964b..0bf2a8f82 100644 --- a/src/storm/settings/modules/RegionSettings.cpp +++ b/src/storm/settings/modules/RegionSettings.cpp @@ -22,21 +22,21 @@ namespace storm { RegionSettings::RegionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the regions.") - .addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, regionsOptionName, true, "Specifies the regions via command line. Format: '0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9'") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build()); std::vector approxModes = {"off", "testfirst", "guessallsat", "guessallviolated"}; this->addOption(storm::settings::OptionBuilder(moduleName, approxmodeOptionName, true, "Sets whether approximation should be done and whether lower or upper bounds are computed first.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, testfirst (default), guessallsat, guessallviolated). E.g. guessallsat will first try to prove ALLSAT") - .addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(approxModes)).setDefaultValueString("testfirst").build()).build()); + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(approxModes)).setDefaultValueString("testfirst").build()).build()); std::vector sampleModes = {"off", "instantiate", "evaluate"}; this->addOption(storm::settings::OptionBuilder(moduleName, samplemodeOptionName, true, "Sets whether sampling should be done and whether to instantiate a model or compute+evaluate a function.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, instantiate (default), evaluate)") - .addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(sampleModes)).setDefaultValueString("instantiate").build()).build()); + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(sampleModes)).setDefaultValueString("instantiate").build()).build()); std::vector smtModes = {"off", "function", "model"}; this->addOption(storm::settings::OptionBuilder(moduleName, smtmodeOptionName, true, "Sets whether SMT solving should be done and whether to encode it via a function or the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function (default), model)") - .addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtModes)).setDefaultValueString("off").build()).build()); + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtModes)).setDefaultValueString("off").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, refinementOptionName, true, "Sets whether refinement (iteratively split regions) should be done. Only works if exactly one region (the parameter spaces) is specified.") .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Number between zero and one. Sets the fraction of undiscovered area at which refinement stops.").build()).build()); } diff --git a/src/storm/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp b/src/storm/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp index 9788927b7..ead40d320 100644 --- a/src/storm/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp +++ b/src/storm/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp @@ -23,7 +23,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build()); }