From 2a6228af718c6e8a03feec0cb9f743173483b395 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Dec 2012 22:25:23 +0100 Subject: [PATCH] Added some options to Gmmxx-Modelchecker. DO NOT PULL FOR THE TIME BEING AS THERE IS A PROBLEM WITH THE OPTIONS. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 50 +++++++++++++++++++ src/mrmc.cpp | 3 +- 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index d654bff81..ff332b566 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -13,6 +13,9 @@ #include "src/solver/GraphAnalyzer.h" #include "src/utility/vector.h" +#include "src/exceptions/InvalidSettings.h" +#include + #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -167,6 +170,53 @@ public: return result; } + + /*! + * Returns the name of this module. + * @return The name of this module. + */ + static std::string getModuleName() { + return "gmm++"; + } + + /*! + * Returns a trigger such that if the option "matrixlib" is set to "gmm++", this model checker + * is to be used. + * @return An option trigger for this module. + */ + static std::pair getOptionTrigger() { + return std::pair("matrixlib", "gmm++"); + } + + /*! + * Registers all options associated with the gmm++ matrix library. + */ + static void putOptions(boost::program_options::options_description* desc) { + desc->add_options()("lemethod", boost::program_options::value()->default_value("bicgstab")->notifier(&validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, gmres, qmr}."); + desc->add_options()("lemethod", boost::program_options::value()->default_value(10000), "Sets the maximal number of iterations used for linear equation solving."); + desc->add_options()("precond", boost::program_options::value()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioner used for linear equation solving. Must be in {ilu, diagonal, ildlt}."); + desc->add_options()("restart", boost::program_options::value()->default_value(40), "Sets the number of iterations after which gmres is restarted."); + } + + /*! + * Validates whether the given lemethod matches one of the available ones. + * Throws an exception of type InvalidSettings in case the selected method is illegal. + */ + static void validateLeMethod(const std::string& lemethod) { + if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0 && lemethod.compare("gmres") != 0) { + throw exceptions::InvalidSettings(); + } + } + + /*! + * Validates whether the given preconditioner matches one of the available ones. + * Throws an exception of type InvalidSettings in case the selected preconditioner is illegal. + */ + static void validatePreconditioner(const std::string& preconditioner) { + if (preconditioner.compare("ilu") != 0 && preconditioner.compare("diagonal") != 0 && preconditioner.compare("ildlt") != 0) { + throw exceptions::InvalidSettings(); + } + } }; } //namespace modelChecker diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 6f2caed40..063d2643c 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -62,7 +62,7 @@ void setUpConsoleLogging() { int main(const int argc, const char* argv[]) { setUpFileLogging(); - mrmc::settings::Settings* s = NULL; + mrmc::settings::Settings* s = nullptr; LOG4CPLUS_INFO(logger, "This is the Markov Reward Model Checker (MRMC) by i2 of RWTH Aachen University."); @@ -74,6 +74,7 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "MRMC command invoked " << commandStream.str()); try { + mrmc::settings::Settings::registerModule >(); s = mrmc::settings::newInstance(argc, argv, nullptr); } catch (mrmc::exceptions::InvalidSettings& e) { LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what());