From e55fca38364f7046f9c2572f80ad8cf3556deb55 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 26 Mar 2013 18:59:05 +0100
Subject: [PATCH] Implemented module renaming.

This includes clone() routines (that accept the renaming information) for all ir::expressions classes, additional constructors for all ir classes and additional rules in PrismParser.

This is the first version that has the chance to work and actually compiles. (Insert some swearing here...)
Testing is to be done, as this will most probably not work yet.
---
 src/ir/Assignment.cpp                         |  7 +++
 src/ir/Assignment.h                           |  2 +
 src/ir/BooleanVariable.cpp                    |  3 ++
 src/ir/BooleanVariable.h                      |  8 +--
 src/ir/Command.cpp                            | 13 ++++-
 src/ir/Command.h                              |  4 +-
 src/ir/IntegerVariable.cpp                    |  3 ++
 src/ir/IntegerVariable.h                      |  4 +-
 src/ir/Module.cpp                             | 53 +++++++++++++++----
 src/ir/Module.h                               | 22 +++++++-
 src/ir/Update.cpp                             | 18 +++++++
 src/ir/Update.h                               |  2 +
 src/ir/Variable.cpp                           |  5 ++
 src/ir/Variable.h                             |  7 +++
 src/ir/expressions/BaseExpression.h           |  6 ++-
 .../BinaryBooleanFunctionExpression.h         |  4 ++
 src/ir/expressions/BinaryExpression.h         |  5 +-
 .../BinaryNumericalFunctionExpression.h       |  4 ++
 src/ir/expressions/BinaryRelationExpression.h |  4 ++
 .../expressions/BooleanConstantExpression.h   |  4 ++
 src/ir/expressions/BooleanLiteral.h           |  6 ++-
 src/ir/expressions/DoubleConstantExpression.h |  4 ++
 src/ir/expressions/DoubleLiteral.h            |  4 ++
 .../expressions/IntegerConstantExpression.h   |  4 ++
 src/ir/expressions/IntegerLiteral.h           |  6 ++-
 .../UnaryBooleanFunctionExpression.h          |  4 ++
 .../UnaryNumericalFunctionExpression.h        |  4 ++
 src/ir/expressions/VariableExpression.h       | 17 ++++++
 src/parser/PrismParser.cpp                    | 46 +++++++++++++++-
 src/parser/PrismParser.h                      |  1 +
 30 files changed, 248 insertions(+), 26 deletions(-)

diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp
index 095a922f3..232472857 100644
--- a/src/ir/Assignment.cpp
+++ b/src/ir/Assignment.cpp
@@ -24,6 +24,13 @@ Assignment::Assignment(std::string variableName, std::shared_ptr<storm::ir::expr
 	// Nothing to do here.
 }
 
+Assignment::Assignment(const Assignment& assignment, 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)
+	: variableName(assignment.variableName), expression(assignment.expression->clone(renaming, bools, ints)) {
+	if (renaming.count(assignment.variableName) > 0) {
+		this->variableName = renaming.at(assignment.variableName);
+	}
+}
+
 // Returns the name of the variable associated with this assignment.
 std::string const& Assignment::getVariableName() const {
 	return variableName;
diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h
index 019cc55eb..b17693bf0 100644
--- a/src/ir/Assignment.h
+++ b/src/ir/Assignment.h
@@ -33,6 +33,8 @@ public:
 	 */
 	Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression);
 
+	Assignment(const Assignment& assignment, 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);
+
 	/*!
 	 * Retrieves the name of the variable that this assignment targets.
 	 * @returns the name of the variable that this assignment targets.
diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp
index b867a1aa1..4ef83a879 100644
--- a/src/ir/BooleanVariable.cpp
+++ b/src/ir/BooleanVariable.cpp
@@ -25,6 +25,9 @@ BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName,
 	// Nothing to do here.
 }
 
+BooleanVariable::BooleanVariable(const BooleanVariable& var, const std::string& newName) : Variable(var, newName) {
+}
+
 // Build a string representation of the variable.
 std::string BooleanVariable::toString() const {
 	std::stringstream result;
diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h
index 9c5ba17c0..fcf5ce602 100644
--- a/src/ir/BooleanVariable.h
+++ b/src/ir/BooleanVariable.h
@@ -8,10 +8,9 @@
 #ifndef STORM_IR_BOOLEANVARIABLE_H_
 #define STORM_IR_BOOLEANVARIABLE_H_
 
-#include "expressions/BooleanLiteral.h"
-
-#include "Variable.h"
+#include "src/ir/Variable.h"
 #include <memory>
+#include <map>
 
 namespace storm {
 
@@ -35,6 +34,9 @@ public:
 	 */
 	BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
 
+
+	BooleanVariable(const BooleanVariable& var, const std::string& newName);
+
 	/*!
 	 * Retrieves a string representation of this variable.
 	 * @returns a string representation of this variable.
diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp
index bec67d4bf..b34ab60ed 100644
--- a/src/ir/Command.cpp
+++ b/src/ir/Command.cpp
@@ -20,10 +20,21 @@ Command::Command() : actionName(), guardExpression(), updates() {
 
 // Initializes all members according to the given values.
 Command::Command(std::string actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates)
-		: actionName(actionName), guardExpression(guardExpression), updates(updates) {
+	: actionName(actionName), guardExpression(guardExpression), updates(updates) {
 	// Nothing to do here.
 }
 
+Command::Command(const Command& cmd, 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)
+	: actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) {
+	if (renaming.count(this->actionName) > 0) {
+		this->actionName = renaming.at(this->actionName);
+	}
+	this->updates.reserve(cmd.updates.size());
+	for (Update u : cmd.updates) {
+		this->updates.emplace_back(u, renaming, bools, ints);
+	}
+}
+
 // Return the action name.
 std::string const& Command::getActionName() const {
 	return this->actionName;
diff --git a/src/ir/Command.h b/src/ir/Command.h
index 9207c76f0..b4049307c 100644
--- a/src/ir/Command.h
+++ b/src/ir/Command.h
@@ -13,6 +13,7 @@
 
 #include <vector>
 #include <string>
+#include <map>
 
 namespace storm {
 
@@ -34,7 +35,8 @@ public:
 	 * @param guardExpression the expression that defines the guard of the command.
 	 */
 	Command(std::string actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates);
-	
+
+	Command(const Command& cmd, 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);
 	/*!
 	 * Retrieves the action name of this command.
 	 * @returns the action name of this command.
diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp
index b07316b65..d96b2221b 100644
--- a/src/ir/IntegerVariable.cpp
+++ b/src/ir/IntegerVariable.cpp
@@ -27,6 +27,9 @@ IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName,
 	}
 }
 
+IntegerVariable::IntegerVariable(const IntegerVariable& var, const std::string& newName) : Variable(var, newName) {
+}
+
 // Return lower bound for variable.
 std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
 	return this->lowerBound;
diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h
index a05ef1d7e..a31ece3e5 100644
--- a/src/ir/IntegerVariable.h
+++ b/src/ir/IntegerVariable.h
@@ -9,7 +9,7 @@
 #define STORM_IR_INTEGERVARIABLE_H_
 
 #include "expressions/BaseExpression.h"
-#include "Variable.h"
+#include "src/ir/Variable.h"
 #include <memory>
 
 namespace storm {
@@ -37,6 +37,8 @@ public:
 	 */
 	IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
 
+	IntegerVariable(const IntegerVariable& var, const std::string& newName);
+	
 	/*!
 	 * Retrieves the lower bound for this integer variable.
 	 * @returns the lower bound for this integer variable.
diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp
index 9a2337f8a..dcacfe198 100644
--- a/src/ir/Module.cpp
+++ b/src/ir/Module.cpp
@@ -10,6 +10,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 
 #include <sstream>
+#include <iostream>
 
 namespace storm {
 
@@ -30,17 +31,34 @@ Module::Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> b
 	: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables),
 	  booleanVariablesToIndexMap(booleanVariableToIndexMap),
 	  integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands), actions(), actionsToCommandIndexMap() {
-	// Build actionsToCommandIndexMap
-	for (unsigned int id = 0; id < this->commands.size(); id++) {
-		std::string action = this->commands[id].getActionName();
-		if (action != "") {
-			if (this->actionsToCommandIndexMap.count(action) == 0) {
-				this->actionsToCommandIndexMap[action] = std::shared_ptr<std::set<uint_fast64_t>>(new std::set<uint_fast64_t>());
-			}
-			this->actionsToCommandIndexMap[action]->insert(id);
-			this->actions.insert(action);
-		}
-	}  
+	this->collectActions();
+}
+
+Module::Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, const VariableAdder& adder)
+	: moduleName(moduleName) {
+	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()));
+			//this->booleanVariablesToIndexMap[renaming.at(it.getName())] = (*boolAdder)(it.getName(), it.getInitialValue());
+			this->booleanVariablesToIndexMap[renaming.at(it.getName())] = adder.addBooleanVariable(it.getName(), it.getInitialValue());
+		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+	}
+	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()));
+			//this->integerVariablesToIndexMap[renaming.at(it.getName())] = (*intAdder)(it.getName(), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
+			this->integerVariablesToIndexMap[renaming.at(it.getName())] = adder.addIntegerVariable(it.getName(), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
+		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+	}
+	
+	this->commands.reserve(module.commands.size());
+	for (Command cmd: module.commands) {
+		this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
+	}
+
+	this->collectActions();
 }
 
 // Return the number of boolean variables.
@@ -125,6 +143,19 @@ std::shared_ptr<std::set<uint_fast64_t>> const Module::getCommandsByAction(std::
 	}
 }
 
+void Module::collectActions() {
+	for (unsigned int id = 0; id < this->commands.size(); id++) {
+		std::string action = this->commands[id].getActionName();
+		if (action != "") {
+			if (this->actionsToCommandIndexMap.count(action) == 0) {
+				this->actionsToCommandIndexMap[action] = std::shared_ptr<std::set<uint_fast64_t>>(new std::set<uint_fast64_t>());
+			}
+			this->actionsToCommandIndexMap[action]->insert(id);
+			this->actions.insert(action);
+		}
+	}
+}
+
 } // namespace ir
 
 } // namespace storm
diff --git a/src/ir/Module.h b/src/ir/Module.h
index 4070846f5..8991062ec 100644
--- a/src/ir/Module.h
+++ b/src/ir/Module.h
@@ -22,6 +22,11 @@ namespace storm {
 
 namespace ir {
 
+	struct VariableAdder {
+		virtual 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) const = 0;
+		virtual uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const = 0;
+	};
+
 /*!
  * A class representing a module.
  */
