diff --git a/src/settings/Settings.h b/src/settings/Settings.h index 50f2b72ba..c90183e20 100644 --- a/src/settings/Settings.h +++ b/src/settings/Settings.h @@ -125,6 +125,16 @@ namespace settings { return this->getByLongName(longName).getHasOptionBeenSet(); } + /*! + * Sets the Option with the specified longName + * This function requires the Option to have no arguments + * This is for TESTING only and should not be used outside of the testing code! + * @throws InvalidArgumentException + */ + void set(std::string const& longName) const { + return this->getByLongName(longName).setHasOptionBeenSet(); + } + /* * This generated a list of all registered options and their arguments together with descriptions and defaults. * @return A std::string containing the help text, delimited by \n diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index 15850860c..f9173d735 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -3,7 +3,7 @@ #include #include -bool optionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { +bool GmmxxLinearEquationSolverOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { std::vector methods; methods.push_back("bicgstab"); diff --git a/src/storm.cpp b/src/storm.cpp index d4564950b..f93ce240e 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -29,6 +29,7 @@ #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" #include "src/settings/Settings.h" +#include "src/utility/StormOptions.h" // Registers all standard options #include "src/utility/ErrorHandling.h" #include "src/formula/Prctl.h" @@ -90,28 +91,6 @@ void printUsage() { #endif } -bool registerStandardOptions(storm::settings::Settings* settings) { - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "help", "h", "Shows all available Options, Arguments and Descriptions").build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "verbose", "v", "Be verbose").build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "debug", "", "Be very verbose (intended for debugging)").build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts)").build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "logfile", "l", "If specified, the log output will also be written to this file").addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the File to write to").build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the File to read from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from Transition- and Labeling Files").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the File to read the transition system from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the File to read the labeling from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given PRISM File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prismFileName", "The path and name of the File to read the PRISM Model from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).setDefaultValueString("").setIsOptional(true).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).setDefaultValueString("").setIsOptional(true).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build()); - std::vector matrixLibrarys; - matrixLibrarys.push_back("gmm++"); - matrixLibrarys.push_back("native"); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Which matrix library is to be used in numerical solving").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "Name of a buildin Library").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibrarys)).setDefaultValueString("gmm++").build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "useHeurisiticPresolve", "", "Sets whether heuristic methods should be applied to get better initial values for value iteration").build()); -} - log4cplus::Logger logger; /*! @@ -163,12 +142,12 @@ void printHeader(const int argc, const char* argv[]) { * @return True iff the program should continue to run after parsing the options. */ bool parseOptions(const int argc, const char* argv[]) { - storm::settings::Settings* s = nullptr; + storm::settings::Settings* s = storm::settings::Settings::getInstance(); try { storm::settings::Settings::parse(argc, argv); } catch (storm::exceptions::OptionParserException& e) { std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; - std::cout << std::endl << storm::settings::Settings::getInstance()->getHelpText(); + std::cout << std::endl << s->getHelpText(); return false; } diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp new file mode 100644 index 000000000..bb9006c1c --- /dev/null +++ b/src/utility/StormOptions.cpp @@ -0,0 +1,25 @@ +#include "src/utility/StormOptions.h" + +bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* settings) -> bool { + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "help", "h", "Shows all available Options, Arguments and Descriptions").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "verbose", "v", "Be verbose").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "debug", "", "Be very verbose (intended for debugging)").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts)").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "logfile", "l", "If specified, the log output will also be written to this file").addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the File to write to").build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the File to read from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from Transition- and Labeling Files").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the File to read the transition system from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the File to read the labeling from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given PRISM File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prismFileName", "The path and name of the File to read the PRISM Model from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).setDefaultValueString("").setIsOptional(true).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).setDefaultValueString("").setIsOptional(true).build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build()); + std::vector matrixLibrarys; + matrixLibrarys.push_back("gmm++"); + matrixLibrarys.push_back("native"); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Which matrix library is to be used in numerical solving").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "Name of a buildin Library").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibrarys)).setDefaultValueString("gmm++").build()).build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "useHeurisiticPresolve", "", "Sets whether heuristic methods should be applied to get better initial values for value iteration").build()); + + return true; +}); \ No newline at end of file diff --git a/src/utility/StormOptions.h b/src/utility/StormOptions.h new file mode 100644 index 000000000..9a0b10780 --- /dev/null +++ b/src/utility/StormOptions.h @@ -0,0 +1,31 @@ +/* + * StormOptions.h + * + * All shared options are declared here, so that they can be reused in the Tests + * + * Created on: 07.09.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_UTILITY_STORMOPTIONS_H_ +#define STORM_UTILITY_STORMOPTIONS_H_ + +#include "src/settings/Settings.h" + + +namespace storm { + namespace utility { + + class StormOptions { + private: + StormOptions() {} + StormOptions(StormOptions& other) {} + ~StormOptions() {} + + static bool optionsRegistered; + }; + + } +} + +#endif // STORM_UTILITY_STORMOPTIONS_H_ \ No newline at end of file diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 7f0195095..2f076a940 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -3,7 +3,7 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "src/parser/AutoParser.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 68fb56738..237bb591c 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp index c826b04e9..3b76dde31 100644 --- a/test/functional/storm-functional-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -6,7 +6,8 @@ #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" +#include "src/utility/StormOptions.h" // Registers all standard options log4cplus::Logger logger; @@ -34,7 +35,7 @@ void setUpLogging() { */ void createEmptyOptions() { const char* newArgv[] = {"storm-performance-tests"}; - storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true); + storm::settings::Settings::parse(1, newArgv); } int main(int argc, char* argv[]) { diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 9ce96d1bc..bf62d4632 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "src/parser/AutoParser.h" #include "src/utility/graph.h" diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 72a2e5fdb..faabd6038 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -110,8 +110,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - s->set("maxiter", 20000); - + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); ASSERT_EQ(parser.getType(), storm::models::MDP); diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 84c3f3743..f451620ba 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -109,7 +109,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(SparseMdpPrctlModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); // Increase the maximal number of iterations, because the solver does not converge otherwise. - s->set("maxiter", 20000); + // This is done in the main cpp unit storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp index 0f22c1dc2..0c143061c 100644 --- a/test/performance/storm-performance-tests.cpp +++ b/test/performance/storm-performance-tests.cpp @@ -6,7 +6,8 @@ #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" +#include "src/utility/StormOptions.h" // Registers all standard options log4cplus::Logger logger; @@ -33,8 +34,8 @@ void setUpLogging() { * Creates an empty settings object as the standard instance of the Settings class. */ void createEmptyOptions() { - const char* newArgv[] = {"storm-performance-tests"}; - storm::settings::Settings* s = storm::settings::newInstance(1, newArgv, nullptr, true); + const char* newArgv[] = {"storm-performance-tests", "--maxIterations", "20000"}; + storm::settings::Settings::parse(3, newArgv); } int main(int argc, char* argv[]) {