Browse Source

reworked argument validators for settings

main
dehnert 8 years ago
parent
commit
49597fca86
  1. 10
      src/storm-dft/settings/modules/DFTSettings.cpp
  2. 9
      src/storm/abstraction/MenuGameRefiner.cpp
  3. 6
      src/storm/abstraction/MenuGameRefiner.h
  4. 6
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  5. 14
      src/storm/settings/Argument.cpp
  6. 34
      src/storm/settings/Argument.h
  7. 128
      src/storm/settings/ArgumentBuilder.h
  8. 186
      src/storm/settings/ArgumentValidators.cpp
  9. 326
      src/storm/settings/ArgumentValidators.h
  10. 123
      src/storm/settings/modules/AbstractionSettings.cpp
  11. 79
      src/storm/settings/modules/AbstractionSettings.h
  12. 2
      src/storm/settings/modules/BisimulationSettings.cpp
  13. 13
      src/storm/settings/modules/CoreSettings.cpp
  14. 2
      src/storm/settings/modules/CounterexampleGeneratorSettings.cpp
  15. 7
      src/storm/settings/modules/CuddSettings.cpp
  16. 9
      src/storm/settings/modules/EigenEquationSolverSettings.cpp
  17. 6
      src/storm/settings/modules/EliminationSettings.cpp
  18. 9
      src/storm/settings/modules/ExplorationSettings.cpp
  19. 4
      src/storm/settings/modules/GSPNSettings.cpp
  20. 5
      src/storm/settings/modules/GeneralSettings.cpp
  21. 2
      src/storm/settings/modules/GlpkSettings.cpp
  22. 9
      src/storm/settings/modules/GmmxxEquationSolverSettings.cpp
  23. 2
      src/storm/settings/modules/GurobiSettings.cpp
  24. 19
      src/storm/settings/modules/IOSettings.cpp
  25. 2
      src/storm/settings/modules/JaniExportSettings.cpp
  26. 4
      src/storm/settings/modules/MinMaxEquationSolverSettings.cpp
  27. 13
      src/storm/settings/modules/MultiObjectiveSettings.cpp
  28. 9
      src/storm/settings/modules/NativeEquationSolverSettings.cpp
  29. 2
      src/storm/settings/modules/PGCLSettings.cpp
  30. 2
      src/storm/settings/modules/ParametricSettings.cpp
  31. 8
      src/storm/settings/modules/RegionSettings.cpp
  32. 2
      src/storm/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp

10
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

9
src/storm/abstraction/MenuGameRefiner.cpp

@ -57,7 +57,11 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseInterpolationSet()), splitAll(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitAllSet()), splitPredicates(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()), splitGuards(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitGuardsSet()), splitInitialGuards(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitInitialGuardsSet()), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) {
MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseInterpolationSet()), splitAll(false), splitPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) {
AbstractionSettings::SplitMode splitMode = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSplitMode();
splitAll = splitMode == AbstractionSettings::SplitMode::All;
splitPredicates = splitMode == AbstractionSettings::SplitMode::NonGuard;
if (storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
std::vector<storm::expressions::Expression> guards;
@ -646,8 +650,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::vector<storm::expressions::Expression> MenuGameRefiner<Type, ValueType>::preprocessPredicates(std::vector<storm::expressions::Expression> 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;

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

6
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@ -63,9 +63,9 @@ namespace storm {
preprocessedModel = model.asJaniModel().flattenComposition();
}
bool reuseAll = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseAllResultsSet();
reuseQualitativeResults = reuseAll || storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseQualitativeResultsSet();
reuseQuantitativeResults = reuseAll || storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseQuantitativeResultsSet();
storm::settings::modules::AbstractionSettings::ReuseMode reuseMode = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().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<storm::dd::DdType Type, typename ModelType>

14
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<typename T>
Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) {
// Intentionally left empty.
}
template<typename T>
Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
Argument<T>::Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
this->setDefaultValue(defaultValue);
}
@ -51,8 +51,6 @@ namespace storm {
return this->argumentType;
}
template<typename T>
T const& Argument<T>::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<typename T>
bool Argument<T>::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;
}

34
src/storm/settings/Argument.h

