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

@@ -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;

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.

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;

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.

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;

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.

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;

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.

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

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

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;

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.

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;

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.

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 '"

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

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) {
 
 	}
 

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

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

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: "

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

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: "

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

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: "

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

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

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

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

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_,

src/parser/PrismParser.h

@@ -13,6 +13,7 @@
 
 // Used for file input.
 #include <istream>
+#include <memory>
 
 namespace storm {