@@ -45,6 +50,18 @@ public:
 			std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
 			std::vector<storm::ir::Command> commands);
 
+	typedef uint_fast64_t (*addIntegerVariablePtr)(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);
+	typedef uint_fast64_t (*addBooleanVariablePtr)(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
+	
+	/*!
+	 * Special copy constructor, implementing the module renaming functionality.
+	 * This will create a new module having all identifier renamed according to the given map.
+	 * @param module Module to be copied.
+	 * @param moduleName Name of the new module.
+	 * @param renaming Renaming map.
+	 */
+	Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, const VariableAdder& adder);
+
 	/*!
 	 * Retrieves the number of boolean variables in the module.
 	 * @returns the number of boolean variables in the module.
@@ -116,6 +133,9 @@ public:
 	std::shared_ptr<std::set<uint_fast64_t>> const getCommandsByAction(std::string const& action) const;
 
 private:
+
+	void collectActions();
+
 	// The name of the module.
 	std::string moduleName;
 
@@ -137,7 +157,7 @@ private:
 	// The set of actions present in this module.
 	std::set<std::string> actions;
 	
-	// A map of actions to the set of commands labelled with this action.
+	// A map of actions to the set of commands labeled with this action.
 	std::map<std::string, std::shared_ptr<std::set<uint_fast64_t>>> actionsToCommandIndexMap;
 };
 
diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp
index edacb6fe9..2d0dc5d2a 100644
--- a/src/ir/Update.cpp
+++ b/src/ir/Update.cpp
@@ -26,6 +26,24 @@ Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoo
 	// Nothing to do here.
 }
 
+Update::Update(const Update& update, 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) {
+	for (auto it : update.booleanAssignments) {
+		if (renaming.count(it.first) > 0) {
+			this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints);
+		} else {
+			this->booleanAssignments[it.first] = Assignment(it.second, renaming, bools, ints);
+		}
+	}
+	for (auto it : update.integerAssignments) {
+		if (renaming.count(it.first) > 0) {
+			this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints);
+		} else {
+			this->integerAssignments[it.first] = Assignment(it.second, renaming, bools, ints);
+		}
+	}
+	this->likelihoodExpression = update.likelihoodExpression->clone(renaming, bools, ints);
+}
+
 // Return the expression for the likelihood of the update.
 std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
 	return likelihoodExpression;
diff --git a/src/ir/Update.h b/src/ir/Update.h
index 54ddc5cd8..4ce6a2fbf 100644
--- a/src/ir/Update.h
+++ b/src/ir/Update.h
@@ -36,6 +36,8 @@ public:
 	 */
 	Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> booleanAssignments, std::map<std::string, storm::ir::Assignment> integerAssignments);
 
