Started to refactor PRISM parser.

src/ir/RewardModel.cpp

@@ -5,25 +5,22 @@
  *      Author: Christian Dehnert
  */
 
-#include "RewardModel.h"
-
 #include <sstream>
 
+#include "RewardModel.h"
+
 namespace storm {
 
 namespace ir {
 
-// Initializes all members with their default constructors.
 RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() {
 	// Nothing to do here.
 }
 
-// Initializes all members according to the given values.
-RewardModel::RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
+RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
 	// Nothing to do here.
 }
 
-// Build a string representation of the reward model.
 std::string RewardModel::toString() const {
 	std::stringstream result;
 	result << "rewards \"" << rewardModelName << "\"" << std::endl;

src/ir/RewardModel.h

@@ -8,12 +8,12 @@
 #ifndef STORM_IR_REWARDMODEL_H_
 #define STORM_IR_REWARDMODEL_H_
 
-#include "StateReward.h"
-#include "TransitionReward.h"
-
 #include <string>
 #include <vector>
 
+#include "StateReward.h"
+#include "TransitionReward.h"
+
 namespace storm {
 
 namespace ir {
@@ -30,41 +30,47 @@ public:
 
 	/*!
 	 * Creates a reward module with the given name, state and transition rewards.
-	 * @param rewardModelName the name of the reward model.
-	 * @param stateRewards A vector of state-based reward.
-	 * @param transitionRewards A vector of transition-based reward.
+     *
+	 * @param rewardModelName The name of the reward model.
+	 * @param stateRewards A vector of state-based rewards.
+	 * @param transitionRewards A vector of transition-based rewards.
 	 */
-	RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards);
+	RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards);
 
 	/*!
-	 * Retrieves a string representation of this variable.
-	 * @returns a string representation of this variable.
+	 * Retrieves a string representation of this reward model.
+     *
+	 * @return a string representation of this reward model.
 	 */
 	std::string toString() const;
 
 	/*!
 	 * Check, if there are any state rewards.
+     *
 	 * @return True, iff there are any state rewards.
 	 */
 	bool hasStateRewards() const;
 
 	/*!
-	 * Retrieve state rewards.
-	 * @return State rewards.
+	 * Retrieves a vector of state rewards associated with this reward model.
+     *
+	 * @return A vector containing the state rewards associated with this reward model.
 	 */
-	std::vector<storm::ir::StateReward> getStateRewards() const;
+	std::vector<storm::ir::StateReward> const& getStateRewards() const;
 
 	/*!
 	 * Check, if there are any transition rewards.
-	 * @return True, iff there are any transition rewards.
+     *
+	 * @return True, iff there are any transition rewards associated with this reward model.
 	 */
 	bool hasTransitionRewards() const;
 
 	/*!
-	 * Retrieve transition rewards.
-	 * @return Transition rewards.
+	 * Retrieves a vector of transition rewards associated with this reward model.
+     *
+	 * @return A vector of transition rewards associated with this reward model.
 	 */
-	std::vector<storm::ir::TransitionReward> getTransitionRewards() const;
+	std::vector<storm::ir::TransitionReward> const& getTransitionRewards() const;
 
 private:
 	// The name of the reward model.

src/ir/StateReward.cpp

@@ -5,38 +5,28 @@
  *      Author: Christian Dehnert
  */
 
-#include "StateReward.h"
-
 #include <sstream>
 
+#include "StateReward.h"
+
 namespace storm {
 
 namespace ir {
 
-// Initializes all members with their default constructors.
 StateReward::StateReward() : statePredicate(), rewardValue() {
 	// Nothing to do here.
 }
 
-// Initializes all members according to the given values.
 StateReward::StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
 	// Nothing to do here.
 }
 
-// Build a string representation of the state reward.
 std::string StateReward::toString() const {
 	std::stringstream result;
 	result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
 	return result.str();
 }
 
-double StateReward::getReward(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const {
-	if (this->statePredicate->getValueAsBool(state)) {
-		return this->rewardValue->getValueAsDouble(state);
-	}
-	return 0;
-}
-
 } // namespace ir
 
 } // namespace storm

src/ir/StateReward.h

@@ -8,10 +8,10 @@
 #ifndef STORM_IR_STATEREWARD_H_
 #define STORM_IR_STATEREWARD_H_
 
-#include "expressions/BaseExpression.h"
-
 #include <memory>
 
+#include "expressions/BaseExpression.h"
+
 namespace storm {
 
 namespace ir {
@@ -29,27 +29,21 @@ public:
 	/*!
 	 * Creates a state reward for the states satisfying the given expression with the value given
 	 * by a second expression.
-	 * @param statePredicate the predicate that states earning this state-based reward need to
+     *
+	 * @param statePredicate The predicate that states earning this state-based reward need to
 	 * satisfy.
-	 * @param rewardValue an expression specifying the values of the rewards to attach to the
+	 * @param rewardValue An expression specifying the values of the rewards to attach to the
 	 * states.
 	 */
 	StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue);
 
 	/*!
 	 * Retrieves a string representation of this state reward.
-	 * @returns a string representation of this state reward.
+     *
+	 * @return A string representation of this state reward.
 	 */
 	std::string toString() const;
 
-	/*!
-	 * Returns the reward for the given state.
-	 * It the state fulfills the predicate, the reward value is returned, zero otherwise.
-	 * @param state State object.
-	 * @return Reward for given state.
-	 */
-	double getReward(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const;
-
 private:
 	// The predicate that characterizes the states that obtain this reward.
 	std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;

src/ir/TransitionReward.cpp

@@ -5,39 +5,28 @@
  *      Author: Christian Dehnert
  */
 
-#include "TransitionReward.h"
-
 #include <sstream>
 
+#include "TransitionReward.h"
+
 namespace storm {
 
 namespace ir {
 
-// Initializes all members with their default constructors.
 TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
 	// Nothing to do here.
 }
 
-// Initializes all members according to the given values.
-TransitionReward::TransitionReward(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
+TransitionReward::TransitionReward(std::string const& commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
 	// Nothing to do here.
 }
 
-// Build a string representation of the transition reward.
 std::string TransitionReward::toString() const {
 	std::stringstream result;
 	result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
 	return result.str();
 }
 
-double TransitionReward::getReward(std::string const & label, std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const {
-	if (this->commandName != label) return 0;
-	if (this->statePredicate->getValueAsBool(state)) {
-		return this->rewardValue->getValueAsDouble(state);
-	}
-	return 0;
-}
-
 } // namespace ir
 
 } // namespace storm

src/ir/TransitionReward.h

@@ -8,10 +8,10 @@
 #ifndef STORM_IR_TRANSITIONREWARD_H_
 #define STORM_IR_TRANSITIONREWARD_H_
 
-#include "expressions/BaseExpression.h"
-
 #include <memory>
 
+#include "expressions/BaseExpression.h"
+
 namespace storm {
 
 namespace ir {
@@ -29,26 +29,22 @@ public:
 	/*!
 	 * Creates a transition reward for the transitions with the given name emanating from states
 	 * satisfying the given expression with the value given by another expression.
-	 * @param commandName the name of the command that obtains this reward.
-	 * @param statePredicate the predicate that needs to hold before taking a transition with the
+     *
+	 * @param commandName The name of the command that obtains this reward.
+	 * @param statePredicate The predicate that needs to hold before taking a transition with the
 	 * previously specified name in order to obtain the reward.
-	 * @param rewardValue an expression specifying the values of the rewards to attach to the
+	 * @param rewardValue An expression specifying the values of the rewards to attach to the
 	 * transitions.
 	 */
-	TransitionReward(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue);
+	TransitionReward(std::string const& commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue);
 
 	/*!
 	 * Retrieves a string representation of this transition reward.
-	 * @returns a string representation of this transition reward.
+     *
+	 * @return A string representation of this transition reward.
 	 */
 	std::string toString() const;
 
-	/*!
-	 * Retrieves reward for given transition.
-	 * Returns reward value if source state fulfills predicate and the transition is labeled correctly, zero otherwise.
-	 */
-	double getReward(std::string const & label, std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const;
-
 private:
 	// The name of the command this transition-based reward is attached to.
 	std::string commandName;

src/ir/Update.cpp

@@ -5,51 +5,47 @@
  *      Author: Christian Dehnert
  */
 
-#include "Update.h"
+#include <sstream>
 
+#include "Update.h"
 #include "src/exceptions/OutOfRangeException.h"
 
-#include <sstream>
-
 namespace storm {
 
 namespace ir {
 
-// Initializes all members with their default constructors.
+
 Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() {
 	// Nothing to do here.
 }
 
-// Initializes all members according to the given values.
 Update::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)
 	: likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) {
 	// 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) {
+Update::Update(Update const& update, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap) {
 	for (auto it : update.booleanAssignments) {
 		if (renaming.count(it.first) > 0) {
-			this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints);
+			this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
 		} else {
-			this->booleanAssignments[it.first] = Assignment(it.second, renaming, bools, ints);
+			this->booleanAssignments[it.first] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
 		}
 	}
 	for (auto it : update.integerAssignments) {
 		if (renaming.count(it.first) > 0) {
-			this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints);
+			this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
 		} else {
-			this->integerAssignments[it.first] = Assignment(it.second, renaming, bools, ints);
+			this->integerAssignments[it.first] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
 		}
 	}
-	this->likelihoodExpression = update.likelihoodExpression->clone(renaming, bools, ints);
+	this->likelihoodExpression = update.likelihoodExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
 }
 
-// Return the expression for the likelihood of the update.
 std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
 	return likelihoodExpression;
 }
 
-// Return the number of assignments.
 uint_fast64_t Update::getNumberOfBooleanAssignments() const {
 	return booleanAssignments.size();
 }
@@ -58,17 +54,14 @@ uint_fast64_t Update::getNumberOfIntegerAssignments() const {
 	return integerAssignments.size();
 }
 
-// Return the boolean variable name to assignment map.
 std::map<std::string, storm::ir::Assignment> const& Update::getBooleanAssignments() const {
 	return booleanAssignments;
 }
 
-// Return the integer variable name to assignment map.
 std::map<std::string, storm::ir::Assignment> const& Update::getIntegerAssignments() const {
 	return integerAssignments;
 }
 
-// Return the assignment for the boolean variable if it exists and throw an exception otherwise.
 storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableName) const {
 	auto it = booleanAssignments.find(variableName);
 	if (it == booleanAssignments.end()) {
@@ -79,7 +72,6 @@ storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableNa
 	return (*it).second;
 }
 
-// Return the assignment for the boolean variable if it exists and throw an exception otherwise.
 storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableName) const {
 	auto it = integerAssignments.find(variableName);
 	if (it == integerAssignments.end()) {
@@ -90,7 +82,6 @@ storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableNa
 	return (*it).second;
 }
 
-// Build a string representation of the update.
 std::string Update::toString() const {
 	std::stringstream result;
 	result << likelihoodExpression->toString() << " : ";

src/ir/Update.h

@@ -8,12 +8,12 @@
 #ifndef STORM_IR_UPDATE_H_
 #define STORM_IR_UPDATE_H_
 
-#include "expressions/BaseExpression.h"
-#include "Assignment.h"
-
 #include <map>
 #include <memory>
 
+#include "expressions/BaseExpression.h"
+#include "Assignment.h"
+
 namespace storm {
 
 namespace ir {
@@ -31,58 +31,76 @@ public:
 	/*!
 	 * Creates an update with the given expression specifying the likelihood and the mapping of
 	 * variable to their assignments.
-	 * @param likelihoodExpression an expression specifying the likelihood of this update.
-	 * @param assignments a map of variable names to their assignments.
+     *
+	 * @param likelihoodExpression An expression specifying the likelihood of this update.
+	 * @param assignments A map of variable names to their assignments.
 	 */
 	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);
+    /*!
+     * Creates a copy of the given update and performs the provided renaming.
+     *
+     * update The update that is to be copied.
+     * renaming A mapping from names that are to be renamed to the names they are to be
+     * replaced with.
+     * @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
+     * @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
+     */
+	Update(Update const& update, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap);
 
 	/*!
 	 * Retrieves the expression for the likelihood of this update.
-	 * @returns the expression for the likelihood of this update.
+     *
+	 * @return The expression for the likelihood of this update.
 	 */
 	std::shared_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
 
 	/*!
 	 * Retrieves the number of boolean assignments associated with this update.
-	 * @returns the number of boolean assignments associated with this update.
+     *
+	 * @return The number of boolean assignments associated with this update.
 	 */
 	uint_fast64_t getNumberOfBooleanAssignments() const;
 
 	/*!
 	 * Retrieves the number of integer assignments associated with this update.
-	 * @returns the number of integer assignments associated with this update.
+     *
+	 * @return The number of integer assignments associated with this update.
 	 */
 	uint_fast64_t getNumberOfIntegerAssignments() const;
 
 	/*!
 	 * Retrieves a reference to the map of boolean variable names to their respective assignments.
-	 * @returns a reference to the map of boolean variable names to their respective assignments.
+     *
+	 * @return A reference to the map of boolean variable names to their respective assignments.
 	 */
 	std::map<std::string, storm::ir::Assignment> const& getBooleanAssignments() const;
 
 	/*!
 	 * Retrieves a reference to the map of integer variable names to their respective assignments.
-	 * @returns a reference to the map of integer variable names to their respective assignments.
+     *
+	 * @return A reference to the map of integer variable names to their respective assignments.
 	 */
 	std::map<std::string, storm::ir::Assignment> const& getIntegerAssignments() const;
 
 	/*!
 	 * Retrieves a reference to the assignment for the boolean variable with the given name.
-	 * @returns a reference to the assignment for the boolean variable with the given name.
+     *
+	 * @return A reference to the assignment for the boolean variable with the given name.
 	 */
 	storm::ir::Assignment const& getBooleanAssignment(std::string variableName) const;
 
 	/*!
 	 * Retrieves a reference to the assignment for the integer variable with the given name.
-	 * @returns a reference to the assignment for the integer variable with the given name.
+     *
+	 * @return A reference to the assignment for the integer variable with the given name.
 	 */
 	storm::ir::Assignment const& getIntegerAssignment(std::string variableName) const;
 
 	/*!
 	 * Retrieves a string representation of this update.
-	 * @returns a string representation of this update.
+     *
+	 * @return A string representation of this update.
 	 */
 	std::string toString() const;
 
@@ -101,4 +119,4 @@ private:
 
 } // namespace storm
 
-#endif /*STORM_IR_UPDATE_H_ */
+#endif /* STORM_IR_UPDATE_H_ */

src/ir/Variable.cpp

@@ -5,54 +5,52 @@
  *      Author: Christian Dehnert
  */
 
-#include "Variable.h"
-
 #include <sstream>
 #include <map>
 #include <iostream>
 
+#include "Variable.h"
+
 namespace storm {
 
 namespace ir {
 
-// Initializes all members with their default constructors.
-Variable::Variable() : index(0), variableName(), initialValue() {
+Variable::Variable() : globalIndex(0), localIndex(0), variableName(), initialValue() {
 	// Nothing to do here.
 }
 
-// Initializes all members according to the given values.
-Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : index(index), variableName(variableName), initialValue(initialValue) {
+Variable::Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
+    : globalIndex(globalIndex), localIndex(localIndex), variableName(variableName), initialValue(initialValue) {
 	// Nothing to do here.
 }
 
-Variable::Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, 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) {
-	this->index = newIndex;
-	this->variableName = newName;
+Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t const newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap)
+    : globalIndex(newGlobalIndex), localIndex(var.getLocalIndex()), variableName(var.getName()) {
 	if (var.initialValue != nullptr) {
-		this->initialValue = var.initialValue->clone(renaming, bools, ints);
+		this->initialValue = var.initialValue->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
 	}
 }
 
-// Return the name of the variable.
 std::string const& Variable::getName() const {
 	return variableName;
 }
 
-uint_fast64_t Variable::getIndex() const {
-	return index;
+uint_fast64_t Variable::getGlobalIndex() const {
+	return globalIndex;
+}
+    
+uint_fast64_t Variable::getLocalIndex() const {
+    return localIndex;
 }
 
-// Return the expression for the initial value of the variable.
 std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
 	return initialValue;
 }
 
-// Set the initial value expression to the one provided.
 void Variable::setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue) {
 	this->initialValue = initialValue;
 }
 
-
 } // namespace ir
 
 } // namespace storm

src/ir/Variable.h

@@ -8,11 +8,11 @@
 #ifndef STORM_IR_VARIABLE_H_
 #define STORM_IR_VARIABLE_H_
 
-#include "expressions/BaseExpression.h"
-
 #include <string>
 #include <memory>
 
+#include "expressions/BaseExpression.h"
+
 namespace storm {
 
 namespace ir {
@@ -29,46 +29,69 @@ public:
 
 	/*!
 	 * Creates an untyped variable with the given name and initial value.
+     *
 	 * @param index A unique (among the variables of equal type) index for the variable.
 	 * @param variableName the name of the variable.
 	 * @param initialValue the expression that defines the initial value of the variable.
 	 */
-	Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+	Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, 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.
+	 * Creates a copy of the given Variable and performs the provided renaming.
+     *
+	 * @param oldVariable The variable to copy.
 	 * @param newName New name of this variable.
+     * @param newGlobalIndex The new global index of the variable.
+     * @param renaming A mapping from names that are to be renamed to the names they are to be
+     * replaced with.
+     * @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
+     * @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
 	 */
-	Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, 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);
+	Variable(const Variable& oldVariable, const std::string& newName, const uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap);
 
 	/*!
 	 * Retrieves the name of the variable.
-	 * @returns the name of the variable.
+     *
+	 * @return The name of the variable.
 	 */
 	std::string const& getName() const;
 
 	/*!
-	 * Retrieves the index of the variable.
-	 * @returns the index of the variable.
+	 * Retrieves the global index of the variable, i.e. the index in all variables of equal type
+     * of all modules.
+     *
+	 * @return The global index of the variable.
 	 */
-	uint_fast64_t getIndex() const;
+	uint_fast64_t getGlobalIndex() const;
+    
+    /*!
+     * Retrieves the global index of the variable, i.e. the index in all variables of equal type in
+     * the same module.
+     *
+     * @return The local index of the variable.
+     */
+    uint_fast64_t getLocalIndex() const;
 
 	/*!
 	 * Retrieves the expression defining the initial value of the variable.
-	 * @returns the expression defining the initial value of the variable.
+     *
+	 * @return The expression defining the initial value of the variable.
 	 */
 	std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
 
 	/*!
 	 * Sets the initial value to the given expression.
-	 * @param initialValue the new initial value.
+     *
+	 * @param initialValue The new initial value.
 	 */
 	void setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue);
 
 private:
-	// A unique (among the variables of equal type) index for the variable
-	uint_fast64_t index;
+	// A unique (among the variables of equal type) index for the variable over all modules.
+	uint_fast64_t globalIndex;
+    
+    // A unique (among the variables of equal type) index for the variable inside its module.
+    uint_fast64_t localIndex;
 
 	// The name of the variable.
 	std::string variableName;