diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/ProbabilisticNoBoundsOperator.h index b89080ca7..e1412c749 100644 --- a/src/formula/ProbabilisticNoBoundsOperator.h +++ b/src/formula/ProbabilisticNoBoundsOperator.h @@ -81,6 +81,21 @@ public: this->pathFormula = pathFormula; } + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker + * class. For other uses, the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the + * called object. + */ + virtual std::vector *check( + const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + return modelChecker.checkProbabilisticOperator(*this); + } + /*! * @returns a string representation of the formula */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 9556fd966..5c074d2af 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -32,6 +32,11 @@ class DtmcPrctlModelChecker; #include "src/storage/BitVector.h" #include +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + namespace mrmc { namespace modelChecker { @@ -53,8 +58,8 @@ public: * * @param model The dtmc model which is checked. */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc& model) { - this->model = &model; + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc& model) : model(model) { + } /*! @@ -70,15 +75,14 @@ public: * Destructor */ virtual ~DtmcPrctlModelChecker() { - //should not be deleted here, according to ticket #24 - //delete this->dtmc; + // Intentionally left empty. } /*! * @returns A reference to the dtmc of the model checker. */ mrmc::models::Dtmc& getModel() const { - return *(this->model); + return this->model; } /*! @@ -89,6 +93,39 @@ public: this->model = &model; } + /*! + * Checks the given state formula on the DTMC and prints the result (true/false) for all initial + * states. + * @param stateFormula The formula to be checked. + */ + void check(const mrmc::formula::PctlStateFormula& stateFormula) { + LOG4CPLUS_INFO(logger, "Model checking formula " << stateFormula.toString()); + mrmc::storage::BitVector* result = stateFormula.check(*this); + LOG4CPLUS_INFO(logger, "Result for initial states:"); + for (auto initialState : *this->getModel().getLabeledStates("init")) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); + } + delete result; + } + + /*! + * Checks the given probabilistic operator (with no bound) on the DTMC and prints the result + * (probability) for all initial states. + * @param probabilisticNoBoundsFormula The formula to be checked. + */ + void check(const mrmc::formula::ProbabilisticNoBoundsOperator& probabilisticNoBoundsFormula) { + LOG4CPLUS_INFO(logger, "Model checking formula " << probabilisticNoBoundsFormula.toString()); + std::cout << "Model checking formula: " << probabilisticNoBoundsFormula.toString() << std::endl; + std::vector* result = probabilisticNoBoundsFormula.check(*this); + LOG4CPLUS_INFO(logger, "Result for initial states:"); + std::cout << "Result for initial states:" << std::endl; + for (auto initialState : *this->getModel().getLabeledStates("init")) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); + std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; + } + delete result; + } + /*! * The check method for a state formula; Will infer the actual type of formula and delegate it * to the specialized method @@ -122,11 +159,11 @@ public: */ mrmc::storage::BitVector* checkAp(const mrmc::formula::Ap& formula) const { if (formula.getAp().compare("true") == 0) { - return new mrmc::storage::BitVector(model->getNumberOfStates(), 1); + return new mrmc::storage::BitVector(this->getModel().getNumberOfStates(), true); } else if (formula.getAp().compare("false") == 0) { - return new mrmc::storage::BitVector(model->getNumberOfStates()); + return new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); } - return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAp())); + return new mrmc::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); } /*! @@ -216,7 +253,7 @@ public: */ std::vector* checkProbabilisticOperator( const mrmc::formula::ProbabilisticNoBoundsOperator& formula) const { - return formula.getPathFormula().check(this); + return formula.getPathFormula().check(*this); } /*! @@ -255,7 +292,7 @@ public: virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const = 0; private: - mrmc::models::Dtmc* model; + mrmc::models::Dtmc& model; }; } //namespace modelChecker diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 5dde36fc4..d1fc59a9c 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -162,7 +162,7 @@ public: if (s->getString("lemethod").compare("bicgstab") == 0) { LOG4CPLUS_INFO(logger, "Using BiCGStab method."); - if (precond.compare("ilu")) { + if (precond == "ilu") { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); } else if (precond == "diagonal") { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); @@ -185,7 +185,7 @@ public: } */ } else if (s->getString("lemethod").compare("qmr") == 0) { LOG4CPLUS_INFO(logger, "Using QMR method."); - if (precond.compare("ilu")) { + if (precond == "ilu") { gmm::qmr(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); } else if (precond == "diagonal" == 0) { gmm::qmr(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 9bb62172a..f786b1982 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -41,43 +41,63 @@ log4cplus::Logger logger; /*! - * Initializes the logging framework. + * Initializes the logging framework and sets up logging to console. */ -void setUpFileLogging() { - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("mrmc.log")); - fileLogAppender->setName("mainFileAppender"); - fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L : %m%n"))); - logger = log4cplus::Logger::getInstance("mainLogger"); - logger.addAppender(fileLogAppender); -} - -void setUpConsoleLogging() { +void initializeLogger() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); consoleLogAppender->setName("mainConsoleAppender"); - consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L : %m%n"))); + consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); logger.addAppender(consoleLogAppender); } -int main(const int argc, const char* argv[]) { - setUpFileLogging(); +/*! + * Sets up the logging to file. + */ +void setUpFileLogging() { + mrmc::settings::Settings* s = mrmc::settings::instance(); + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getString("logfile"))); + fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); + logger.addAppender(fileLogAppender); +} - mrmc::settings::Settings* s = nullptr; - - LOG4CPLUS_INFO(logger, "This is the Markov Reward Model Checker (MRMC) by i2 of RWTH Aachen University."); +/*! + * Prints the header. + */ +void printHeader(const int argc, const char* argv[]) { + std::cout << "MRMC" << std::endl; + std::cout << "====" << std::endl << std::endl; - // "Compute" the command line argument string with which MRMC was invoked and log as diagnostic information. + std::cout << "Version: 1.0" << std::endl; + // "Compute" the command line argument string with which MRMC was invoked. std::stringstream commandStream; for (int i = 0; i < argc; ++i) { commandStream << argv[i] << " "; } - LOG4CPLUS_INFO(logger, "MRMC command invoked " << commandStream.str()); + std::cout << "Command line: " << commandStream.str() << std::endl << std::endl; +} + +/*! + * Prints the footer. + */ +void printFooter() { + std::cout << "Nothing more to do, exiting." << std::endl; +} +/*! + * Function that parses the command line options. + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ +bool parseOptions(const int argc, const char* argv[]) { + mrmc::settings::Settings* s = nullptr; try { - mrmc::settings::Settings::registerModule >(); + mrmc::settings::Settings::registerModule>(); s = mrmc::settings::newInstance(argc, argv, nullptr); } catch (mrmc::exceptions::InvalidSettingsException& e) { - LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what() << "."); - LOG4CPLUS_FATAL(logger, "Could not recover from settings error, terminating."); std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; std::cout << std::endl << mrmc::settings::help; delete s; @@ -87,31 +107,71 @@ int main(const int argc, const char* argv[]) { if (s->isSet("help")) { std::cout << mrmc::settings::help; delete s; - return 0; + return false; } if (s->isSet("test-prctl")) { mrmc::parser::PrctlParser parser(s->getString("test-prctl").c_str()); delete s; - return 0; + return false; } - if (s->isSet("verbose")) - { - setUpConsoleLogging(); + if (!s->isSet("verbose") && !s->isSet("logfile")) { + logger.setLogLevel(log4cplus::FATAL_LOG_LEVEL); + } else if (!s->isSet("verbose")) { + logger.removeAppender("mainConsoleAppender"); + setUpFileLogging(); + } else if (!s->isSet("logfile")) { + LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); + } else { + setUpFileLogging(); LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); } - mrmc::parser::TraParser traparser(s->getString("trafile").c_str()); + return true; +} + +/*! + * Function to perform some cleanup. + */ +void cleanUp() { + if (mrmc::settings::instance() != nullptr) { + delete mrmc::settings::instance(); + } +} + +/*! + * Simple testing procedure. + */ +void testChecking() { + mrmc::settings::Settings* s = mrmc::settings::instance(); + mrmc::parser::TraParser traparser(s->getString("trafile").c_str()); mrmc::parser::LabParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str()); mrmc::models::Dtmc dtmc(traparser.getMatrix(), labparser.getLabeling()); - dtmc.printModelInformationToStream(std::cout); - if (s != nullptr) { - delete s; + mrmc::formula::Ap* trueFormula = new mrmc::formula::Ap("true"); + mrmc::formula::Ap* observe0Greater1Formula = new mrmc::formula::Ap("observe0Greater1"); + mrmc::formula::Until* untilFormula = new mrmc::formula::Until(trueFormula, observe0Greater1Formula); + mrmc::formula::ProbabilisticNoBoundsOperator* probFormula = new mrmc::formula::ProbabilisticNoBoundsOperator(*untilFormula); + mrmc::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new mrmc::modelChecker::GmmxxDtmcPrctlModelChecker(dtmc); + mc->check(*probFormula); + + delete mc; + delete probFormula; +} + +/*! + * Main entry point. + */ +int main(const int argc, const char* argv[]) { + initializeLogger(); + if (!parseOptions(argc, argv)) { + return 0; } - - LOG4CPLUS_INFO(logger, "Nothing more to do, exiting."); + printHeader(argc, argv); + + testChecking(); + cleanUp(); return 0; } diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 64eaf0d41..cbb56f196 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -1106,8 +1106,6 @@ private: }; - - } // namespace storage } // namespace mrmc diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h index c25d00e37..6409b80da 100644 --- a/src/utility/OsDetection.h +++ b/src/utility/OsDetection.h @@ -19,4 +19,4 @@ # error Could not detect Operating System #endif -#endif // MRMC_UTILITY_OSDETECTION_H_ \ No newline at end of file +#endif // MRMC_UTILITY_OSDETECTION_H_ diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index bf79a0441..063fc0e33 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -125,6 +125,7 @@ void Settings::initDescriptions() { Settings::desc->add_options() ("help,h", "produce help message") ("verbose,v", "be verbose") + ("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")