From ebe6775b279fbecd1fb1281c97dab0f9bc7785df Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Fri, 1 Jul 2016 10:45:08 +0200 Subject: [PATCH 01/11] Fix missing ValueType template arguments (which defaulted to double) Former-commit-id: a97910eaf929907bd2ba6e1c70c727bb62875566 --- src/builder/DdPrismModelBuilder.cpp | 25 ++++++++----------- src/builder/DdPrismModelBuilder.h | 2 +- src/models/symbolic/Ctmc.cpp | 2 +- src/models/symbolic/DeterministicModel.cpp | 4 +-- src/models/symbolic/Dtmc.cpp | 2 +- src/models/symbolic/Mdp.cpp | 2 +- src/models/symbolic/Model.cpp | 2 +- src/models/symbolic/StandardRewardModel.cpp | 2 +- src/storage/dd/Add.cpp | 2 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 2 +- src/storage/dd/cudd/InternalCuddDdManager.cpp | 2 +- 11 files changed, 22 insertions(+), 25 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 2af7fed58..a397b0de0 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -32,12 +32,9 @@ namespace storm { template class DdPrismModelBuilder::GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); - - rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); - columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); } // The program that is currently translated. @@ -49,12 +46,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; std::shared_ptr> variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; std::shared_ptr> variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. std::vector> rowColumnMetaVariablePairs; @@ -794,7 +791,7 @@ namespace storm { } } - result.setValue(metaVariableNameToValueMap, 1); + result.setValue(metaVariableNameToValueMap, ValueType(1)); return result; } @@ -835,7 +832,7 @@ namespace storm { for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { // Determine the set of states with exactly currentChoices choices. - equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(static_cast(currentChoices))); + equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices))); // If there is no such state, continue with the next possible number of choices. if (equalsNumberOfChoicesDd.isZero()) { @@ -1110,7 +1107,7 @@ namespace storm { } template - storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { + storm::models::symbolic::StandardRewardModel DdPrismModelBuilder::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd) { // Start by creating the state reward vector. boost::optional> stateRewards; @@ -1222,7 +1219,7 @@ namespace storm { } } - return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); + return storm::models::symbolic::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards); } template @@ -1394,7 +1391,7 @@ namespace storm { selectedRewardModels.push_back(preparedProgram->getRewardModel(0)); } - std::unordered_map> rewardModels; + std::unordered_map> rewardModels; for (auto const& rewardModel : selectedRewardModels) { rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, transitionMatrix, reachableStatesAdd, stateActionDd)); } @@ -1406,11 +1403,11 @@ namespace storm { } if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 0cb8cc6fd..6db0c4639 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -238,7 +238,7 @@ namespace storm { static storm::dd::Add createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); + static storm::models::symbolic::StandardRewardModel createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add const& transitionMatrix, storm::dd::Add const& reachableStatesAdd, storm::dd::Add const& stateActionDd); static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp index 2f1e65aec..1c612d090 100644 --- a/src/models/symbolic/Ctmc.cpp +++ b/src/models/symbolic/Ctmc.cpp @@ -23,7 +23,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables()); } diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp index 66f97bc87..6824357d6 100644 --- a/src/models/symbolic/DeterministicModel.cpp +++ b/src/models/symbolic/DeterministicModel.cpp @@ -24,7 +24,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { // Intentionally left empty. } @@ -34,4 +34,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp index a9483862f..6f63ff394 100644 --- a/src/models/symbolic/Dtmc.cpp +++ b/src/models/symbolic/Dtmc.cpp @@ -33,4 +33,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp index 70017195a..f438e6f1d 100644 --- a/src/models/symbolic/Mdp.cpp +++ b/src/models/symbolic/Mdp.cpp @@ -34,4 +34,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 25bc5404b..16339c0d1 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -249,4 +249,4 @@ namespace storm { } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp index 4ec405405..1342abb3d 100644 --- a/src/models/symbolic/StandardRewardModel.cpp +++ b/src/models/symbolic/StandardRewardModel.cpp @@ -155,4 +155,4 @@ namespace storm { template class StandardRewardModel; } } -} \ No newline at end of file +} diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index bcff0e3da..a6cb3daac 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -767,4 +767,4 @@ namespace storm { template class Add; template class Add; } -} \ No newline at end of file +} diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 0925b4f58..393e8d262 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -596,4 +596,4 @@ namespace storm { template class InternalAdd; template class InternalAdd; } -} \ No newline at end of file +} diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp index 9f33c803d..5fc5ebcd0 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -106,4 +106,4 @@ namespace storm { template InternalAdd InternalDdManager::getConstant(double const& value) const; template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; } -} \ No newline at end of file +} From d02c918f6a89f74e1234bc27e575dd7105de99a1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 1 Jul 2016 11:11:16 +0200 Subject: [PATCH 02/11] forgot a little something... Former-commit-id: dc5b68bdb61e94cd36dc570200e0d30c58689bfd --- src/models/sparse/StandardRewardModel.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index c8fd2aa8f..823d3a884 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -248,7 +248,13 @@ namespace storm { if(hasStateRewards() && !std::all_of(getStateRewardVector().begin(), getStateRewardVector().end(), storm::utility::isZero)) { return false; } - return !(static_cast(this->optionalStateRewardVector) || static_cast(this->optionalStateActionRewardVector) || static_cast(this->optionalTransitionRewardMatrix)); + if(hasStateActionRewards() && !std::all_of(getStateActionRewardVector().begin(), getStateActionRewardVector().end(), storm::utility::isZero)) { + return false; + } + if(hasTransitionRewards() && !std::all_of(getTransitionRewardMatrix().begin(), getTransitionRewardMatrix().end(), [](storm::storage::MatrixEntry entry){ return storm::utility::isZero(entry.getValue()); })) { + return false; + } + return true; } From 4f1b8f12f0a5b81c7a9e8ace7a631c08cdae9d58 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 1 Jul 2016 15:08:25 +0200 Subject: [PATCH 03/11] Extra method Former-commit-id: 44b165558da3d348f8017cb31700a501b7c8e468 --- src/utility/macros.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/utility/macros.h b/src/utility/macros.h index 9c79fcc4d..b72cf5f26 100644 --- a/src/utility/macros.h +++ b/src/utility/macros.h @@ -131,6 +131,11 @@ do { \ } \ } while (false) \ +#define STORM_GLOBAL_LOGLEVEL_ERROR() \ +do { \ +storm_runtime_loglevel = STORM_LOGLEVEL_ERROR; \ +} while(false) + #define STORM_GLOBAL_LOGLEVEL_INFO() \ do { \ storm_runtime_loglevel = STORM_LOGLEVEL_INFO; \ From d9cb1a79f8a466b0e6b9b181e1025db6d0c895e1 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 16:17:42 +0200 Subject: [PATCH 04/11] 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 05/11] 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 06/11] 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 07/11] 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 08/11] 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 09/11] 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 c672f7aea22f7b541c51becff3dc432b534210a2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 9 Jul 2016 21:01:41 +0200 Subject: [PATCH 10/11] fix in bounded reachability computation with Markov automata Former-commit-id: fe2b39977886f2a3c4962341f3d4968bc61b1928 --- src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 7817dc644..90f858756 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -72,7 +72,7 @@ namespace storm { std::vector bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. - std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates); + std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowGroupSumVector(probabilisticNonGoalStates, goalStates); std::vector bMarkovianFixed; bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); for (auto state : markovianNonGoalStates) { From 2b399c887b5a90d701114cd4f850aeee777e423a Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 20 Jul 2016 17:19:44 +0200 Subject: [PATCH 11/11] Doxygen not required Former-commit-id: a5599d681da4006826000f78ebef338177b9bd97 --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 846980de3..54ee8452f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -744,7 +744,7 @@ endif(LINK_LIBCXXABI) ## ############################################################# -find_package(Doxygen REQUIRED) +find_package(Doxygen) # Add a target to generate API documentation with Doxygen if(DOXYGEN_FOUND) set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc")