From c3cfc5404c9ac090caa20e939bdcc09149a3284f Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 30 Apr 2013 15:05:42 +0200
Subject: [PATCH] Somewhat fixed weird issue during module renaming.

The "fix" is very weird (see VariableState.cpp:55 and following) and still seems to lead to a segfault upon program termination...
---
 src/ir/Module.cpp                             |  15 +-
 src/ir/expressions/BinaryExpression.h         |   7 +-
 src/ir/expressions/VariableExpression.h       |   2 +
 src/parser/PrismParser.cpp                    |  12 +-
 .../PrismParser/BooleanExpressionGrammar.cpp  |   2 +-
 src/parser/PrismParser/Includes.h             |   4 +
 .../PrismParser/IntegerExpressionGrammar.cpp  |   2 +-
 src/parser/PrismParser/VariableState.cpp      | 135 ++++++++++++++++++
 src/parser/PrismParser/VariableState.h        | 117 +++------------
 9 files changed, 189 insertions(+), 107 deletions(-)
 create mode 100644 src/parser/PrismParser/VariableState.cpp

diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp
index 80aa288c3..40d40fb2f 100644
--- a/src/ir/Module.cpp
+++ b/src/ir/Module.cpp
@@ -12,6 +12,10 @@
 #include <sstream>
 #include <iostream>
 
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+extern log4cplus::Logger logger;
+
 namespace storm {
 
 namespace ir {
@@ -37,29 +41,30 @@ 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);
 	this->booleanVariables.reserve(module.booleanVariables.size());
 	for (BooleanVariable it: module.booleanVariables) {
 		if (renaming.count(it.getName()) > 0) {
 			this->booleanVariablesToIndexMap[renaming.at(it.getName())] = adder->addBooleanVariable(renaming.at(it.getName()), it.getInitialValue());
-		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+		} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
 	}
 	this->integerVariables.reserve(module.integerVariables.size());
 	for (IntegerVariable it: module.integerVariables) {
 		if (renaming.count(it.getName()) > 0) {
 			this->integerVariablesToIndexMap[renaming.at(it.getName())] = adder->addIntegerVariable(renaming.at(it.getName()), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
-		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+		} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
 	}
 	this->booleanVariables.reserve(module.booleanVariables.size());
 	for (BooleanVariable it: module.booleanVariables) {
 		if (renaming.count(it.getName()) > 0) {
 			this->booleanVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
-		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+		} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
 	}
 	this->integerVariables.reserve(module.integerVariables.size());
 	for (IntegerVariable it: module.integerVariables) {
 		if (renaming.count(it.getName()) > 0) {
 			this->integerVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
-		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+		} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!");
 	}
 	
 	this->commands.reserve(module.commands.size());
@@ -67,6 +72,8 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m
 		this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
 	}
 	this->collectActions();
+
+	LOG4CPLUS_DEBUG(logger, "Finished renaming...");
 }
 
 // Return the number of boolean variables.
diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h
index de0b1d8ab..3897c0cc6 100644
--- a/src/ir/expressions/BinaryExpression.h
+++ b/src/ir/expressions/BinaryExpression.h
@@ -10,6 +10,7 @@
 
 #include "src/ir/expressions/BaseExpression.h"
 #include <memory>
+#include <iostream>
 
 namespace storm {
 
@@ -21,7 +22,11 @@ class BinaryExpression : public BaseExpression {
 public:
 	BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right)
 		: BaseExpression(type), left(left), right(right) {
-
+		if (left == nullptr || right == nullptr) {
+			std::cerr << "BinaryExpression" << std::endl;
+			if (left != nullptr) std::cerr << "\tleft: " << left->toString() << std::endl;
+			if (right != nullptr) std::cerr << "\tright: " << right->toString() << std::endl;
+		}
 	}
 
 	std::shared_ptr<BaseExpression> const& getLeft() const {
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
index f7811e3e4..e14e33d7e 100644
--- a/src/ir/expressions/VariableExpression.h
+++ b/src/ir/expressions/VariableExpression.h
@@ -26,9 +26,11 @@ public:
 			std::shared_ptr<BaseExpression> upperBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr))
 			: BaseExpression(type), index(index), variableName(variableName),
 			  lowerBound(lowerBound), upperBound(upperBound) {
+		std::cerr << "Creating " << this << std::endl;
 	}
 
 	virtual ~VariableExpression() {
+		std::cerr << "Destroying " << this << std::endl;
 	}
 
 	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 4a9678827..08f534691 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -26,7 +26,6 @@
 #include <iomanip>
 #include <limits>
 
-
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -69,7 +68,7 @@ namespace parser {
 		this->state->moduleNames_.add(name, name);
 		Module* old = this->state->moduleMap_.find(oldname);
 		if (old == nullptr) {
-			std::cerr << "Renaming module failed: module " << oldname << " does not exist!" << std::endl;
+			LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!");
 			throw "Renaming module failed";
 		}
 		Module res(*old, name, mapping, this->state);
@@ -236,7 +235,16 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type
 	}
 	
 	void PrismParser::PrismGrammar::prepareForSecondRun() {
+		LOG4CPLUS_INFO(logger, "Preparing parser for second run.");
+		this->state->getIntegerVariable("d1");
+		this->state->getIntegerVariable("d2");
+		this->state->getIntegerVariable("s1");
+		this->state->getIntegerVariable("s2");
 		this->state->prepareForSecondRun();
+		this->state->getIntegerVariable("d1");
+		this->state->getIntegerVariable("d2");
+		this->state->getIntegerVariable("s1");
+		this->state->getIntegerVariable("s2");
 		prism::BooleanExpressionGrammar::secondRun();
 		prism::ConstBooleanExpressionGrammar::secondRun();
 		prism::ConstDoubleExpressionGrammar::secondRun();
diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.cpp b/src/parser/PrismParser/BooleanExpressionGrammar.cpp
index 00ca2fe40..6a2d421bb 100644
--- a/src/parser/PrismParser/BooleanExpressionGrammar.cpp
+++ b/src/parser/PrismParser/BooleanExpressionGrammar.cpp
@@ -33,7 +33,7 @@ namespace prism {
 	}
 
 	void BooleanExpressionGrammar::prepareSecondRun() {
-		booleanVariableExpression = this->state->booleanVariables_;
+		booleanVariableExpression %= this->state->booleanVariables_;
 		booleanVariableExpression.name("boolean variable");
 	}
 
diff --git a/src/parser/PrismParser/Includes.h b/src/parser/PrismParser/Includes.h
index fe3418b2c..3bce26d00 100644
--- a/src/parser/PrismParser/Includes.h
+++ b/src/parser/PrismParser/Includes.h
@@ -33,5 +33,9 @@ typedef boost::spirit::unused_type Unused;
 using namespace storm::ir;
 using namespace storm::ir::expressions;
 
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+extern log4cplus::Logger logger;
+
 #endif	/* BOOSTINCLUDES_H */
 
diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.cpp b/src/parser/PrismParser/IntegerExpressionGrammar.cpp
index e0e363030..ba1a35eb6 100644
--- a/src/parser/PrismParser/IntegerExpressionGrammar.cpp
+++ b/src/parser/PrismParser/IntegerExpressionGrammar.cpp
@@ -27,7 +27,7 @@ namespace prism {
 	}
 
 	void IntegerExpressionGrammar::prepareSecondRun() {
-		integerVariableExpression = this->state->integerVariables_;
+		integerVariableExpression %= this->state->integerVariables_;
 		integerVariableExpression.name("integer variable");
 	}
 
diff --git a/src/parser/PrismParser/VariableState.cpp b/src/parser/PrismParser/VariableState.cpp
new file mode 100644
index 000000000..91d41be77
--- /dev/null
+++ b/src/parser/PrismParser/VariableState.cpp
@@ -0,0 +1,135 @@
+#include "VariableState.h"
+
+namespace storm {
+namespace parser {
+namespace prism {
+
+using namespace storm::ir;
+using namespace storm::ir::expressions;
+
+template<typename T>
+struct SymbolDump {
+	SymbolDump(std::ostream& out) : out(out) {}
+	void operator() (std::basic_string<char> s, T elem) {
+		this->out << "\t" << s << " -> " << elem << std::endl;
+	}
+private:
+	std::ostream& out;
+};
+template<typename T>
+std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols) {
+	out << "Dumping symbol table" << std::endl;
+	SymbolDump<T> dump(out);
+	symbols.for_each(dump);
+	return out;
+}
+
+
+VariableState::VariableState(bool firstRun)
+		: firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) {
+}
+
+uint_fast64_t VariableState::addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
+	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);
+		this->booleanVariables_.add(name, varExpr);
+		this->booleanVariableNames_.add(name, name);
+		this->nextBooleanVariableIndex++;
+		return varExpr->getVariableIndex();
+	} else {
+		std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
+		if (res != nullptr) {
+			return res->getVariableIndex();
+		} else {
+			LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " was not created in first run.");
+			return 0;
+		}
+	}
+}
+
+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, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
+	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);
+		this->integerVariables_.add(name, varExpr);
+		LOG4CPLUS_DEBUG(logger, "Int variables: " << this->integerVariables_);
+		this->integerVariables_.at(name) = varExpr;
+		LOG4CPLUS_DEBUG(logger, "Int variables: " << this->integerVariables_);
+		this->integerVariableNames_.add(name, name);
+		this->nextIntegerVariableIndex++;
+		return varExpr->getVariableIndex();
+	} else {
+		std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
+		if (res != nullptr) {
+			return res->getVariableIndex();
+		} else {
+
+			LOG4CPLUS_ERROR(logger, "Integer variable " << name << " was not created in first run.");
+			return 0;
+		}
+	}
+}
+
+std::shared_ptr<VariableExpression> VariableState::getBooleanVariable(const std::string& name) {
+	std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
+	if (res != nullptr) {
+		LOG4CPLUS_DEBUG(logger, "Getting boolean variable " << name << ", was found at " << res);
+		return res;
+	} else {
+		if (firstRun) {
+			LOG4CPLUS_DEBUG(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.");
+			return std::shared_ptr<VariableExpression>(nullptr);
+		}
+	}
+}
+
+std::shared_ptr<VariableExpression> VariableState::getIntegerVariable(const std::string& name) {
+	std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
+	if (res != nullptr) {
+		LOG4CPLUS_DEBUG(logger, "Getting integer variable " << name << ", was found at " << res);
+		return res;
+	} else {
+		if (firstRun) {
+			LOG4CPLUS_DEBUG(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.");
+			return std::shared_ptr<VariableExpression>(nullptr);
+		}
+	}
+}
+
+void VariableState::startModule() {
+	this->localBooleanVariables_.clear();
+	this->localIntegerVariables_.clear();
+}
+
+bool VariableState::isFreeIdentifier(std::string& s) const {
+	if (this->integerVariableNames_.find(s) != nullptr) return false;
+	if (this->allConstantNames_.find(s) != nullptr) return false;
+	if (this->labelNames_.find(s) != nullptr) return false;
+	if (this->moduleNames_.find(s) != nullptr) return false;
+	if (this->keywords.find(s) != nullptr) return false;
+	return true;
+}
+bool VariableState::isIdentifier(std::string& s) const {
+	if (this->allConstantNames_.find(s) != nullptr) return false;
+	if (this->keywords.find(s) != nullptr) return false;
+	return true;
+}
+
+void VariableState::prepareForSecondRun() {
+	integerConstants_.clear();
+	booleanConstants_.clear();
+	doubleConstants_.clear();
+	allConstantNames_.clear();
+	this->firstRun = false;
+}
+
+}
+}
+}
diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h
index e94d44056..6293da58b 100644
--- a/src/parser/PrismParser/VariableState.h
+++ b/src/parser/PrismParser/VariableState.h
@@ -11,6 +11,7 @@
 #include "src/ir/IR.h"
 #include "Includes.h"
 #include "Tokens.h"
