// We don't need to check whether this option exists or not, because this is already checked when
// parsing the configuration file.
// Now go through all the matching options and set them according to the values.
for(autooption:options->second){
if(option->getHasOptionBeenSet()){
// If the option was already set from the command line, we issue a warning and ignore the
// settings from the configuration file.
STORM_LOG_WARN("The option '"<<option->getLongName()<<"' of module '"<<option->getModuleName()<<"' has been set in the configuration file '"<<configFilename<<"', but was overwritten on the command line."<<std::endl);
}else{
// If, however, the option has not been set yet, we try to assign values ot its arguments
STORM_LOG_THROW(moduleIterator!=moduleOptions.end(),storm::exceptions::IllegalFunctionCallException,"Cannot print help for unknown module '"<<moduleName<<"'.");
STORM_LOG_THROW(argumentCache.size()<=option->getArgumentCount(),storm::exceptions::OptionParserException,"Too many arguments for option '"<<optionName<<"'.");
// Now set the provided argument values one by one.
STORM_LOG_THROW(conversionOk,storm::exceptions::OptionParserException,"Conversion of value of argument '"<<argument.getName()<<"' to its type failed.");
}
// In case there are optional arguments that were not set, we set them to their default value.
// Iterate over all options and set the arguments.
for(auto&option:optionIterator->second){
option->setHasOptionBeenSet();
STORM_LOG_THROW(argumentCache.size()<=option->getArgumentCount(),storm::exceptions::OptionParserException,"Too many arguments for option '"<<optionName<<"'.");
// Now set the provided argument values one by one.
STORM_LOG_THROW(conversionOk,storm::exceptions::OptionParserException,"Conversion of value of argument '"<<argument.getName()<<"' to its type failed.");
}
// In case there are optional arguments that were not set, we set them to their default value.
// If the first character of the line is a "[", we expect the settings of a new module to start and
// the line to be of the shape [<module>].
if(line.at(0)=='['){
STORM_LOG_THROW(line.at(0)=='['&&line.find("]")==line.length()-1&&line.find("[",1)==line.npos,storm::exceptions::OptionParserException,"Illegal module name header in configuration file '"<<filename<<" in line "<<std::to_string(lineNumber)<<". Expected [<module>] where <module> is a placeholder for a known module.");
// Extract the module name and check whether it's a legal one.
STORM_LOG_THROW(moduleName!=""&&(moduleName=="global"||(this->modules.find(moduleName)!=this->modules.end())),storm::exceptions::OptionParserException,"Module header in configuration file '"<<filename<<" in line "<<std::to_string(lineNumber)<<" refers to unknown module '"<<moduleName<<".");
// If the module name is "global", we unset the currently active module and treat all options to follow as unprefixed.
if(moduleName=="global"){
globalScope=true;
}else{
activeModule=moduleName;
globalScope=false;
}
}else{
// In this case, we expect the line to be of the shape o or o=a b c, where o is an option and a, b
// and c are the values that are supposed to be assigned to the arguments of the option.
std::size_tassignmentSignIndex=line.find("=");
boolcontainsAssignment=false;
if(assignmentSignIndex!=line.npos){
containsAssignment=true;
}
std::stringoptionName;
if(containsAssignment){
optionName=line.substr(0,assignmentSignIndex);
}else{
optionName=line;
}
if(globalScope){
STORM_LOG_THROW(this->longNameToOptions.find(optionName)!=this->longNameToOptions.end(),storm::exceptions::OptionParserException,"Option assignment in configuration file '"<<filename<<" in line "<<lineNumber<<" refers to unknown option '"<<optionName<<"'.");
}else{
STORM_LOG_THROW(this->longNameToOptions.find(activeModule+":"+optionName)!=this->longNameToOptions.end(),storm::exceptions::OptionParserException,"Option assignment in configuration file '"<<filename<<" in line "<<lineNumber<<" refers to unknown option '"<<activeModule<<":"<<optionName<<"'.");
STORM_LOG_WARN_COND(result.find(fullOptionName)==result.end(),"Option '"<<fullOptionName<<"' is set in line "<<lineNumber<<" of configuration file "<<filename<<", but has been set before.");
// If the current line is an assignment, split the right-hand side of the assignment into parts
// If the input could not be matched, we have a parsing error.
STORM_LOG_THROW(hasMatch,storm::exceptions::OptionParserException,"Parsing error in configuration file '"<<filename<<"' in line "<<lineNumber<<". Unexpected input '"<<assignedValues<<"'.");
// Extract the matched argument and cut off the quotation marks if necessary.
this->addOption(storm::settings::OptionBuilder(moduleName,schedulerCutsOptionName,true,"Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
// Ensure that the model was given either symbolically or explicitly.
STORM_LOG_THROW(!isMinimalCommandSetGenerationSet()||storm::settings::generalSettings().isSymbolicSet(),storm::exceptions::InvalidSettingsException,"For the generation of a minimal command set, the model has to be specified symbolically.");
if(isMinimalCommandSetGenerationSet()){
STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet()||!isEncodeReachabilitySet(),"Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
STORM_LOG_WARN_COND(isUseMilpBasedMinimalCommandSetGenerationSet()||!isUseSchedulerCutsSet(),"Using scheduler cuts is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
// Ensure that the model was given either symbolically or explicitly.
STORM_LOG_THROW(!isSymbolicSet()||!isExplicitSet(),storm::exceptions::InvalidSettingsException,"The model may be either given in an explicit or a symbolic format, but not both.");
// Make sure that one "source" for properties is given.
STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver()==storm::settings::modules::GeneralSettings::LpSolver::glpk,"glpk is not selected as the used LP solver, so setting options for glpk has no effect.");
this->addOption(storm::settings::OptionBuilder(moduleName,absoluteOptionName,false,"Sets whether the relative or the absolute error is considered for detecting convergence.").build());
STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver()==storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx||!optionsSet,"gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
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());
STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver()==storm::settings::modules::GeneralSettings::LpSolver::Gurobi,"Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect.");
this->addOption(storm::settings::OptionBuilder(moduleName,absoluteOptionName,false,"Sets whether the relative or the absolute error is considered for detecting convergence.").build());
STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver()==storm::settings::modules::GeneralSettings::EquationSolver::Native||!optionSet,"Native is not selected as the equation solver, so setting options for native has no effect.");
STORM_LOG_THROW(model->getType()==storm::models::MDP,storm::exceptions::InvalidTypeException,"Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(),storm::exceptions::InvalidSettingsException,"Minimal command set generation is only available for symbolic models.");
sjunges
10 years ago