From d9cb1a79f8a466b0e6b9b181e1025db6d0c895e1 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 16:17:42 +0200 Subject: [PATCH 1/7] Replace cout macros with l3pp Former-commit-id: 0cde42558de5f4aab1aa383025d9a1aa5220fec2 --- src/cli/cli.cpp | 7 +- src/utility/initialize.cpp | 43 +++++++++--- src/utility/initialize.h | 7 ++ src/utility/logging.h | 23 +++++++ src/utility/macros.h | 135 ++++--------------------------------- 5 files changed, 81 insertions(+), 134 deletions(-) create mode 100644 src/utility/logging.h diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index c9e88410d..0c2e80f53 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -186,14 +186,13 @@ namespace storm { } if (storm::settings::getModule().isVerboseSet()) { - STORM_GLOBAL_LOGLEVEL_INFO(); + storm::utility::setLogLevel(l3pp::LogLevel::INFO); } if (storm::settings::getModule().isDebugSet()) { - STORM_GLOBAL_LOGLEVEL_DEBUG(); - + storm::utility::setLogLevel(l3pp::LogLevel::DEBUG); } if (storm::settings::getModule().isTraceSet()) { - STORM_GLOBAL_LOGLEVEL_TRACE(); + storm::utility::setLogLevel(l3pp::LogLevel::TRACE); } if (storm::settings::getModule().isLogfileSet()) { storm::utility::initializeFileLogging(); diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp index ac139d1c9..2729c7791 100644 --- a/src/utility/initialize.cpp +++ b/src/utility/initialize.cpp @@ -1,30 +1,55 @@ #include "initialize.h" -#include "src/utility/macros.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/DebugSettings.h" -int storm_runtime_loglevel = STORM_LOGLEVEL_WARN; +#include +#include namespace storm { namespace utility { - + void initializeLogger() { - // Intentionally left empty. + l3pp::Logger::initialize(); + // By default output to std::cout + l3pp::SinkPtr sink = l3pp::StreamSink::create(std::cout); + l3pp::Logger::getRootLogger()->addSink(sink); + // Default to warn, set by user to something else + l3pp::Logger::getRootLogger()->setLevel(l3pp::LogLevel::WARN); + + l3pp::FormatterPtr fptr = l3pp::makeTemplateFormatter( + l3pp::FieldStr(), + ' (', l3pp::FieldStr, ':', l3pp::FieldStr, '): ', + l3pp::FieldStr(), '\n' + ); + sink->setFormatter(fptr); } - + void setUp() { initializeLogger(); std::cout.precision(10); } - + void cleanUp() { // Intentionally left empty. } - + + void setLogLevel(l3pp::LogLevel level) { + l3pp::Logger::getRootLogger()->setLevel(level); + if (level <= l3pp::LogLevel::DEBUG) { +#if STORM_LOG_DISABLE_DEBUG + std::cout << "***** warning ***** requested loglevel is not compiled\n"; +#endif + } + } + void initializeFileLogging() { - // FIXME. + if (storm::settings::getModule().isLogfileSet()) { + std::string logFileName = storm::settings::getModule().getLogfilename(); + l3pp::SinkPtr sink = l3pp::FileSink::create(logFileName); + l3pp::Logger::getRootLogger()->addSink(sink); + } } - + } } diff --git a/src/utility/initialize.h b/src/utility/initialize.h index 6241add70..48e4855c9 100644 --- a/src/utility/initialize.h +++ b/src/utility/initialize.h @@ -1,6 +1,8 @@ #ifndef STORM_UTILITY_INITIALIZE_H #define STORM_UTILITY_INITIALIZE_H +#include "src/utility/logging.h" + namespace storm { namespace utility { /*! @@ -17,6 +19,11 @@ namespace storm { */ void cleanUp(); + /*! + * Set the global log level + */ + void setLogLevel(l3pp::LogLevel level); + /*! * Sets up the logging to file. */ diff --git a/src/utility/logging.h b/src/utility/logging.h new file mode 100644 index 000000000..a036127b5 --- /dev/null +++ b/src/utility/logging.h @@ -0,0 +1,23 @@ +#ifndef STORM_UTILITY_LOGGING_H_ +#define STORM_UTILITY_LOGGING_H_ + +#include + +#if !defined(STORM_LOG_DISABLE_DEBUG) && !defined(STORM_LOG_DISABLE_TRACE) +#define STORM_LOG_TRACE(message) L3PP_LOG_TRACE(l3pp::Logging::getRootLogger(), message) +#else +#define STORM_LOG_TRACE(message) (void)(0) +#endif + +#if !defined(STORM_LOG_DISABLE_DEBUG) +#define STORM_LOG_DEBUG(message) L3PP_LOG_DEBUG(l3pp::Logging::getRootLogger(), message) +#else +#define STORM_LOG_DEBUG(message) (void)(0) +#endif + +// Define STORM_LOG_WARN, STORM_LOG_ERROR and STORM_LOG_INFO to log the given message with the corresponding log levels. +#define STORM_LOG_INFO(message) L3PP_LOG_INFO(l3pp::Logging::getRootLogger(), message) +#define STORM_LOG_WARN(message) L3PP_LOG_WARN(l3pp::Logging::getRootLogger(), message) +#define STORM_LOG_ERROR(message) L3PP_LOG_ERROR(l3pp::Logging::getRootLogger(), message) + +#endif /* STORM_UTILITY_LOGGING_H_ */ diff --git a/src/utility/macros.h b/src/utility/macros.h index 9c79fcc4d..2d49be58b 100644 --- a/src/utility/macros.h +++ b/src/utility/macros.h @@ -1,128 +1,47 @@ #ifndef STORM_UTILITY_MACROS_H_ #define STORM_UTILITY_MACROS_H_ -#include -#include - -#include "storm-config.h" +#include "src/utility/logging.h" #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 - -#ifdef STORM_LOG_DISABLE_DEBUG -#define STORM_LOG_DISABLE_TRACE -#endif - - -#define __SHORT_FORM_OF_FILE__ \ -(strrchr(__FILE__,'/') \ -? strrchr(__FILE__,'/')+1 \ -: __FILE__ \ -) - -#ifndef STORM_LOG_DISABLE_DEBUG -#define STORM_LOG_DEBUG(message) \ -do { \ - if(storm_runtime_loglevel >= STORM_LOGLEVEL_DEBUG) { \ - std::stringstream __ss; \ - __ss << message; \ - std::cout << "DEBUG (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << __ss.str() << std::endl; \ - } \ -} while (false) -#else -#define STORM_LOG_DEBUG(message) \ -do { \ -} while (false) -#endif - -#ifndef STORM_LOG_DISABLE_TRACE -#define STORM_LOG_TRACE(message) \ -do { \ - if(storm_runtime_loglevel >= STORM_LOGLEVEL_TRACE) { \ - std::stringstream __ss; \ - __ss << message; \ - std::cout << "TRACE (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << __ss.str() << std::endl; \ - } \ -} while(false) -#else -#define STORM_LOG_TRACE(message) \ -do { \ -} while (false) -#endif - +#include // 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 << "ASSERT FAILED (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << message << std::endl; \ -assert(cond); \ -} \ -} while (false) + if (!(cond)) { \ + STORM_LOG_ERROR(message); \ + assert(cond); \ + } \ +} while (false) #else -#define STORM_LOG_ASSERT(cond, message) +#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 << "ERROR (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << message << std::endl; \ + STORM_LOG_ERROR(message); \ 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 { \ - if(storm_runtime_loglevel >= STORM_LOGLEVEL_WARN) { \ - std::stringstream __ss; \ - __ss << message; \ - std::cout << "WARN (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << __ss.str() << std::endl; \ - } \ -} while (false) +} while (false) #define STORM_LOG_WARN_COND(cond, message) \ do { \ if (!(cond)) { \ - STORM_LOG_WARN(message); \ + STORM_LOG_WARN(message); \ } \ -} while (false) - -#define STORM_LOG_INFO(message) \ -do { \ - if(storm_runtime_loglevel >= STORM_LOGLEVEL_INFO) { \ - std::stringstream __ss; \ - __ss << message; \ - std::cout << "INFO (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << __ss.str() << std::endl; \ - } \ -} while (false) +} while (false) #define STORM_LOG_INFO_COND(cond, message) \ do { \ if (!(cond)) { \ STORM_LOG_INFO(message); \ } \ -} while (false) - -#define STORM_LOG_ERROR(message) \ -do { \ - if(storm_runtime_loglevel >= STORM_LOGLEVEL_ERROR) { \ - std::stringstream __ss; \ - __ss << message; \ - std::cout << "ERROR (" << __SHORT_FORM_OF_FILE__ << ":" << __LINE__ << "): " << __ss.str() << std::endl; \ - } \ -} while (false) \ +} while (false) #define STORM_LOG_ERROR_COND(cond, message) \ do { \ @@ -131,32 +50,6 @@ do { \ } \ } while (false) \ -#define STORM_GLOBAL_LOGLEVEL_INFO() \ -do { \ -storm_runtime_loglevel = STORM_LOGLEVEL_INFO; \ -} while (false) - -#ifndef STORM_LOG_DISABLE_DEBUG -#define STORM_GLOBAL_LOGLEVEL_DEBUG() \ -do { \ -storm_runtime_loglevel = STORM_LOGLEVEL_DEBUG; \ -} while(false) -#else -#define STORM_GLOBAL_LOGLEVEL_DEBUG() \ -std::cout << "***** warning ***** loglevel debug is not compiled\n" -#endif - -#ifndef STORM_LOG_DISABLE_TRACE -#define STORM_GLOBAL_LOGLEVEL_TRACE() \ -do { \ -storm_runtime_loglevel = STORM_LOGLEVEL_TRACE; \ -} while(false) -#else -#define STORM_GLOBAL_LOGLEVEL_TRACE() \ -std::cout << "***** warning ***** loglevel trace is not compiled\n" -#endif - - /*! * Define the macros that print information and optionally also log it. */ From 067b43525b7c7cc15a3f3a2190be2768517c1bd9 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 16:24:53 +0200 Subject: [PATCH 2/7] Add l3pp as project Former-commit-id: 2ea4009282606592e84371ad366a1305971106bd --- CMakeLists.txt | 10 ++++++++++ resources/3rdparty/CMakeLists.txt | 10 ++++++++++ 2 files changed, 20 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 6775e3fff..846980de3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -200,6 +200,16 @@ message(STATUS "StoRM - Using Compiler Configuration: ${STORM_COMPILED_BY}") # in the the system does not have a library add_subdirectory(resources/3rdparty) +############################################################# +## +## l3pp +## +############################################################# + +# l3pp is set up as external project +include_directories(${l3pp_INCLUDE}) +add_dependencies(resources l3pp) + ############################################################# ## ## gmm diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 9b30445f3..7008de089 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -81,3 +81,13 @@ set(GTEST_INCLUDE_DIR ${source_dir}/include PARENT_SCOPE) # Specify MainTest's link libraries ExternalProject_Get_Property(googletest binary_dir) set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a PARENT_SCOPE) + +ExternalProject_Add( + l3pp + GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git + GIT_TAG master + SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/l3pp + LOG_INSTALL ON +) +ExternalProject_Get_Property(l3pp source_dir) +set(l3pp_INCLUDE "${source_dir}/" PARENT_SCOPE) From 4e4bc255b5d6d770f465c250849773b97609f73f Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 17:10:02 +0200 Subject: [PATCH 3/7] Fix some typos in l3pp usage Former-commit-id: c9da06a59671298205b6aeb657d687e681c9d84e --- src/utility/initialize.cpp | 2 +- src/utility/logging.h | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp index 2729c7791..273d0dee0 100644 --- a/src/utility/initialize.cpp +++ b/src/utility/initialize.cpp @@ -19,7 +19,7 @@ namespace storm { l3pp::FormatterPtr fptr = l3pp::makeTemplateFormatter( l3pp::FieldStr(), - ' (', l3pp::FieldStr, ':', l3pp::FieldStr, '): ', + " (", l3pp::FieldStr(), ':', l3pp::FieldStr(), "): ", l3pp::FieldStr(), '\n' ); sink->setFormatter(fptr); diff --git a/src/utility/logging.h b/src/utility/logging.h index a036127b5..2fc58a008 100644 --- a/src/utility/logging.h +++ b/src/utility/logging.h @@ -1,23 +1,23 @@ #ifndef STORM_UTILITY_LOGGING_H_ #define STORM_UTILITY_LOGGING_H_ -#include +#include #if !defined(STORM_LOG_DISABLE_DEBUG) && !defined(STORM_LOG_DISABLE_TRACE) -#define STORM_LOG_TRACE(message) L3PP_LOG_TRACE(l3pp::Logging::getRootLogger(), message) +#define STORM_LOG_TRACE(message) L3PP_LOG_TRACE(l3pp::Logger::getRootLogger(), message) #else #define STORM_LOG_TRACE(message) (void)(0) #endif #if !defined(STORM_LOG_DISABLE_DEBUG) -#define STORM_LOG_DEBUG(message) L3PP_LOG_DEBUG(l3pp::Logging::getRootLogger(), message) +#define STORM_LOG_DEBUG(message) L3PP_LOG_DEBUG(l3pp::Logger::getRootLogger(), message) #else #define STORM_LOG_DEBUG(message) (void)(0) #endif // Define STORM_LOG_WARN, STORM_LOG_ERROR and STORM_LOG_INFO to log the given message with the corresponding log levels. -#define STORM_LOG_INFO(message) L3PP_LOG_INFO(l3pp::Logging::getRootLogger(), message) -#define STORM_LOG_WARN(message) L3PP_LOG_WARN(l3pp::Logging::getRootLogger(), message) -#define STORM_LOG_ERROR(message) L3PP_LOG_ERROR(l3pp::Logging::getRootLogger(), message) +#define STORM_LOG_INFO(message) L3PP_LOG_INFO(l3pp::Logger::getRootLogger(), message) +#define STORM_LOG_WARN(message) L3PP_LOG_WARN(l3pp::Logger::getRootLogger(), message) +#define STORM_LOG_ERROR(message) L3PP_LOG_ERROR(l3pp::Logger::getRootLogger(), message) #endif /* STORM_UTILITY_LOGGING_H_ */ From efae19b09285946c471014d6baf688dd000f3f85 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 17:10:45 +0200 Subject: [PATCH 4/7] Use toString() for exit rates, ADL not working for some reason Former-commit-id: cbc9eaf7222efe1ebe123185bb51b702097ac8ae --- src/builder/ExplicitDFTModelBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 4fb6131df..3f0682e54 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -86,7 +86,7 @@ namespace storm { } else { STORM_LOG_TRACE("Transition matrix: too big to print"); } - STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); + STORM_LOG_TRACE("Exit rates: " << storm::utility::vector::toString(modelComponents.exitRates)); STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); // Build state labeling From 8ef899ef1c58c54ea8a82ff038bde17ba854d8ed Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 17:30:10 +0200 Subject: [PATCH 5/7] Fix log file name argument Former-commit-id: c13b4ca3ad7687e24710fe3ce2e16d4304159298 --- src/settings/modules/DebugSettings.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp index 0f37e7ce7..92e8de9a9 100644 --- a/src/settings/modules/DebugSettings.cpp +++ b/src/settings/modules/DebugSettings.cpp @@ -38,7 +38,7 @@ namespace storm { } std::string DebugSettings::getLogfilename() const { - return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString(); + return this->getOption(logfileOptionName).getArgumentByName("filename").getValueAsString(); } bool DebugSettings::isTestSet() const { @@ -47,4 +47,4 @@ namespace storm { } // namespace modules } // namespace settings -} // namespace storm \ No newline at end of file +} // namespace storm From 346d4740d254c73ea4c6c5fa8af704ab644c186e Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Tue, 5 Jul 2016 09:07:25 +0200 Subject: [PATCH 6/7] Set l3pp project commands empty (header only) Former-commit-id: d99a6b5f0da4cdce485464de306a8a0662940f48 --- resources/3rdparty/CMakeLists.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 7008de089..88263eaad 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -87,6 +87,9 @@ ExternalProject_Add( GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git GIT_TAG master SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/l3pp + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND "" LOG_INSTALL ON ) ExternalProject_Get_Property(l3pp source_dir) From 5faebdff8682c1490051f3ee9454b19c55f482da Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 19 Jul 2016 11:46:22 +0200 Subject: [PATCH 7/7] constants in header Former-commit-id: 281e4908734c5f65f371db11161c064223a4b166 --- CMakeLists.txt | 2 +- src/builder/ExplicitDFTModelBuilder.cpp | 2 +- src/utility/constants.cpp | 520 ++++++++++++------------ src/utility/constants.h | 195 +++++++-- src/utility/storm.h | 2 +- src/utility/vector.h | 7 +- 6 files changed, 436 insertions(+), 292 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0c564cf61..0f5eb9612 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -364,7 +364,7 @@ find_package(CLN QUIET) set(STORM_USE_CLN_NUMBERS OFF) if(CLN_FOUND) set(STORM_HAVE_CLN ON) - set(STORM_USE_CLN_NUMBERS ON) + set(STORM_USE_CLN_NUMBERS OFF) message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") include_directories("${CLN_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 4fb6131df..25b96b9cd 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -2,7 +2,7 @@ #include #include #include -#include +#include "src/utility/vector.h" #include #include diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 4821d1b94..00b6e1154 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -1,168 +1,168 @@ -#include "src/utility/constants.h" - -#include "src/storage/sparse/StateType.h" +//#include "src/utility/constants.h" +// +//#include "src/storage/sparse/StateType.h" #include "src/storage/SparseMatrix.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" - -#include "src/adapters/CarlAdapter.h" - +//#include "src/settings/SettingsManager.h" +//#include "src/settings/modules/GeneralSettings.h" +// +//#include "src/adapters/CarlAdapter.h" +// namespace storm { namespace utility { - - template - ValueType one() { - return ValueType(1); - } - - template - ValueType zero() { - return ValueType(0); - } - - template - ValueType infinity() { - return std::numeric_limits::infinity(); - } - - template - bool isOne(ValueType const& a) { - return a == one(); - } - - template - bool isZero(ValueType const& a) { - return a == zero(); - } - - template - bool isConstant(ValueType const& a) { - return true; - } - - template<> - bool isOne(storm::RationalNumber const& a) { - return carl::isOne(a); - } - - template<> - bool isZero(storm::RationalNumber const& a) { - return carl::isZero(a); - } - - template<> - storm::RationalNumber infinity() { - // FIXME: this should be treated more properly. - return storm::RationalNumber(-1); - } - - template<> - bool isOne(storm::RationalFunction const& a) { - return a.isOne(); - } - - template<> - bool isZero(storm::RationalFunction const& a) { - return a.isZero(); - } - - template<> - bool isConstant(storm::RationalFunction const& a) { - return a.isConstant(); - } - - template<> - bool isOne(storm::Polynomial const& a) { - return a.isOne(); - } - - template<> - bool isZero(storm::Polynomial const& a) { - return a.isZero(); - } - - template<> - bool isConstant(storm::Polynomial const& a) { - return a.isConstant(); - } - - template<> - storm::RationalFunction infinity() { - // FIXME: this should be treated more properly. - return storm::RationalFunction(-1.0); - } - - template - ValueType pow(ValueType const& value, uint_fast64_t exponent) { - return std::pow(value, exponent); - } - - template - ValueType simplify(ValueType value) { - // In the general case, we don't do anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - - template<> - double convertNumber(double const& number){ - return number; - } - - template - ValueType abs(ValueType const& number) { - return std::fabs(number); - } - - template<> - RationalFunction& simplify(RationalFunction& value); - - template<> - RationalFunction&& simplify(RationalFunction&& value); - - template<> - RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { - return carl::pow(value, exponent); - } - - template<> - RationalFunction simplify(RationalFunction value) { - value.simplify(); - return value; - } - - template<> - RationalFunction& simplify(RationalFunction& value) { - value.simplify(); - return value; - } - - template<> - RationalFunction&& simplify(RationalFunction&& value) { - value.simplify(); - return std::move(value); - } - - template<> - double convertNumber(RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } - - template<> - RationalFunction convertNumber(double const& number){ - return RationalFunction(carl::rationalize(number)); - } - - template<> - storm::RationalNumber abs(storm::RationalNumber const& number) { - return carl::abs(number); - } +// template +// ValueType one() { +// return ValueType(1); +// } +// +// template +// ValueType zero() { +// return ValueType(0); +// } +// +// template +// ValueType infinity() { +// return std::numeric_limits::infinity(); +// } +// +// template +// bool isOne(ValueType const& a) { +// return a == one(); +// } +// +// template +// bool isZero(ValueType const& a) { +// return a == zero(); +// } +// +// template +// bool isConstant(ValueType const& a) { +// return true; +// } +// +// template<> +// bool isOne(storm::RationalNumber const& a) { +// return carl::isOne(a); +// } +// +// template<> +// bool isZero(storm::RationalNumber const& a) { +// return carl::isZero(a); +// } +// +// template<> +// storm::RationalNumber infinity() { +// // FIXME: this should be treated more properly. +// return storm::RationalNumber(-1); +// } +// +// template<> +// bool isOne(storm::RationalFunction const& a) { +// return a.isOne(); +// } +// +// template<> +// bool isZero(storm::RationalFunction const& a) { +// return a.isZero(); +// } +// +// template<> +// bool isConstant(storm::RationalFunction const& a) { +// return a.isConstant(); +// } +// +// template<> +// bool isOne(storm::Polynomial const& a) { +// return a.isOne(); +// } +// +// template<> +// bool isZero(storm::Polynomial const& a) { +// return a.isZero(); +// } +// +// template<> +// bool isConstant(storm::Polynomial const& a) { +// return a.isConstant(); +// } +// +// template<> +// storm::RationalFunction infinity() { +// // FIXME: this should be treated more properly. +// return storm::RationalFunction(-1.0); +// } +// +// template +// ValueType pow(ValueType const& value, uint_fast64_t exponent) { +// return std::pow(value, exponent); +// } +// +// template +// ValueType simplify(ValueType value) { +// // In the general case, we don't do anything here, but merely return the value. If something else is +// // supposed to happen here, the templated function can be specialized for this particular type. +// return value; +// } +// +// template<> +// double convertNumber(double const& number){ +// return number; +// } +// +// template +// ValueType abs(ValueType const& number) { +// return carl::abs(number); +// } +// +// template<> +// RationalFunction& simplify(RationalFunction& value); +// +// template<> +// RationalFunction&& simplify(RationalFunction&& value); +// +// template<> +// RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { +// return carl::pow(value, exponent); +// } +// +// template<> +// RationalFunction simplify(RationalFunction value) { +// value.simplify(); +// return value; +// } +// +// template<> +// RationalFunction& simplify(RationalFunction& value) { +// value.simplify(); +// return value; +// } +// +// template<> +// RationalFunction&& simplify(RationalFunction&& value) { +// value.simplify(); +// return std::move(value); +// } +// +// template<> +// double convertNumber(RationalNumber const& number){ +// return carl::toDouble(number); +// } +// +// template<> +// RationalNumber convertNumber(double const& number){ +// return carl::rationalize(number); +// } +// +// template<> +// RationalFunction convertNumber(double const& number){ +// return RationalFunction(carl::rationalize(number)); +// } +//// +//// template<> +//// storm::RationalNumber abs(storm::RationalNumber const& number) { +//// return carl::abs(number); +//// } +// template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { simplify(matrixEntry.getValue()); @@ -180,127 +180,127 @@ namespace storm { simplify(matrixEntry.getValue()); return std::move(matrixEntry); } - - // Explicit instantiations. - template bool isOne(double const& value); - template bool isZero(double const& value); - template bool isConstant(double const& value); - - template double one(); - template double zero(); - template double infinity(); - - template double pow(double const& value, uint_fast64_t exponent); - - template double simplify(double value); +// +// // Explicit instantiations. +// template bool isOne(double const& value); +// template bool isZero(double const& value); +// template bool isConstant(double const& value); +// +// template double one(); +// template double zero(); +// template double infinity(); +// +// template double pow(double const& value, uint_fast64_t exponent); +// +// template double simplify(double value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template double abs(double const& number); - - template bool isOne(float const& value); - template bool isZero(float const& value); - template bool isConstant(float const& value); - - template float one(); - template float zero(); - template float infinity(); - - template float pow(float const& value, uint_fast64_t exponent); - - template float simplify(float value); +// +// template double abs(double const& number); +// +// template bool isOne(float const& value); +// template bool isZero(float const& value); +// template bool isConstant(float const& value); +// +// template float one(); +// template float zero(); +// template float infinity(); +// +// template float pow(float const& value, uint_fast64_t exponent); +// +// template float simplify(float value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template bool isOne(int const& value); - template bool isZero(int const& value); - template bool isConstant(int const& value); - - template int one(); - template int zero(); - template int infinity(); - - template int pow(int const& value, uint_fast64_t exponent); - - template int simplify(int value); - + +// template bool isOne(int const& value); +// template bool isZero(int const& value); +// template bool isConstant(int const& value); +// +// template int one(); +// template int zero(); +// template int infinity(); +// +// template int pow(int const& value, uint_fast64_t exponent); +// +// template int simplify(int value); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - template bool isOne(storm::storage::sparse::state_type const& value); - template bool isZero(storm::storage::sparse::state_type const& value); - template bool isConstant(storm::storage::sparse::state_type const& value); - - template uint32_t one(); - template uint32_t zero(); - template uint32_t infinity(); - - template storm::storage::sparse::state_type one(); - template storm::storage::sparse::state_type zero(); - template storm::storage::sparse::state_type infinity(); - - template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); - - template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); - +// template bool isOne(storm::storage::sparse::state_type const& value); +// template bool isZero(storm::storage::sparse::state_type const& value); +// template bool isConstant(storm::storage::sparse::state_type const& value); +// +// template uint32_t one(); +// template uint32_t zero(); +// template uint32_t infinity(); +// +// template storm::storage::sparse::state_type one(); +// template storm::storage::sparse::state_type zero(); +// template storm::storage::sparse::state_type infinity(); +// +// template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); +// +// template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); +// template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - // Instantiations for rational number. - template bool isOne(storm::RationalNumber const& value); - template bool isZero(storm::RationalNumber const& value); - template bool isConstant(storm::RationalNumber const& value); - - template storm::RationalNumber one(); - template storm::RationalNumber zero(); - template storm::RationalNumber infinity(); - - template double convertNumber(storm::RationalNumber const& number); - template storm::RationalNumber convertNumber(double const& number); - - template storm::RationalNumber abs(storm::RationalNumber const& number); - -// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); - - template storm::RationalNumber simplify(storm::RationalNumber value); +// +// // Instantiations for rational number. +// template bool isOne(storm::RationalNumber const& value); +// template bool isZero(storm::RationalNumber const& value); +// template bool isConstant(storm::RationalNumber const& value); +// +// template storm::RationalNumber one(); +// template storm::RationalNumber zero(); +// template storm::RationalNumber infinity(); +// +// template double convertNumber(storm::RationalNumber const& number); +// template storm::RationalNumber convertNumber(double const& number); +// +// template storm::RationalNumber abs(storm::RationalNumber const& number); +// +//// template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); +// +// template storm::RationalNumber simplify(storm::RationalNumber value); template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - + #ifdef STORM_HAVE_CARL - template bool isOne(RationalFunction const& value); - template bool isZero(RationalFunction const& value); - template bool isConstant(RationalFunction const& value); - - template RationalFunction one(); - template RationalFunction zero(); - template storm::RationalFunction infinity(); - - template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); - template RationalFunction simplify(RationalFunction value); - template RationalFunction& simplify(RationalFunction& value); - template RationalFunction&& simplify(RationalFunction&& value); - - template Polynomial one(); - template Polynomial zero(); - - template bool isOne(Interval const& value); - template bool isZero(Interval const& value); - template bool isConstant(Interval const& value); - - template Interval one(); - template Interval zero(); - +// template bool isOne(RationalFunction const& value); +// template bool isZero(RationalFunction const& value); +// template bool isConstant(RationalFunction const& value); +// +// template RationalFunction one(); +// template RationalFunction zero(); +// template storm::RationalFunction infinity(); +// +// template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); +// template RationalFunction simplify(RationalFunction value); +// template RationalFunction& simplify(RationalFunction& value); +// template RationalFunction&& simplify(RationalFunction&& value); +// +// template Polynomial one(); +// template Polynomial zero(); +// +// template bool isOne(Interval const& value); +// template bool isZero(Interval const& value); +// template bool isConstant(Interval const& value); +// +// template Interval one(); +// template Interval zero(); + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); #endif - +// } } diff --git a/src/utility/constants.h b/src/utility/constants.h index 4ec4e7539..7f97acdb4 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,6 +11,11 @@ #include #include +#include "src/storage/sparse/StateType.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/adapters/CarlAdapter.h" namespace storm { @@ -20,42 +25,182 @@ namespace storm { } namespace utility { - + template - ValueType one(); - + ValueType one() { + return ValueType(1); + } + template - ValueType zero(); - + ValueType zero() { + return ValueType(0); + } + template - ValueType infinity(); - + ValueType infinity() { + return std::numeric_limits::infinity(); + } + template - bool isOne(ValueType const& a); - + bool isOne(ValueType const& a) { + return a == one(); + } + template - bool isZero(ValueType const& a); - + bool isZero(ValueType const& a) { + return a == zero(); + } + template - bool isConstant(ValueType const& a); - + bool isConstant(ValueType const& a) { + return true; + } + + template<> + bool isOne(storm::RationalNumber const& a) { + return carl::isOne(a); + } + + template<> + bool isZero(storm::RationalNumber const& a) { + return carl::isZero(a); + } + + template<> + storm::RationalNumber infinity() { + // FIXME: this should be treated more properly. + return storm::RationalNumber(-1); + } + + template<> + bool isOne(storm::RationalFunction const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::RationalFunction const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::RationalFunction const& a) { + return a.isConstant(); + } + + template<> + bool isOne(storm::Polynomial const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::Polynomial const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::Polynomial const& a) { + return a.isConstant(); + } + + template<> + storm::RationalFunction infinity() { + // FIXME: this should be treated more properly. + return storm::RationalFunction(-1.0); + } + template - ValueType pow(ValueType const& value, uint_fast64_t exponent); - + ValueType pow(ValueType const& value, uint_fast64_t exponent) { + return std::pow(value, exponent); + } + template - ValueType simplify(ValueType value); - - template - storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + ValueType simplify(ValueType value) { + // In the general case, we don't do anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. + return value; + } - template - storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - - template + template TargetType convertNumber(SourceType const& number); - + + template<> + double convertNumber(double const& number){ + return number; + } + template - ValueType abs(ValueType const& number); + ValueType abs(ValueType const& number) { + return carl::abs(number); + } + + template<> + RationalFunction& simplify(RationalFunction& value); + + template<> + RationalFunction&& simplify(RationalFunction&& value); + + template<> + RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { + return carl::pow(value, exponent); + } + + template<> + RationalFunction simplify(RationalFunction value) { + value.simplify(); + return value; + } + + template<> + RationalFunction& simplify(RationalFunction& value) { + value.simplify(); + return value; + } + + template<> + RationalFunction&& simplify(RationalFunction&& value) { + value.simplify(); + return std::move(value); + } + + template<> + double convertNumber(RationalNumber const& number){ + return carl::toDouble(number); + } + + template<> + RationalNumber convertNumber(double const& number){ + return carl::rationalize(number); + } + + template<> + RationalFunction convertNumber(double const& number){ + return RationalFunction(carl::rationalize(number)); + } +// +// template<> +// storm::RationalNumber abs(storm::RationalNumber const& number) { +// return carl::abs(number); +// } + + template + storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + simplify(matrixEntry.getValue()); + return matrixEntry; + } + + template + storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { + simplify(matrixEntry.getValue()); + return std::move(matrixEntry); + } + + } } diff --git a/src/utility/storm.h b/src/utility/storm.h index 49ef4bf04..6dd9dc526 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -243,7 +243,7 @@ namespace storm { case storm::settings::modules::CoreSettings::Engine::Sparse: { std::shared_ptr> sparseModel = model->template as>(); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); - return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant); + return (sparseModel, formula, onlyInitialStatesRelevant); } case storm::settings::modules::CoreSettings::Engine::Hybrid: { std::shared_ptr> ddModel = model->template as>(); diff --git a/src/utility/vector.h b/src/utility/vector.h index 6faf88c7c..e22564f08 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -12,7 +12,6 @@ #include #include "src/storage/BitVector.h" -#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/solver/OptimizationDirection.h" @@ -588,7 +587,7 @@ namespace storm { * @return True iff the elements are considered equal. */ template - bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) { + bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) { if (relativeError) { if (val2 == 0) { return (storm::utility::abs(val1) <= precision); @@ -612,7 +611,7 @@ namespace storm { * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. */ template - bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T const& precision, bool relativeError) { STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { @@ -636,7 +635,7 @@ namespace storm { * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. */ template - bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T precision, bool relativeError) { + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T const& precision, bool relativeError) { STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); for (uint_fast64_t position : positions) {