From 54954569917c2ed45465e49746f9447689be5eb7 Mon Sep 17 00:00:00 2001 From: gereon Date: Sat, 11 May 2013 16:07:44 +0200 Subject: [PATCH] Added new log level "trace" Fixed bug in ExplicitModelAdapter --- src/adapters/ExplicitModelAdapter.cpp | 23 ++++++++++++++++++----- src/adapters/ExplicitModelAdapter.h | 10 ++++++++++ src/ir/Module.cpp | 4 ++-- src/ir/Module.h | 2 +- src/ir/Program.cpp | 22 ++++++++++++++++++++++ src/ir/Program.h | 2 ++ src/parser/PrismParser/VariableState.cpp | 10 +++++----- src/storm.cpp | 4 ++++ src/utility/Settings.cpp | 1 + 9 files changed, 65 insertions(+), 13 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index dc4080ce4..1bc602797 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -16,6 +16,8 @@ typedef std::pair, std::vector> StateType; +#include + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -95,6 +97,13 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { std::get<1>(*state)[index] = value; } + std::string ExplicitModelAdapter::toString(StateType const * const state) { + std::stringstream ss; + for (unsigned int i = 0; i < state->first.size(); i++) ss << state->first[i] << "\t"; + for (unsigned int i = 0; i < state->second.size(); i++) ss << state->second[i] << "\t"; + return ss.str(); + } + std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { std::shared_ptr> results(new std::vector(this->allStates.size())); for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { @@ -193,12 +202,16 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { * @return Resulting state. */ StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, storm::ir::Update const& update) const { + return this->applyUpdate(state, state, update); + } + + StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const { StateType* newState = new StateType(*state); for (auto assignedVariable : update.getBooleanAssignments()) { - setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(state)); + setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(baseState)); } for (auto assignedVariable : update.getIntegerAssignments()) { - setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(state)); + setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(baseState)); } return newState; } @@ -364,7 +377,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { // Iterate over all resultStates. for (auto it : resultStates) { // Apply the new update and get resulting state. - StateType* newState = this->applyUpdate(it.first, update); + StateType* newState = this->applyUpdate(it.first, this->allStates[stateID], update); probSum += update.getLikelihoodExpression()->getValueAsDouble(it.first); // Insert the new state into newStates array. // Take care of calculation of likelihood, combine identical states. @@ -425,7 +438,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { } numberOfTransitions += set.size(); } - LOG4CPLUS_DEBUG(logger, "Building deterministic transition matrix with " << numberOfTransitions << " transitions now."); + LOG4CPLUS_INFO(logger, "Building deterministic transition matrix: " << allStates.size() << " x " << allStates.size() << " with " << numberOfTransitions << " transitions."); // Now build matrix. std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); @@ -472,7 +485,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { * @return result matrix. */ std::shared_ptr> ExplicitModelAdapter::buildNondeterministicMatrix() { - LOG4CPLUS_DEBUG(logger, "Building nondeterministic transition matrix: " << this->numberOfChoices << " x " << allStates.size() << " with " << this->numberOfTransitions << " transitions now."); + LOG4CPLUS_INFO(logger, "Building nondeterministic transition matrix: " << this->numberOfChoices << " x " << allStates.size() << " with " << this->numberOfTransitions << " transitions."); std::shared_ptr> result(new storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); result->initialize(this->numberOfTransitions); if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 272d79c10..63cd91646 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -78,6 +78,7 @@ private: * @param value New value. */ static void setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value); + static std::string toString(StateType const * const state); /*! * Apply an update to the given state and return the resulting new state object. * This methods creates a copy of the given state. @@ -86,6 +87,15 @@ private: * @return Resulting state. */ StateType* applyUpdate(StateType const * const state, storm::ir::Update const& update) const; + /*! + * Apply an update to a given state and return the resulting new state object. + * Updates are done using the variable values from a given baseState. + * @params state State to be updated. + * @params baseState State used for update variables. + * @params update Update to be applied. + * @return Resulting state. + */ + StateType* applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const; /*! * Reads and combines variables from all program modules and stores them. diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 61c245b26..624f1876c 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -41,7 +41,7 @@ Module::Module(std::string moduleName, Module::Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder) : moduleName(moduleName) { - LOG4CPLUS_DEBUG(logger, "Start renaming " << module.moduleName << " to " << moduleName); + LOG4CPLUS_TRACE(logger, "Start renaming " << module.moduleName << " to " << moduleName); // First step: Create new Variables via the adder. adder->performRenaming(renaming); @@ -79,7 +79,7 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m } this->collectActions(); - LOG4CPLUS_DEBUG(logger, "Finished renaming..."); + LOG4CPLUS_TRACE(logger, "Finished renaming..."); } // Return the number of boolean variables. diff --git a/src/ir/Module.h b/src/ir/Module.h index 6fbe1658e..e4343e357 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -151,7 +151,7 @@ private: // A map of boolean variable names to their index. std::map booleanVariablesToIndexMap; - // A map of integer variable names to their details. + // A map of integer variable names to their index. std::map integerVariablesToIndexMap; // The commands associated with the module. diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index fd75d9b3e..96ad94b2b 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -118,6 +118,28 @@ std::map> P return this->labels; } +std::string Program::getVariableString() const { + std::map bools; + std::map ints; + unsigned maxInt = 0, maxBool = 0; + for (Module module: this->modules) { + for (unsigned int i = 0; i < module.getNumberOfBooleanVariables(); i++) { + storm::ir::BooleanVariable var = module.getBooleanVariable(i); + bools[var.getIndex()] = var.getName(); + if (var.getIndex() >= maxBool) maxBool = var.getIndex()+1; + } + for (unsigned int i = 0; i < module.getNumberOfIntegerVariables(); i++) { + storm::ir::IntegerVariable var = module.getIntegerVariable(i); + ints[var.getIndex()] = var.getName(); + if (var.getIndex() >= maxInt) maxInt = var.getIndex()+1; + } + } + std::stringstream ss; + for (unsigned int i = 0; i < maxBool; i++) ss << bools[i] << "\t"; + for (unsigned int i = 0; i < maxInt; i++) ss << ints[i] << "\t"; + return ss.str(); +} + } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index a181bbcc3..c12b6dddd 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -113,6 +113,8 @@ public: */ std::map> getLabels() const; + std::string getVariableString() const; + private: // The type of the model. ModelType modelType; diff --git a/src/parser/PrismParser/VariableState.cpp b/src/parser/PrismParser/VariableState.cpp index 3634b8954..e9be69435 100644 --- a/src/parser/PrismParser/VariableState.cpp +++ b/src/parser/PrismParser/VariableState.cpp @@ -37,7 +37,7 @@ VariableState::VariableState(bool firstRun) uint_fast64_t VariableState::addBooleanVariable(const std::string& name) { if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); - LOG4CPLUS_DEBUG(logger, "Adding boolean variable " << name << " with new id " << this->nextBooleanVariableIndex); + LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextBooleanVariableIndex); this->booleanVariables_.add(name, varExpr); this->booleanVariableNames_.add(name, name); this->nextBooleanVariableIndex++; @@ -56,7 +56,7 @@ uint_fast64_t VariableState::addBooleanVariable(const std::string& name) { uint_fast64_t VariableState::addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) { if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); - LOG4CPLUS_DEBUG(logger, "Adding integer variable " << name << " with new id " << this->nextIntegerVariableIndex); + LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextIntegerVariableIndex); this->integerVariables_.add(name, varExpr); this->integerVariableNames_.add(name, name); this->nextIntegerVariableIndex++; @@ -79,7 +79,7 @@ std::shared_ptr VariableState::getBooleanVariable(const std: return *res; } else { if (firstRun) { - LOG4CPLUS_DEBUG(logger, "Getting boolean variable " << name << ", was not yet created."); + LOG4CPLUS_TRACE(logger, "Getting boolean variable " << name << ", was not yet created."); return std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "bool", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); } else { LOG4CPLUS_ERROR(logger, "Getting boolean variable " << name << ", but was not found. This variable does not exist."); @@ -94,7 +94,7 @@ std::shared_ptr VariableState::getIntegerVariable(const std: return *res; } else { if (firstRun) { - LOG4CPLUS_DEBUG(logger, "Getting integer variable " << name << ", was not yet created."); + LOG4CPLUS_TRACE(logger, "Getting integer variable " << name << ", was not yet created."); return std::shared_ptr(new VariableExpression(BaseExpression::int_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); } else { LOG4CPLUS_ERROR(logger, "Getting integer variable " << name << ", but was not found. This variable does not exist."); @@ -133,7 +133,7 @@ void VariableState::performRenaming(const std::map& re } std::string* oldCmdName = this->commandNames_.find(it.first); if (oldCmdName != nullptr) { - LOG4CPLUS_DEBUG(logger, "Adding new command name " << it.second << " due to module renaming."); + LOG4CPLUS_TRACE(logger, "Adding new command name " << it.second << " due to module renaming."); this->commandNames_.at(it.second) = it.second; } } diff --git a/src/storm.cpp b/src/storm.cpp index 4cc2f5e41..fe3f24dc4 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -137,6 +137,10 @@ bool parseOptions(const int argc, const char* argv[]) { logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); LOG4CPLUS_INFO(logger, "Enable very verbose mode, log output gets printed to console."); } + if (s->isSet("trace")) { + logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enable trace mode, log output gets printed to console."); + } if (s->isSet("logfile")) { setUpFileLogging(); } diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index d6e2f5bc3..6d3bb950d 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -132,6 +132,7 @@ void Settings::initDescriptions() { ("help,h", "produce help message") ("verbose,v", "be verbose") ("debug", "be very verbose, intended for debugging") + ("trace", "be extremely verbose, expect lots of output") ("logfile,l", bpo::value(), "name of the log file") ("configfile,c", bpo::value(), "name of config file") ("test-prctl", bpo::value(), "name of prctl file")