diff --git a/CMakeLists.txt b/CMakeLists.txt index b297bca7c..c17fb7774 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,6 +28,7 @@ option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) option(USE_CARL "Sets whether carl should be included." ON) option(FORCE_COLOR "Force color output" OFF) option(STORM_COMPILE_WITH_CCACHE "Compile using CCache" ON) +option(STORM_LOGGING_FRAMEWORK "Use a framework for logging" OFF) set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") @@ -573,20 +574,21 @@ endif() ## Log4CPlus ## ############################################################# -set(BUILD_SHARED_LIBS OFF CACHE BOOL "If TRUE, log4cplus is built as a shared library, otherwise as a static library") -set(LOG4CPLUS_BUILD_LOGGINGSERVER OFF) -set(LOG4CPLUS_BUILD_TESTING OFF) -set(LOG4CPLUS_USE_UNICODE OFF) -set(LOG4CPLUS_DEFINE_INSTALL_TARGET OFF) -add_subdirectory("${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.3-rc1") -include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.3-rc1/include") -include_directories("${PROJECT_BINARY_DIR}/resources/3rdparty/log4cplus-1.1.3-rc1/include") # This adds the defines.hxx file - -list(APPEND STORM_LINK_LIBRARIES log4cplusS) -if (UNIX AND NOT APPLE) - list(APPEND STORM_LINK_LIBRARIES rt) -endif(UNIX AND NOT APPLE) - +if(STORM_LOGGING_FRAMEWORK) + set(BUILD_SHARED_LIBS OFF CACHE BOOL "If TRUE, log4cplus is built as a shared library, otherwise as a static library") + set(LOG4CPLUS_BUILD_LOGGINGSERVER OFF) + set(LOG4CPLUS_BUILD_TESTING OFF) + set(LOG4CPLUS_USE_UNICODE OFF) + set(LOG4CPLUS_DEFINE_INSTALL_TARGET OFF) + add_subdirectory("${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.3-rc1") + include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.3-rc1/include") + include_directories("${PROJECT_BINARY_DIR}/resources/3rdparty/log4cplus-1.1.3-rc1/include") # This adds the defines.hxx file + + list(APPEND STORM_LINK_LIBRARIES log4cplusS) + if (UNIX AND NOT APPLE) + list(APPEND STORM_LINK_LIBRARIES rt) + endif(UNIX AND NOT APPLE) +endif() ############################################################# ## ## Intel Threading Building Blocks (optional) diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index df81b46f7..ad4c82a0e 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -16,10 +16,7 @@ #include "src/storage/SparseMatrix.h" #include "src/utility/ConversionHelper.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; +#include "src/utility/macros.h" namespace storm { diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 758ac9a2a..0b384b539 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -186,18 +186,14 @@ namespace storm { } if (storm::settings::generalSettings().isVerboseSet()) { - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console."); + STORM_GLOBAL_LOGLEVEL_INFO(); } if (storm::settings::debugSettings().isDebugSet()) { - logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console."); + STORM_GLOBAL_LOGLEVEL_DEBUG(); + } if (storm::settings::debugSettings().isTraceSet()) { - logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); + STORM_GLOBAL_LOGLEVEL_TRACE(); } if (storm::settings::debugSettings().isLogfileSet()) { storm::utility::initializeFileLogging(); diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 349bfb56b..090a568b7 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -16,10 +16,6 @@ #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - namespace storm { namespace parser { diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index f18b46441..da200fe2e 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -17,11 +17,7 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/adapters/CarlAdapter.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "src/utility/macros.h" namespace storm { namespace parser { diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp index 86f2648eb..b4e8f30f0 100644 --- a/src/parser/MappedFile.cpp +++ b/src/parser/MappedFile.cpp @@ -14,11 +14,7 @@ #include #include "src/exceptions/FileIoException.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "src/utility/macros.h" namespace storm { namespace parser { diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index b4ee7be34..37eeacbcd 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -8,10 +8,6 @@ #include "src/adapters/CarlAdapter.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - namespace storm { namespace parser { diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 220451c33..b2d539c3a 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -11,6 +11,7 @@ #include "src/parser/SparseChoiceLabelingParser.h" #include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" namespace storm { namespace parser { diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 89322808c..e89fe76e2 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -14,11 +14,7 @@ #include "src/utility/cstring.h" #include "src/adapters/CarlAdapter.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "src/utility/macros.h" namespace storm { namespace parser { diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 35e1c3d59..2207813ab 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -8,11 +8,7 @@ #include "src/parser/MappedFile.h" #include "src/adapters/CarlAdapter.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "src/utility/macros.h" namespace storm { namespace parser { diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index bb912371b..793842849 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -13,11 +13,7 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "src/utility/macros.h" #include "storm-config.h" #ifdef STORM_HAVE_CUDA # include "cudaForStorm.h" diff --git a/src/storage/ModelFormulasPair.h b/src/storage/ModelFormulasPair.h index 490116c46..fab8cb3d1 100644 --- a/src/storage/ModelFormulasPair.h +++ b/src/storage/ModelFormulasPair.h @@ -1,6 +1,6 @@ #pragma once #include "../models/ModelBase.h" - +#include namespace storm { namespace logic { diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 253609210..3dbabf854 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -22,10 +22,6 @@ #include "src/utility/macros.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - namespace storm { namespace storage { diff --git a/src/utility/cstring.cpp b/src/utility/cstring.cpp index d80059e94..f27ca73a4 100644 --- a/src/utility/cstring.cpp +++ b/src/utility/cstring.cpp @@ -3,11 +3,7 @@ #include #include "src/exceptions/WrongFormatException.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "src/utility/macros.h" namespace storm { namespace utility { diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index e4839b1aa..de920ad21 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -16,11 +16,7 @@ #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/DdManager.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; +#include "src/utility/macros.h" namespace storm { namespace utility { diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp index d5cbb58db..72e3fd964 100644 --- a/src/utility/initialize.cpp +++ b/src/utility/initialize.cpp @@ -4,19 +4,26 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/DebugSettings.h" - +#ifdef STORM_LOGGING_FRAMEWORK log4cplus::Logger logger; log4cplus::Logger printer; +#else +int storm_runtime_loglevel = STORM_LOGLEVEL_WARN; +#endif + namespace storm { namespace utility { void initializeLogger() { +#ifdef STORM_LOGGING_FRAMEWORK auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; initializeLogger(loglevel); +#endif } +#ifdef STORM_LOGGING_FRAMEWORK void initializeLogger(log4cplus::LogLevel const& loglevel) { logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); @@ -26,6 +33,7 @@ namespace storm { logger.setLogLevel(loglevel); consoleLogAppender->setThreshold(loglevel); } +#endif void setUp() { initializeLogger(); @@ -37,10 +45,12 @@ namespace storm { } void initializeFileLogging() { +#ifdef STORM_LOGGING_FRAMEWORK 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); +#endif } } diff --git a/src/utility/initialize.h b/src/utility/initialize.h index 06fa8c2fa..dac87fa74 100644 --- a/src/utility/initialize.h +++ b/src/utility/initialize.h @@ -4,10 +4,6 @@ -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "log4cplus/consoleappender.h" -#include "log4cplus/fileappender.h" #include "macros.h" #include "src/settings/SettingsManager.h" @@ -19,8 +15,9 @@ namespace storm { * Initializes the logging framework and sets up logging to console. */ void initializeLogger(); +#ifdef STORM_LOGGING_FRAMEWORK void initializeLogger(log4cplus::LogLevel const&); - +#endif /*! * Performs some necessary initializations. */ diff --git a/src/utility/macros.h b/src/utility/macros.h index 037d1882b..79293f3ea 100644 --- a/src/utility/macros.h +++ b/src/utility/macros.h @@ -2,12 +2,113 @@ #define STORM_UTILITY_MACROS_H_ #include +#include "storm-config.h" +#ifndef STORM_LOGGING_FRAMEWORK +#include +#include + +extern int storm_runtime_loglevel; + +#define STORM_LOGLEVEL_ERROR 0 +#define STORM_LOGLEVEL_WARN 1 +#define STORM_LOGLEVEL_INFO 2 +#define STORM_LOGLEVEL_DEBUG 3 +#define STORM_LOGLEVEL_TRACE 4 + +#define STORM_LOG_DEBUG(message) \ +do { \ + if(storm_runtime_loglevel <= STORM_LOGLEVEL_DEBUG) { \ + std::cout << "LOG DBG: " << message << std::endl; \ + } \ +} while (false) + +#define STORM_LOG_TRACE(message) \ +do { \ + std::cout << "LOG TRC: " << message << std::endl; \ +} while(false) + + +// Define STORM_LOG_ASSERT which is only checked when NDEBUG is not set. +#ifndef NDEBUG +#define STORM_LOG_ASSERT(cond, message) \ +do { \ +if (!(cond)) { \ +std::cout << "LOG ERR: " << message << std::endl; \ +assert(cond); \ +} \ +} while (false) \ + +#else +#define STORM_LOG_ASSERT(cond, message) +#endif +// Define STORM_LOG_THROW to always throw the exception with the given message if the condition fails to hold. +#define STORM_LOG_THROW(cond, exception, message) \ +do { \ + if (!(cond)) { \ + std::cout << "LOG ERR: " << message << std::endl; \ + throw exception() << message; \ + } \ +} while (false) \ + + +// Define STORM_LOG_WARN, STORM_LOG_ERROR and STORM_LOG_INFO to log the given message with the corresponding log levels. +#define STORM_LOG_WARN(message) \ +do { \ + std::cout << "LOG WRN: " << message << std::endl; \ +} while (false) \ + +#define STORM_LOG_WARN_COND(cond, message) \ +do { \ + if (!(cond)) { \ + std::cout << "LOG WRN: " << message << std::endl; \ + } \ +} while (false) \ + +#define STORM_LOG_INFO(message) \ +do { \ + std::cout << "LOG INF: " << message << std::endl; \ +} while (false) \ + +#define STORM_LOG_INFO_COND(cond, message) \ +do { \ + if (!(cond)) { \ + std::cout << "LOG INF: " << message << std::endl; \ + } \ +} while (false) \ + +#define STORM_LOG_ERROR(message) \ +do { \ + std::stringstream __ss; \ + __ss << message; \ + std::cout << "LOG ERR: " << __ss.str() << std::endl; \ +} while (false) \ + +#define STORM_LOG_ERROR_COND(cond, message) \ +do { \ + if (!(cond)) { \ + STORM_LOG_ERROR(message) \ + } \ +} while (false) \ + +#define STORM_GLOBAL_LOGLEVEL_INFO() \ +do { \ +} while (false) + +#define STORM_GLOBAL_LOGLEVEL_DEBUG() \ +do { \ +} while(false) + +#define STORM_GLOBAL_LOGLEVEL_TRACE() \ +do { \ +} while(false) + + +#else // Include the parts necessary for Log4cplus. #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; - /*! * Define the macros STORM_LOG_DEBUG and STORM_LOG_TRACE. */ @@ -81,6 +182,30 @@ do { \ } \ } while (false) \ + +#define STORM_GLOBAL_LOGLEVEL_INFO() \ +do { \ +logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); \ +LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console."); \ +} while (false) + +#define STORM_GLOBAL_LOGLEVEL_DEBUG() \ +do { \ +logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); \ +logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); \ +LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console."); \ +} while(false) + +#define STORM_GLOBAL_LOGLEVEL_TRACE() \ +do { \ +logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); \ +logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); \ +LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); \ +} while(false) + + + +#endif /*! * Define the macros that print information and optionally also log it. */ diff --git a/storm-config.h.in b/storm-config.h.in index ec45f1445..e7fbd50e6 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -44,5 +44,6 @@ // Whether smtrat is available and to be used. #cmakedefine STORM_HAVE_SMTRAT +#cmakedefine STORM_LOGGING_FRAMEWORK #endif // STORM_GENERATED_STORMCONFIG_H_