@ -19,40 +19,38 @@
namespace storm {
namespace settings {
namespace settings {
template <typename ValueType>
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<typename T>
class Argument : public ArgumentBase {
public:
// Introduce shortcuts for validation functions.
typedef std::function<bool (T const&)> userValidationFunction_t;
template<typename T>
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<userValidationFunction_t> const& validationFunctions);
Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> 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<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue);
Argument(std::string const& name, std::string const& description, std::vector<std::shared_ptr<ArgumentValidator<T>>> 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<userValidationFunction_t> validationFunctions;
std::vector<std::shared_ptr<ArgumentValidator<T>>> 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.

128
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<ArgumentValidator< funcType >>&& 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<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->userValidationFunctions_String, this->isOptional, this->defaultValue_String));
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->validators_String, this->isOptional, this->defaultValue_String));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->userValidationFunctions_String));
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->validators_String));
}
break;
}
case ArgumentType::Integer:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->userValidationFunctions_Integer));
}
break;
case ArgumentType::UnsignedInteger:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->userValidationFunctions_UnsignedInteger));
}
break;
case ArgumentType::Double:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->userValidationFunctions_Double, this->isOptional, this->defaultValue_Double));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->userValidationFunctions_Double));
}
break;
case ArgumentType::Boolean:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->userValidationFunctions_Boolean));
}
break;
case ArgumentType::Integer:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->validators_Integer, this->isOptional, this->defaultValue_Integer));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->validators_Integer));
}
break;
case ArgumentType::UnsignedInteger:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->validators_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->validators_UnsignedInteger));
}
break;
case ArgumentType::Double:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->validators_Double, this->isOptional, this->defaultValue_Double));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->validators_Double));
}
break;
case ArgumentType::Boolean:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->validators_Boolean, this->isOptional, this->defaultValue_Boolean));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<bool>(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<storm::settings::Argument<std::string>::userValidationFunction_t> userValidationFunctions_String;
std::vector<storm::settings::Argument<int_fast64_t>::userValidationFunction_t> userValidationFunctions_Integer;
std::vector<storm::settings::Argument<uint_fast64_t>::userValidationFunction_t> userValidationFunctions_UnsignedInteger;
std::vector<storm::settings::Argument<double>::userValidationFunction_t> userValidationFunctions_Double;
std::vector<storm::settings::Argument<bool>::userValidationFunction_t> userValidationFunctions_Boolean;
std::vector<std::shared_ptr<ArgumentValidator<std::string>>> validators_String;
std::vector<std::shared_ptr<ArgumentValidator<int_fast64_t>>> validators_Integer;
std::vector<std::shared_ptr<ArgumentValidator<uint_fast64_t>>> validators_UnsignedInteger;
std::vector<std::shared_ptr<ArgumentValidator<double>>> validators_Double;
std::vector<std::shared_ptr<ArgumentValidator<bool>>> validators_Boolean;
};
}
}

186
src/storm/settings/ArgumentValidators.cpp

