sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed some more places in the code to use the new option system. 

Former-commit-id: 15ff64f1dc
tempestpy_adaptions
dehnert 10 years ago
parent
685d9274eb
commit
5ecc96fa3a
7 changed files with 40 additions and 37 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  2. 6
      src/settings/modules/CounterexampleGeneratorSettings.cpp
  3. 8
      src/settings/modules/CounterexampleGeneratorSettings.h
  4. 10
      src/settings/modules/GeneralSettings.cpp
  5. 9
      src/settings/modules/GeneralSettings.h
  6. 16
      src/solver/GurobiLpSolver.cpp
  7. 24
      test/functional/solver/GurobiLpSolverTest.cpp

4
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -1759,7 +1759,7 @@ namespace storm {
// Compute and emit the time measurements if the corresponding flag was set.
totalTime = std::chrono::high_resolution_clock::now() - totalClock;
if (storm::settings::Settings::getInstance()->isSet("stats")) {
if (storm::settings::generalSettings().isShowStatisticsSet()) {
std::cout << std::endl;
std::cout << "Time breakdown:" << std::endl;
std::cout << " * time for setup: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalSetupTime).count() << "ms" << std::endl;
@ -1824,7 +1824,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::Settings::getInstance()->isSet("encreach"));
auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

6
src/settings/modules/CounterexampleGeneratorSettings.cpp
View File

@ -10,14 +10,12 @@ namespace storm {
const std::string CounterexampleGeneratorSettings::minimalCommandSetOptionName = "mincmd";
const std::string CounterexampleGeneratorSettings::encodeReachabilityOptionName = "encreach";
const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts";
const std::string CounterexampleGeneratorSettings::statisticsOptionName = "stats";
CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, 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("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.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());
this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics for counterexample generation.").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());
}
@ -46,10 +44,6 @@ namespace storm {
return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
}
bool CounterexampleGeneratorSettings::isShowStatisticsSet() const {
return this->getOption(statisticsOptionName).getHasOptionBeenSet();
}
} // namespace modules
} // namespace settings
} // namespace storm

8
src/settings/modules/CounterexampleGeneratorSettings.h
View File

@ -66,13 +66,6 @@ namespace storm {
*/
bool isUseSchedulerCutsSet() const;
/*!
* Retrieves whether statistics are to be shown for counterexample generation.
*
* @return True iff statistics are to be shown for counterexample generation.
*/
bool isShowStatisticsSet() const;
// The name of the module.
static const std::string moduleName;
@ -81,7 +74,6 @@ namespace storm {
static const std::string minimalCommandSetOptionName;
static const std::string encodeReachabilityOptionName;
static const std::string schedulerCutsOptionName;
static const std::string statisticsOptionName;
};
} // namespace modules

10
src/settings/modules/GeneralSettings.cpp
View File

@ -35,7 +35,9 @@ namespace storm {
const std::string GeneralSettings::lpSolverOptionName = "lpsolver";
const std::string GeneralSettings::constantsOptionName = "constants";
const std::string GeneralSettings::constantsOptionShortName = "const";
const std::string GeneralSettings::statisticsOptionName = "statistics";
const std::string GeneralSettings::statisticsOptionShortName = "stats";
GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
@ -77,6 +79,8 @@ namespace storm {
.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());
this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").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, statisticsOptionName, true, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
}
bool GeneralSettings::isHelpSet() const {
@ -224,6 +228,10 @@ namespace storm {
return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString();
}
bool GeneralSettings::isShowStatisticsSet() const {
return this->getOption(statisticsOptionName).getHasOptionBeenSet();
}
} // namespace modules
} // namespace settings
} // namespace storm

9
src/settings/modules/GeneralSettings.h
View File

@ -264,6 +264,13 @@ namespace storm {
* @return The string that defines the constants of a symbolic model.
*/
std::string getConstantDefinitionString() const;
/*!
* Retrieves whether statistics are to be shown for counterexample generation.
*
* @return True iff statistics are to be shown for counterexample generation.
*/
bool isShowStatisticsSet() const;
// The name of the module.
static const std::string moduleName;
@ -297,6 +304,8 @@ namespace storm {
static const std::string lpSolverOptionName;
static const std::string constantsOptionName;
static const std::string constantsOptionShortName;
static const std::string statisticsOptionName;
static const std::string statisticsOptionShortName;
};
} // namespace modules