+#include <iostream>
 
 namespace storm {
 namespace parser {
@@ -19,14 +20,15 @@ namespace prism {
 using namespace storm::ir;
 using namespace storm::ir::expressions;
 
+template<typename T>
+std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols);
 
 struct VariableState : public storm::ir::VariableAdder {
 
 public:
-	VariableState(bool firstRun = true)
-			: firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) {
-	}
+	VariableState(bool firstRun = true);
 
+public:
 	bool firstRun;
 	keywordsStruct keywords;
 
@@ -43,102 +45,21 @@ public:
 	// A structure representing the identity function over identifier names.
 	struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
 			localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
+public:
+	uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
+
+	uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
+
+	std::shared_ptr<VariableExpression> getBooleanVariable(const std::string& name);
+
+	std::shared_ptr<VariableExpression> getIntegerVariable(const std::string& name);
+
+	void startModule();
+
+	bool isFreeIdentifier(std::string& s) const;
+	bool isIdentifier(std::string& s) const;
 
-	uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
-		if (firstRun) {
-			std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name));
-			this->booleanVariables_.add(name, varExpr);
-			this->booleanVariableNames_.add(name, name);
-			this->nextBooleanVariableIndex++;
-			return varExpr->getVariableIndex();
-		} else {
-			std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
-			if (res != nullptr) {
-				return res->getVariableIndex();
-			} else {
-				std::cerr << "Variable " << name << " was not created in first run" << std::endl;
-				return 0;
-			}
-		}
-	}
-
-	uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
-		//std::cerr << "adding integer variable " << name << std::endl;
-		if (firstRun) {
-			std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper));
-			this->integerVariables_.add(name, varExpr);
-			this->integerVariableNames_.add(name, name);
-			this->nextIntegerVariableIndex++;
-			return varExpr->getVariableIndex();
-		} else {
-			std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
-			if (res != nullptr) {
-				return res->getVariableIndex();
-			} else {
-				std::cerr << "Variable " << name << " was not created in first run" << std::endl;
-				return 0;
-			}
-		}
-	}
-
-	std::shared_ptr<VariableExpression> getBooleanVariable(const std::string& name) {
-		std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
-		if (res != nullptr) {
-			return res;
-		} else {
-			if (firstRun) {
-				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 {
-				std::cerr << "bool Variable " << name << " was not created in first run" << std::endl;
-				return std::shared_ptr<VariableExpression>(nullptr);
-			}
-		}
-	}
-
-	std::shared_ptr<VariableExpression> getIntegerVariable(const std::string& name) {
-		//std::cerr << "getting integer variable " << name << std::endl;
-		std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
-		if (res != nullptr) {
-			return res;
-		} else {
-			if (firstRun) {
-				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 {
-				std::cerr << "int Variable " << name << " was not created in first run" << std::endl;
-				return std::shared_ptr<VariableExpression>(nullptr);
-			}
-		}
-	}
-
-	void startModule() {
-		//std::cerr << "starting new module" << std::endl;
-		this->localBooleanVariables_.clear();
-		this->localIntegerVariables_.clear();
-	}
-
-	bool isFreeIdentifier(std::string& s) const {
-		//std::cerr << "Checking if " << s << " is free" << std::endl;
-		if (this->integerVariableNames_.find(s) != nullptr) return false;
-		if (this->allConstantNames_.find(s) != nullptr) return false;
-		if (this->labelNames_.find(s) != nullptr) return false;
-		if (this->moduleNames_.find(s) != nullptr) return false;
-		if (this->keywords.find(s) != nullptr) return false;
-		return true;
-	}
-	bool isIdentifier(std::string& s) const {
-		//std::cerr << "Checking if " << s << " is identifier" << std::endl;
-		if (this->allConstantNames_.find(s) != nullptr) return false;
-		if (this->keywords.find(s) != nullptr) return false;
-		return true;
-	}
-
-	void prepareForSecondRun() {
-		integerConstants_.clear();
-		booleanConstants_.clear();
-		doubleConstants_.clear();
-		allConstantNames_.clear();
-		this->firstRun = false;
-	}
+	void prepareForSecondRun();
 };
 
 }