Browse Source

removed obsolete 'inplace' setting for multiplier

tempestpy_adaptions
TimQu 7 years ago
parent
commit
f5511f4213
  1. 2
      src/storm/settings/modules/MultiplierSettings.cpp

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

@ -15,7 +15,7 @@ namespace storm {
const std::string MultiplierSettings::multiplierTypeOptionName = "type";
MultiplierSettings::MultiplierSettings() : ModuleSettings(moduleName) {
std::vector<std::string> multiplierTypes = {"native", "inplace", "gmmxx"};
std::vector<std::string> multiplierTypes = {"native", "gmmxx"};
this->addOption(storm::settings::OptionBuilder(moduleName, multiplierTypeOptionName, true, "Sets which type of multiplier is preferred.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplier.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplierTypes)).setDefaultValueString("gmmxx").build()).build());

Loading…
Cancel
Save