16
src/solver/GurobiLpSolver.cpp
View File

@ -54,15 +54,15 @@ namespace storm {
int error = 0;
// Enable the following line to only print the output of Gurobi if the debug flag is set.
error = GRBsetintparam(env, "OutputFlag", storm::settings::Settings::getInstance()->isSet("debug") || storm::settings::Settings::getInstance()->isSet("gurobioutput") ? 1 : 0);
error = GRBsetintparam(env, "OutputFlag", storm::settings::debugSettings().isDebugSet() || storm::settings::gurobiSettings().isOutputSet() ? 1 : 0);
LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// Enable the following line to restrict Gurobi to one thread only.
error = GRBsetintparam(env, "Threads", storm::settings::Settings::getInstance()->getOptionByLongName("gurobithreads").getArgument(0).getValueAsUnsignedInteger());
error = GRBsetintparam(env, "Threads", storm::settings::gurobiSettings().getNumberOfThreads());
LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ").");
// Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option.
error = GRBsetdblparam(env, "IntFeasTol", storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble());
error = GRBsetdblparam(env, "IntFeasTol", storm::settings::gurobiSettings().getIntegerTolerance());
LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ").");
}
@ -155,13 +155,13 @@ namespace storm {
int error = 0;
switch (constraint.getOperator()) {
case storm::expressions::OperatorType::Less:
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.second - storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble(), name == "" ? nullptr : name.c_str());
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.second - storm::settings::gurobiSettings().getIntegerTolerance(), name == "" ? nullptr : name.c_str());
break;
case storm::expressions::OperatorType::LessOrEqual:
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_LESS_EQUAL, rightCoefficients.second, name == "" ? nullptr : name.c_str());
break;
case storm::expressions::OperatorType::Greater:
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.second + storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble(), name == "" ? nullptr : name.c_str());
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.second + storm::settings::gurobiSettings().getIntegerTolerance(), name == "" ? nullptr : name.c_str());
break;
case storm::expressions::OperatorType::GreaterOrEqual:
error = GRBaddconstr(model, variables.size(), variables.data(), coefficients.data(), GRB_GREATER_EQUAL, rightCoefficients.second, name == "" ? nullptr : name.c_str());
@ -288,7 +288,7 @@ namespace storm {
double value = 0;
int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value);
LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
return static_cast<int_fast64_t>(value);
}
@ -308,9 +308,9 @@ namespace storm {
LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ").");
if (value > 0.5) {
LOG_THROW(std::abs(static_cast<int>(value) - 1) <= storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
LOG_THROW(std::abs(static_cast<int>(value) - 1) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
} else {
LOG_THROW(value <= storm::settings::Settings::getInstance()->getOptionByLongName("gurobiinttol").getArgument(0).getValueAsDouble(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
LOG_THROW(value <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ").");
}
return static_cast<bool>(value);

24
test/functional/solver/GurobiLpSolverTest.cpp
View File

@ -25,16 +25,16 @@ TEST(GurobiLpSolver, LPOptimizeMax) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue("x"));
ASSERT_LT(std::abs(xValue - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue("y"));
ASSERT_LT(std::abs(yValue - 6.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(yValue - 6.5), storm::settings::generalSettings().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 2.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 2.75), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::generalSettings().getPrecision());
}
TEST(GurobiLpSolver, LPOptimizeMin) {
@ -55,16 +55,16 @@ TEST(GurobiLpSolver, LPOptimizeMin) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue("x"));
ASSERT_LT(std::abs(xValue - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue("y"));
ASSERT_LT(std::abs(yValue - 0), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(yValue - 0), storm::settings::generalSettings().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 5.7), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 5.7), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::generalSettings().getPrecision());
}
TEST(GurobiLpSolver, MILPOptimizeMax) {
@ -91,10 +91,10 @@ TEST(GurobiLpSolver, MILPOptimizeMax) {
ASSERT_EQ(6, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 3), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 3), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::generalSettings().getPrecision());
}
TEST(GurobiLpSolver, MILPOptimizeMin) {
@ -121,10 +121,10 @@ TEST(GurobiLpSolver, MILPOptimizeMin) {
ASSERT_EQ(0, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 5), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::generalSettings().getPrecision());
}
TEST(GurobiLpSolver, LPInfeasible) {

Write Preview
Loading…
Cancel
Save