Added new log level "trace"

Fixed bug in ExplicitModelAdapter

src/adapters/ExplicitModelAdapter.cpp

@@ -16,6 +16,8 @@
 
 typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType;
 
+#include <sstream>
+
 #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<std::vector<double>> ExplicitModelAdapter::getStateRewards(std::vector<storm::ir::StateReward> const & rewards) {
 		std::shared_ptr<std::vector<double>> results(new std::vector<double>(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<storm::storage::SparseMatrix<double>> result(new storm::storage::SparseMatrix<double>(allStates.size()));
@@ -472,7 +485,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
 	 * @return result matrix.
 	 */
 	std::shared_ptr<storm::storage::SparseMatrix<double>> 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<storm::storage::SparseMatrix<double>> result(new storm::storage::SparseMatrix<double>(this->numberOfChoices, allStates.size()));
 		result->initialize(this->numberOfTransitions);
 		if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) {

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.

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<std::string, std::string>& renaming, std::shared_ptr<VariableAdder> 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.

src/ir/Module.h

@@ -151,7 +151,7 @@ private:
 	// A map of boolean variable names to their index.
 	std::map<std::string, uint_fast64_t> booleanVariablesToIndexMap;
 
-	// A map of integer variable names to their details.
+	// A map of integer variable names to their index.
 	std::map<std::string, uint_fast64_t> integerVariablesToIndexMap;
 
 	// The commands associated with the module.

src/ir/Program.cpp

@@ -118,6 +118,28 @@ std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> P
 	return this->labels;
 }
 
+std::string Program::getVariableString() const {
+	std::map<unsigned int, std::string> bools;
+	std::map<unsigned int, std::string> 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

src/ir/Program.h

@@ -113,6 +113,8 @@ public:
 	 */
 	std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> getLabels() const;
 
+	std::string getVariableString() const;
+
 private:
 	// The type of the model.
 	ModelType modelType;

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<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(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<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper) {
 	if (firstRun) {
 		std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(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<VariableExpression> 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<VariableExpression>(new VariableExpression(BaseExpression::bool_, std::numeric_limits<uint_fast64_t>::max(), "bool", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(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<VariableExpression> 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<VariableExpression>(new VariableExpression(BaseExpression::int_, std::numeric_limits<uint_fast64_t>::max(), "int", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(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<std::string, std::string>& 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;
 		}
 	}

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();
 	}

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<std::string>(), "name of the log file")
 		("configfile,c", bpo::value<std::string>(), "name of config file")
 		("test-prctl", bpo::value<std::string>(), "name of prctl file")