Browse Source

Added a set() Method to the Settings.h for the Tests

Moved all standard options into a helper class/compilation unit as to reuse it in the Tests
Moved the MaxIteration set call in the tests


Former-commit-id: f436511107
tempestpy_adaptions
PBerger 11 years ago
parent
commit
938959de56
  1. 10
      src/settings/Settings.h
  2. 2
      src/solver/GmmxxLinearEquationSolver.cpp
  3. 27
      src/storm.cpp
  4. 25
      src/utility/StormOptions.cpp
  5. 31
      src/utility/StormOptions.h
  6. 2
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  7. 2
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  8. 5
      test/functional/storm-functional-tests.cpp
  9. 2
      test/performance/graph/GraphTest.cpp
  10. 1
      test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
  11. 2
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  12. 7
      test/performance/storm-performance-tests.cpp

10
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

2
src/solver/GmmxxLinearEquationSolver.cpp

@ -3,7 +3,7 @@
#include <vector>
#include <string>
bool optionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool {
bool GmmxxLinearEquationSolverOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool {
std::vector<std::string> methods;
methods.push_back("bicgstab");

27
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<std::string> 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;
}

25
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<std::string> 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;
});

31
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_

2
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) {

2
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"

5
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[]) {

2
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"

1
test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

@ -110,7 +110,6 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
s->set<unsigned>("maxiter", 20000);
storm::parser::AutoParser<double> 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", "");

2
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<unsigned>("maxiter", 20000);
// This is done in the main cpp unit
storm::parser::AutoParser<double> 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", "");

7
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[]) {

Loading…
Cancel
Save