diff --git a/src/storm.cpp b/src/storm.cpp index 230223125..2ed0a42d3 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -8,7 +8,7 @@ */ int main(const int argc, const char** argv) { try { - storm::utility::cli::setUp(); + storm::utility::setUp(); storm::utility::cli::printHeader(argc, argv); bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv); if (!optionsCorrect) { @@ -19,7 +19,7 @@ int main(const int argc, const char** argv) { storm::utility::cli::processOptions(); // All operations have now been performed, so we clean up everything and terminate. - storm::utility::cli::cleanUp(); + storm::utility::cleanUp(); return 0; } catch (storm::exceptions::BaseException const& exception) { STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what()); diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp new file mode 100644 index 000000000..99f425a8d --- /dev/null +++ b/src/utility/cli.cpp @@ -0,0 +1,162 @@ +#include "cli.h" + +// Includes for the linked libraries and versions header. +#ifdef STORM_HAVE_INTELTBB +# include "tbb/tbb_stddef.h" +#endif +#ifdef STORM_HAVE_GLPK +# include "glpk.h" +#endif +#ifdef STORM_HAVE_GUROBI +# include "gurobi_c.h" +#endif +#ifdef STORM_HAVE_Z3 +# include "z3.h" +#endif +#ifdef STORM_HAVE_MSAT +# include "mathsat.h" +#endif +#ifdef STORM_HAVE_CUDA +#include +#include +#endif + +#ifdef STORM_HAVE_SMTRAT +#include "lib/smtrat.h" +#endif + +namespace storm { + namespace utility { + namespace cli { + std::string getCurrentWorkingDirectory() { + char temp[512]; + return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); + } + + void printHeader(const int argc, const char* argv[]) { + std::cout << "StoRM" << std::endl; + std::cout << "--------" << std::endl << std::endl; + + + // std::cout << storm::utility::StormVersion::longVersionString() << std::endl; +#ifdef STORM_HAVE_INTELTBB + std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; +#endif +#ifdef STORM_HAVE_GLPK + std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; +#endif +#ifdef STORM_HAVE_GUROBI + std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; +#endif +#ifdef STORM_HAVE_Z3 + unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; + Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); + std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; +#endif +#ifdef STORM_HAVE_MSAT + char* msatVersion = msat_get_version(); + std::cout << "Linked with " << msatVersion << "." << std::endl; + msat_free(msatVersion); +#endif +#ifdef STORM_HAVE_SMTRAT + std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl; +#endif +#ifdef STORM_HAVE_CARL + std::cout << "Linked with CARL." << std::endl; + // TODO get version string +#endif + +#ifdef STORM_HAVE_CUDA + int deviceCount = 0; + cudaError_t error_id = cudaGetDeviceCount(&deviceCount); + + if (error_id == cudaSuccess) + { + std::cout << "Compiled with CUDA support, "; + // This function call returns 0 if there are no CUDA capable devices. + if (deviceCount == 0) + { + std::cout<< "but there are no available device(s) that support CUDA." << std::endl; + } else + { + std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl; + } + + int dev, driverVersion = 0, runtimeVersion = 0; + + for (dev = 0; dev < deviceCount; ++dev) + { + cudaSetDevice(dev); + cudaDeviceProp deviceProp; + cudaGetDeviceProperties(&deviceProp, dev); + + std::cout << "CUDA Device " << dev << ": \"" << deviceProp.name << "\"" << std::endl; + + // Console log + cudaDriverGetVersion(&driverVersion); + cudaRuntimeGetVersion(&runtimeVersion); + std::cout << " CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl; + std::cout << " CUDA Capability Major/Minor version number: " << deviceProp.major<<"."<(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds + uLargeInteger.LowPart = ftUser.dwLowDateTime; + uLargeInteger.HighPart = ftUser.dwHighDateTime; + double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; + + std::cout << "CPU Time: " << std::endl; + std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; + std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; +#endif + } + + } + } +} \ No newline at end of file diff --git a/src/utility/cli.h b/src/utility/cli.h index 40f50acfa..de6db5768 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -8,39 +8,11 @@ #include #include +#include "initialize.h" + #include "storm-config.h" -// Includes for the linked libraries and versions header. -#ifdef STORM_HAVE_INTELTBB -# include "tbb/tbb_stddef.h" -#endif -#ifdef STORM_HAVE_GLPK -# include "glpk.h" -#endif -#ifdef STORM_HAVE_GUROBI -# include "gurobi_c.h" -#endif -#ifdef STORM_HAVE_Z3 -# include "z3.h" -#endif -#ifdef STORM_HAVE_MSAT -# include "mathsat.h" -#endif -#ifdef STORM_HAVE_CUDA -#include -#include -#endif -#ifdef STORM_HAVE_SMTRAT -#include "lib/smtrat.h" -#endif - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "log4cplus/consoleappender.h" -#include "log4cplus/fileappender.h" -log4cplus::Logger logger; -log4cplus::Logger printer; // Headers that provide auxiliary functionality. #include "src/utility/storm-version.h" @@ -93,181 +65,8 @@ namespace storm { namespace utility { namespace cli { - /*! - * Initializes the logging framework and sets up logging to console. - */ - void initializeLogger() { - logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - 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"))); - logger.addAppender(consoleLogAppender); - auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; - logger.setLogLevel(loglevel); - consoleLogAppender->setThreshold(loglevel); - } - - /*! - * Performs some necessary initializations. - */ - void setUp() { - initializeLogger(); - std::cout.precision(10); - } - - /*! - * Performs some necessary clean-up. - */ - void cleanUp() { - // Intentionally left empty. - } - - /*! - * Sets up the logging to file. - */ - void initializeFileLogging() { - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename())); - 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); - } - - /*! - * Gives the current working directory - * - * @return std::string The path of the current working directory - */ - std::string getCurrentWorkingDirectory() { - char temp[512]; - return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); - } - - /*! - * Prints the header including information about the linked libraries. - */ - void printHeader(const int argc, const char* argv[]) { - std::cout << "StoRM" << std::endl; - std::cout << "--------" << std::endl << std::endl; - - - // std::cout << storm::utility::StormVersion::longVersionString() << std::endl; -#ifdef STORM_HAVE_INTELTBB - std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; -#endif -#ifdef STORM_HAVE_GLPK - std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; -#endif -#ifdef STORM_HAVE_GUROBI - std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; -#endif -#ifdef STORM_HAVE_Z3 - unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; - Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); - std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; -#endif -#ifdef STORM_HAVE_MSAT - char* msatVersion = msat_get_version(); - std::cout << "Linked with " << msatVersion << "." << std::endl; - msat_free(msatVersion); -#endif -#ifdef STORM_HAVE_SMTRAT - std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl; -#endif -#ifdef STORM_HAVE_CARL - std::cout << "Linked with CARL." << std::endl; - // TODO get version string -#endif - -#ifdef STORM_HAVE_CUDA - int deviceCount = 0; - cudaError_t error_id = cudaGetDeviceCount(&deviceCount); - - if (error_id == cudaSuccess) - { - std::cout << "Compiled with CUDA support, "; - // This function call returns 0 if there are no CUDA capable devices. - if (deviceCount == 0) - { - std::cout<< "but there are no available device(s) that support CUDA." << std::endl; - } else - { - std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl; - } - - int dev, driverVersion = 0, runtimeVersion = 0; - - for (dev = 0; dev < deviceCount; ++dev) - { - cudaSetDevice(dev); - cudaDeviceProp deviceProp; - cudaGetDeviceProperties(&deviceProp, dev); - - std::cout << "CUDA Device " << dev << ": \"" << deviceProp.name << "\"" << std::endl; - - // Console log - cudaDriverGetVersion(&driverVersion); - cudaRuntimeGetVersion(&runtimeVersion); - std::cout << " CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl; - std::cout << " CUDA Capability Major/Minor version number: " << deviceProp.major<<"."<(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds - uLargeInteger.LowPart = ftUser.dwLowDateTime; - uLargeInteger.HighPart = ftUser.dwHighDateTime; - double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; - - std::cout << "CPU Time: " << std::endl; - std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; - std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; -#endif - } + + /*! diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp new file mode 100644 index 000000000..7ca64f1d3 --- /dev/null +++ b/src/utility/initialize.cpp @@ -0,0 +1,35 @@ +#include "initialize.h" + +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace utility { + void initializeLogger() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + 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"))); + logger.addAppender(consoleLogAppender); + auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; + logger.setLogLevel(loglevel); + consoleLogAppender->setThreshold(loglevel); + } + + void setUp() { + initializeLogger(); + std::cout.precision(10); + } + + void cleanUp() { + // Intentionally left empty. + } + + void initializeFileLogging() { + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename())); + 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); + } + + } +} diff --git a/src/utility/initialize.h b/src/utility/initialize.h new file mode 100644 index 000000000..4a848b89b --- /dev/null +++ b/src/utility/initialize.h @@ -0,0 +1,41 @@ +#ifndef INITIALIZE_H +#define INITIALIZE_H + + + + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" +log4cplus::Logger logger; +log4cplus::Logger printer; + + +namespace storm { + namespace utility { + /*! + * Initializes the logging framework and sets up logging to console. + */ + void initializeLogger(); + + /*! + * Performs some necessary initializations. + */ + void setUp(); + + /*! + * Performs some necessary clean-up. + */ + void cleanUp(); + + /*! + * Sets up the logging to file. + */ + void initializeFileLogging(); + + } +} + +#endif /* INITIALIZE_H */ +