+	Update(const Update& update, 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);
+
 	/*!
 	 * Retrieves the expression for the likelihood of this update.
 	 * @returns the expression for the likelihood of this update.
diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp
index 19d7f211f..caef3aad0 100644
--- a/src/ir/Variable.cpp
+++ b/src/ir/Variable.cpp
@@ -8,6 +8,7 @@
 #include "Variable.h"
 
 #include <sstream>
+#include <map>
 
 namespace storm {
 
@@ -23,6 +24,10 @@ Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_pt
 	// Nothing to do here.
 }
 
+Variable::Variable(const Variable& var, const std::string& newName) : Variable(var.index, newName, var.initialValue) {
+	// Nothing to do here
+}
+
 // Return the name of the variable.
 std::string const& Variable::getName() const {
 	return variableName;
diff --git a/src/ir/Variable.h b/src/ir/Variable.h
index 6f31280e2..2348346c3 100644
--- a/src/ir/Variable.h
+++ b/src/ir/Variable.h
@@ -35,6 +35,13 @@ public:
 	 */
 	Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
 
+	/*!
+	 * Creates a copy of the given Variable and gives it a new name.
+	 * @param var Variable to copy.
+	 * @param newName New name of this variable.
+	 */
+	Variable(const Variable& var, const std::string& newName);
+
 	/*!
 	 * Retrieves the name of the variable.
 	 * @returns the name of the variable.
diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h
index 3f93607ba..563037266 100644
--- a/src/ir/expressions/BaseExpression.h
+++ b/src/ir/expressions/BaseExpression.h
@@ -15,11 +15,11 @@
 
 #include <string>
 #include <vector>
+#include <map>
+#include <memory>
 
 namespace storm {
-
 namespace ir {
-
 namespace expressions {
 
 class BaseExpression {
@@ -39,6 +39,8 @@ public:
 
 	}
 
+	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) = 0;
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (type != int_) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h
index 85c927c60..dc1dc1147 100644
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h
@@ -31,6 +31,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		bool resultLeft = this->getLeft()->getValueAsBool(variableValues);
 		bool resultRight = this->getRight()->getValueAsBool(variableValues);
diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h
index c5b4ba9f5..de0b1d8ab 100644
--- a/src/ir/expressions/BinaryExpression.h
+++ b/src/ir/expressions/BinaryExpression.h
@@ -8,7 +8,7 @@
 #ifndef STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_
 #define STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_
 
-#include "BaseExpression.h"
+#include "src/ir/expressions/BaseExpression.h"
 #include <memory>
 
 namespace storm {
@@ -19,7 +19,8 @@ namespace expressions {
 
 class BinaryExpression : public BaseExpression {
 public:
-	BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) : BaseExpression(type), left(left), right(right) {
+	BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right)
+		: BaseExpression(type), left(left), right(right) {
 
 	}
 
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h
index 153f4331d..49d2c9494 100644
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h
@@ -24,6 +24,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	virtual ~BinaryNumericalFunctionExpression() {
 
 	}
diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h
index 1a60cd34d..38a09b179 100644
--- a/src/ir/expressions/BinaryRelationExpression.h
+++ b/src/ir/expressions/BinaryRelationExpression.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType));
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues);
 		int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues);
diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h
index 858fe0c12..15dcd9d4b 100644
--- a/src/ir/expressions/BooleanConstantExpression.h
+++ b/src/ir/expressions/BooleanConstantExpression.h
@@ -29,6 +29,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h
index 04f40285f..696deb787 100644
--- a/src/ir/expressions/BooleanLiteral.h
+++ b/src/ir/expressions/BooleanLiteral.h
@@ -11,9 +11,7 @@
 #include "src/ir/expressions/BaseExpression.h"
 
 namespace storm {
-
 namespace ir {
-
 namespace expressions {
 
 class BooleanLiteral : public BaseExpression {
@@ -28,6 +26,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h
index a027afa17..a0c31efbe 100644
--- a/src/ir/expressions/DoubleConstantExpression.h
+++ b/src/ir/expressions/DoubleConstantExpression.h
@@ -26,6 +26,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h
index 72c464100..efa0d1bb5 100644
--- a/src/ir/expressions/DoubleLiteral.h
+++ b/src/ir/expressions/DoubleLiteral.h
@@ -30,6 +30,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h
index 8c58260f6..01d8f2d71 100644
--- a/src/ir/expressions/IntegerConstantExpression.h
+++ b/src/ir/expressions/IntegerConstantExpression.h
@@ -26,6 +26,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h
index a5130bd5e..8911f640a 100644
--- a/src/ir/expressions/IntegerLiteral.h
+++ b/src/ir/expressions/IntegerLiteral.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
@@ -35,7 +39,7 @@ public:
 	virtual void accept(ExpressionVisitor* visitor) {
 		visitor->visit(this);
 	}
-
+	
 	virtual std::string toString() const {
 		return boost::lexical_cast<std::string>(value);
 	}
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h
index 26b448548..73b9969a7 100644
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	FunctionType getFunctionType() const {
 		return functionType;
 	}
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h
index 2a1f02125..0556892f2 100644
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	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) {
+		return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != int_) {
 			BaseExpression::getValueAsInt(variableValues);
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
index 1b9dfd46b..bbdb11ea6 100644
--- a/src/ir/expressions/VariableExpression.h
+++ b/src/ir/expressions/VariableExpression.h
@@ -33,6 +33,23 @@ public:
 
 	}
 
+	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) {
+		if (renaming.count(this->variableName) > 0) {
+			std::string newName = renaming.at(this->variableName);
+			if (this->getType() == bool_) {
+				return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, bools.at(newName), newName, this->lowerBound, this->upperBound));
+			} else if (this->getType() == int_) {
+				return std::shared_ptr<BaseExpression>(new VariableExpression(int_, ints.at(newName), newName, this->lowerBound, this->upperBound));
+			} else {
+				std::cerr << "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int." << std::endl;
+				return std::shared_ptr<BaseExpression>(this);
+			}
+		} else {
+			return std::shared_ptr<BaseExpression>(this);
+		}
+	}
+
+
 	virtual void accept(ExpressionVisitor* visitor) {
 		visitor->visit(this);
 	}
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index e9bd368eb..948f32ad6 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -222,8 +222,28 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 		variableDefinition.name("variable declaration");
 
 		// This block defines all entities that are needed for parsing a module.
-		moduleDefinition = (qi::lit("module")[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct<Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
+		moduleDefinition = (qi::lit("module")
+				[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))]
+				>> freeIdentifierName >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) > +commandDefinition > qi::lit("endmodule"))
+				[
+					phoenix::bind(moduleNames_.add, qi::_1, qi::_1),
+					qi::_val = phoenix::construct<Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2),
+					phoenix::bind(moduleMap_.add, qi::_1, qi::_val)
+				];
+
+		Module const * (qi::symbols<char, Module>::*moduleFinder)(const std::string&) const = &qi::symbols<char, Module>::find;
 		moduleDefinition.name("module");
+		moduleRenaming = (qi::lit("module")
+				[phoenix::clear(phoenix::ref(localRenamings_))]
+				>> freeIdentifierName >> qi::lit("=") > moduleNames_ > qi::lit("[") > *(
+						(identifierName > qi::lit("=") > identifierName)[phoenix::insert(phoenix::ref(localRenamings_), phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
+				) > qi::lit("]") > qi::lit("endmodule"))
+				[
+					phoenix::bind(moduleNames_.add, qi::_1, qi::_1),
+					qi::_val = phoenix::construct<Module>(*phoenix::bind(moduleFinder, moduleMap_, qi::_2), qi::_1, localRenamings_, VariableAdder(this)),
+					phoenix::bind(moduleMap_.add, qi::_1, qi::_val)
+
+				];
 		moduleDefinitionList %= +moduleDefinition;
 		moduleDefinitionList.name("module list");
 
@@ -268,6 +288,26 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 		if (keywords_.find(s) != nullptr) return false;
 		return true;
 	}
+
+	struct VariableAdder : public storm::ir::VariableAdder{
+		VariableAdder(PrismGrammar* grammar) : grammar(grammar) {};
+		PrismGrammar* grammar;
+		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) const {
+			std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, grammar->nextIntegerVariableIndex, name, lower, upper));
+			grammar->integerVariables_.add(name, varExpr);
+			grammar->integerVariableNames_.add(name, name);
+			grammar->nextIntegerVariableIndex++;
+			return grammar->nextIntegerVariableIndex-1;
+		}
+
+		uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const {
+			std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, grammar->nextBooleanVariableIndex, name));
+			grammar->integerVariables_.add(name, varExpr);
+			grammar->integerVariableNames_.add(name, name);
+			grammar->nextBooleanVariableIndex++;
+			return grammar->nextBooleanVariableIndex-1;
+		}
+	};
 	
 	void prepareForSecondRun() {
 		// Clear constants.
@@ -317,6 +357,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 
 	// Rules for module definition.
 	qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
+	qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleRenaming;
 
 	// Rules for variable definitions.
 	qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
@@ -469,6 +510,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 	// the intermediate representation.
 	struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerVariables_, booleanVariables_;
 	struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
+	struct qi::symbols<char, Module> moduleMap_;
+
+	std::map<std::string, std::string> localRenamings_;
 
 	// A structure representing the identity function over identifier names.
 	struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index f4a563e37..1fca04c55 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -13,6 +13,7 @@
 
 // Used for file input.
 #include <istream>
+#include <memory>
 
 namespace storm {