@ -0,0 +1,186 @@
#include "storm/settings/ArgumentValidators.h"
#include <boost/algorithm/string/join.hpp>
#include <sys/stat.h>
#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 <typename ValueType>
RangeArgumentValidator<ValueType>::RangeArgumentValidator(boost::optional<ValueType> const& lower, boost::optional<ValueType> const& upper, bool lowerIncluded, bool upperIncluded) : lower(lower), upper(upper), lowerIncluded(lowerIncluded), upperIncluded(upperIncluded) {
// Intentionally left empty.
}
template <typename ValueType>
bool RangeArgumentValidator<ValueType>::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 <typename ValueType>
std::string RangeArgumentValidator<ValueType>::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<std::string> 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<ArgumentValidator<int64_t>> ArgumentValidatorFactory::createIntegerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound) {
return createRangeValidatorExcluding<int64_t>(lowerBound, upperBound);
}
std::shared_ptr<ArgumentValidator<uint64_t>> ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound) {
return createRangeValidatorExcluding<uint64_t>(lowerBound, upperBound);
}
std::shared_ptr<ArgumentValidator<double>> ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(double lowerBound, double upperBound) {
return createRangeValidatorExcluding<double>(lowerBound, upperBound);
}
std::shared_ptr<ArgumentValidator<int64_t>> ArgumentValidatorFactory::createIntegerGreaterValidator(int_fast64_t lowerBound) {
return createGreaterValidator<int64_t>(lowerBound, false);
}
std::shared_ptr<ArgumentValidator<uint64_t>> ArgumentValidatorFactory::createUnsignedGreaterValidator(uint64_t lowerBound) {
return createGreaterValidator<uint64_t>(lowerBound, false);
}
std::shared_ptr<ArgumentValidator<double>> ArgumentValidatorFactory::createDoubleGreaterValidator(double lowerBound) {
return createGreaterValidator<double>(lowerBound, false);
}
std::shared_ptr<ArgumentValidator<int64_t>> ArgumentValidatorFactory::createIntegerGreaterEqualValidator(int_fast64_t lowerBound) {
return createGreaterValidator<int64_t>(lowerBound, true);
}
std::shared_ptr<ArgumentValidator<uint64_t>> ArgumentValidatorFactory::createUnsignedGreaterEqualValidator(uint64_t lowerBound) {
return createGreaterValidator<uint64_t>(lowerBound, true);
}
std::shared_ptr<ArgumentValidator<double>> ArgumentValidatorFactory::createDoubleGreaterEqualValidator(double lowerBound) {
return createGreaterValidator<double>(lowerBound, true);
}
std::shared_ptr<ArgumentValidator<std::string>> ArgumentValidatorFactory::createExistingFileValidator() {
return std::make_unique<FileValidator>(FileValidator::Mode::Exists);
}
std::shared_ptr<ArgumentValidator<std::string>> ArgumentValidatorFactory::createWritableFileValidator() {
return std::make_unique<FileValidator>(FileValidator::Mode::Writable);
}
std::shared_ptr<ArgumentValidator<std::string>> ArgumentValidatorFactory::createMultipleChoiceValidator(std::vector<std::string> const& choices) {
return std::make_unique<MultipleChoiceValidator>(choices);
}
template <typename ValueType>
std::shared_ptr<ArgumentValidator<ValueType>> ArgumentValidatorFactory::createRangeValidatorExcluding(ValueType lowerBound, ValueType upperBound) {
return std::make_unique<RangeArgumentValidator<ValueType>>(lowerBound, upperBound, false, false);
}
template <typename ValueType>
std::shared_ptr<ArgumentValidator<ValueType>> ArgumentValidatorFactory::createGreaterValidator(ValueType lowerBound, bool equalAllowed) {
return std::make_unique<RangeArgumentValidator<ValueType>>(lowerBound, boost::none, equalAllowed, false);
}
}
}

326
src/storm/settings/ArgumentValidators.h

