diff --git a/src/storm.cpp b/src/storm.cpp index e7f7c6323..4720e7016 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -110,10 +110,6 @@ bool parseOptions(const int argc, const char* argv[]) { std::cout << storm::settings::help; return false; } - if (s->isSet("test-prctl")) { - storm::parser::PrctlParser parser(s->getString("test-prctl").c_str()); - return false; - } if (s->isSet("verbose")) { logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); @@ -210,7 +206,7 @@ void checkMdp(std::shared_ptr> mdp) { } if(s->isSet("csl")) { - LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); + LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on MDPs."); } } @@ -238,37 +234,6 @@ void checkDtmc(std::shared_ptr> dtmc) { } } -/*! - * Simple testing procedure. - */ -void check_main() { - storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew")); - - LOG4CPLUS_DEBUG(logger, s->getString("matrixlib")); - - - switch (parser.getType()) { - case storm::models::DTMC: - LOG4CPLUS_INFO(logger, "Model was detected as DTMC"); - checkDtmc(parser.getModel>()); - break; - case storm::models::MDP: - LOG4CPLUS_INFO(logger, "Model was detected as MDP"); - checkMdp(parser.getModel>()); - break; - case storm::models::CTMC: - case storm::models::CTMDP: - // Continuous time model checking is not implemented yet - LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm."); - break; - case storm::models::Unknown: - default: - LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); - break; - } -} - /*! * Main entry point. */ @@ -279,15 +244,46 @@ int main(const int argc, const char* argv[]) { printHeader(argc, argv); initializeLogger(); - if (!parseOptions(argc, argv)) { - return 0; - } + setUp(); try { LOG4CPLUS_INFO(logger, "StoRM was invoked."); - check_main(); + // Parse options + if (!parseOptions(argc, argv)) { + // If false is returned, the program execution is stopped here + // E.g. if the user asked to see the help text + return 0; + } + + // Now, the settings are receivd and the model is parsed. + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew")); + + LOG4CPLUS_DEBUG(logger, s->getString("matrixlib")); + + + // Depending on the model type, the respective model checking procedure is chosen. + switch (parser.getType()) { + case storm::models::DTMC: + LOG4CPLUS_INFO(logger, "Model was detected as DTMC"); + checkDtmc(parser.getModel>()); + break; + case storm::models::MDP: + LOG4CPLUS_INFO(logger, "Model was detected as MDP"); + checkMdp(parser.getModel>()); + break; + case storm::models::CTMC: + case storm::models::CTMDP: + // Continuous time model checking is not implemented yet + LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm."); + break; + case storm::models::Unknown: + default: + LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); + break; + } cleanUp(); diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 9a9ab1120..9c2688f58 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -134,7 +134,6 @@ void Settings::initDescriptions() { ("debug", "be very verbose, intended for debugging") ("logfile,l", bpo::value(), "name of the log file") ("configfile,c", bpo::value(), "name of config file") - ("test-prctl", bpo::value(), "name of prctl file") ("trafile", bpo::value()->required(), "name of the .tra file") ("labfile", bpo::value()->required(), "name of the .lab file") ("prctl", bpo::value(), "text file containing prctl formulas")