diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index bac940957..5b3404deb 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -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(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(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index cf66717c9..17196a4bd 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -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 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 \ No newline at end of file diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h index 0cee9ff5b..e6d2b6f7e 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/settings/modules/CounterexampleGeneratorSettings.h @@ -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 diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 3446d16c4..822fa73d6 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -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 \ No newline at end of file diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 472668188..460e2cdd4 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -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 diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index 139bda5fe..519062b28 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -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(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(value) - value) <= storm::settings::gurobiSettings().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); return static_cast(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(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(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(value); diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index 88c8929c0..e71ad3711 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -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) {