@ -1,275 +1,95 @@
#ifndef STORM_SETTINGS_ARGUMENTVALIDATORS_H_
#define STORM_SETTINGS_ARGUMENTVALIDATORS_H_
#pragma once
#include <iostream>
#include <ostream>
#include <fstream>
#include <list>
#include <utility>
#include <functional>
#include <vector>
#include <memory>
#include <vector>
#include <string>
#include <stdio.h>
#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 <sys/stat.h>
#include <boost/optional.hpp>
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<bool (int_fast64_t const&)> integerRangeValidatorIncluding(int_fast64_t lowerBound, int_fast64_t upperBound) {
return rangeValidatorIncluding<int_fast64_t>(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<bool (int_fast64_t const&)> integerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound) {
return rangeValidatorExcluding<int_fast64_t>(lowerBound, upperBound);
}
namespace settings {
template <typename ValueType>
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<bool (int_fast64_t const&)> integerGreaterValidatorIncluding(int_fast64_t threshold) {
return greaterValidatorIncluding<int_fast64_t>(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<bool (int_fast64_t const&)> integerGreaterValidatorExcluding(int_fast64_t threshold) {
return greaterValidatorExcluding<int_fast64_t>(threshold);
}
* Retrieves a string representation of the valid values.
*/
virtual std::string toString() const = 0;
};
template <typename ValueType>
class RangeArgumentValidator : public ArgumentValidator<ValueType> {
public:
RangeArgumentValidator(boost::optional<ValueType> const& lower, boost::optional<ValueType> 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<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorIncluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) {
return rangeValidatorIncluding<uint_fast64_t>(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<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorExcluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) {
return rangeValidatorExcluding<uint_fast64_t>(lowerBound, upperBound);
}
private:
boost::optional<ValueType> lower;
boost::optional<ValueType> upper;
bool lowerIncluded;
bool upperIncluded;
};
class FileValidator : public ArgumentValidator<std::string> {
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<bool (uint_fast64_t const&)> unsignedIntegerGreaterValidatorIncluding(uint_fast64_t threshold) {
return greaterValidatorIncluding<uint_fast64_t>(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<bool (uint_fast64_t const&)> unsignedIntegerGreaterValidatorExcluding(uint_fast64_t threshold) {
return greaterValidatorExcluding<uint_fast64_t>(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<bool (double const&)> doubleRangeValidatorIncluding(double lowerBound, double upperBound) {
return rangeValidatorIncluding<double>(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<bool (double const&)> doubleRangeValidatorExcluding(double lowerBound, double upperBound) {
return rangeValidatorExcluding<double>(lowerBound, upperBound);
}
private:
Mode mode;
};
class MultipleChoiceValidator : public ArgumentValidator<std::string> {
public:
MultipleChoiceValidator(std::vector<std::string> 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<bool (double const&)> doubleGreaterValidatorIncluding(double threshold) {
return greaterValidatorIncluding<double>(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<bool (double const&)> doubleGreaterValidatorExcluding(double threshold) {
return greaterValidatorExcluding<double>(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<bool (std::string const&)> 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<bool (std::string const&)> 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<bool (std::string const&)> stringInListValidator(std::vector<std::string> 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<std::string> legalValues;
};
class ArgumentValidatorFactory {
public:
static std::shared_ptr<ArgumentValidator<int64_t>> createIntegerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound);
static std::shared_ptr<ArgumentValidator<uint64_t>> createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound);
static std::shared_ptr<ArgumentValidator<double>> 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<typename T>
static std::function<bool (T const&)> 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<ArgumentValidator<int64_t>> createIntegerGreaterValidator(int_fast64_t lowerBound);
static std::shared_ptr<ArgumentValidator<uint64_t>> createUnsignedGreaterValidator(uint64_t lowerBound);
static std::shared_ptr<ArgumentValidator<double>> 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<typename T>
static std::function<bool (T const&)> 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<ArgumentValidator<int64_t>> createIntegerGreaterEqualValidator(int_fast64_t lowerBound);
static std::shared_ptr<ArgumentValidator<uint64_t>> createUnsignedGreaterEqualValidator(uint64_t lowerBound);
static std::shared_ptr<ArgumentValidator<double>> 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<typename T>
static std::function<bool (T const&)> 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<ArgumentValidator<std::string>> createExistingFileValidator();
static std::shared_ptr<ArgumentValidator<std::string>> 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<typename T>
static std::function<bool (T const&)> 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<ArgumentValidator<std::string>> createMultipleChoiceValidator(std::vector<std::string> const& choices);
private:
template <typename ValueType>
static std::shared_ptr<ArgumentValidator<ValueType>> createRangeValidatorExcluding(ValueType lowerBound, ValueType upperBound);
template <typename ValueType>
static std::shared_ptr<ArgumentValidator<ValueType>> createGreaterValidator(ValueType lowerBound, bool equalAllowed);
};
}
}
#endif // STORM_SETTINGS_ARGUMENTVALIDATORS_H_

123
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<std::string> 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<std::string> 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<std::string> 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<std::string> 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();
}
}
}
}

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

2
src/storm/settings/modules/BisimulationSettings.cpp

@ -15,7 +15,7 @@ namespace storm {
BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) {
std::vector<std::string> 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 {

13
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<std::string> 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<std::string> 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<std::string> 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<std::string> 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<std::string> 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());
}

2
src/storm/settings/modules/CounterexampleGeneratorSettings.cpp

@ -20,7 +20,7 @@ namespace storm {
CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) {
std::vector<std::string> 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());
}

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

9
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<std::string> 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<std::string> 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 {

6
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<std::string> 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<std::string> 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.")

9
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<std::string> 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<std::string> 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 {

4
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 {

5
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 {

2
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 {

9
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<std::string> 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<std::string> 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());
}

2
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 {

19
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<std::string> 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)

2
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 {

4
src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@ -21,11 +21,11 @@ namespace storm {
MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) {
std::vector<std::string> 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());
}

13
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<storm::settings::ArgumentValidator<std::string>> 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

9
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<std::string> 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());
}

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

2
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 {

8
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<std::string> 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<std::string> 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<std::string> 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());
}

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

|||||||
100:0
Loading…
Cancel
Save