Further refactoring of IR and PRISM parser.

src/ir/Module.cpp

@@ -38,7 +38,7 @@ Module::Module(std::string const& moduleName,
 	this->collectActions();
 }
 
-Module::Module(Module const& oldModule, std::string const& newModuleName, 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, std::shared_ptr<VariableAdder> const& adder)
+Module::Module(Module const& oldModule, std::string const& newModuleName, 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, std::shared_ptr<VariableStateInterface> const& variableState)
 	: moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) {
 	LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << ".");
 
@@ -51,8 +51,8 @@ Module::Module(Module const& oldModule, std::string const& newModuleName, std::m
             LOG4CPLUS_ERROR(logger, "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed.");
             throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed.";
         } else {
-            this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, adder->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
-            adder->addBooleanVariable(renamingPair->second);
+            this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, variableState->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
+            variableState->addBooleanVariable(renamingPair->second);
         }
     }
     // Now do the same for the integer variables.
@@ -63,8 +63,8 @@ Module::Module(Module const& oldModule, std::string const& newModuleName, std::m
             LOG4CPLUS_ERROR(logger, "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed.");
             throw storm::exceptions::InvalidArgumentException() << "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed.";
         } else {
-            this->integerVariables.emplace_back(integerVariable, renamingPair->second, adder->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
-            adder->addIntegerVariable(renamingPair->second);
+            this->integerVariables.emplace_back(integerVariable, renamingPair->second, variableState->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
+            variableState->addIntegerVariable(renamingPair->second);
         }
     }
 

src/ir/Module.h

@@ -14,43 +14,16 @@
 #include <vector>
 #include <memory>
 
+#include "VariableStateInterface.h"
 #include "BooleanVariable.h"
 #include "IntegerVariable.h"
-#include "expressions/VariableExpression.h"
 #include "Command.h"
+#include "expressions/VariableExpression.h"
 
 namespace storm {
 
 namespace ir {
 
-	struct VariableAdder {
-        /*!
-         * Adds an integer variable with the given name, lower and upper bound.
-         *
-         * @param name The name of the boolean variable to add.
-         */
-		uint_fast64_t addBooleanVariable(std::string const& name) = 0;
-
-        /*!
-         * Adds an integer variable with the given name, lower and upper bound.
-         *
-         * @param name The name of the integer variable to add.
-         * @param lower The lower bound of the integer variable.
-         * @param upper The upper bound of the integer variable.
-         */
-		uint_fast64_t addIntegerVariable(std::string const& name) = 0;
-        
-        /*!
-         * Retrieves the next free (global) index for a boolean variable.
-         */
-        uint_fast64_t getNextGlobalBooleanVariableIndex() const = 0;
-        
-        /*!
-         * Retrieves the next free (global) index for a integer variable.
-         */
-        uint_fast64_t getNextGlobalIntegerVariableIndex() const = 0;
-	};
-
 /*!
  * A class representing a module.
  */
@@ -92,7 +65,7 @@ public:
      * @param adder An instance of the VariableAdder interface that keeps track of all the variables in the probabilistic
      * program.
 	 */
-	Module(Module const& oldModule, std::string const& newModuleName, 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, std::shared_ptr<VariableAdder> const& adder);
+	Module(Module const& oldModule, std::string const& newModuleName, 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, std::shared_ptr<VariableStateInterface> const& variableState);
 
 	/*!
 	 * Retrieves the number of boolean variables in the module.

src/ir/expressions/VariableExpression.h

@@ -8,11 +8,13 @@
 #ifndef VARIABLEEXPRESSION_H_
 #define VARIABLEEXPRESSION_H_
 
-#include "src/ir/expressions/BaseExpression.h"
-
 #include <memory>
 #include <iostream>
 
+#include "src/ir/VariableStateInterface.h"
+#include "BaseExpression.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -25,32 +27,41 @@ namespace expressions {
 
 class VariableExpression : public BaseExpression {
 public:
-	VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName,
-			std::shared_ptr<BaseExpression> lowerBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr),
-			std::shared_ptr<BaseExpression> upperBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr))
-			: BaseExpression(type), index(index), variableName(variableName),
-			  lowerBound(lowerBound), upperBound(upperBound) {
+    VariableExpression(ReturnType type, std::string variableName) : BaseExpression(type), localIndex(0), globalIndex(0), variableName(variableName) {
+        // Nothing to do here.
+    }
+    
+	VariableExpression(ReturnType type, uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string variableName)
+			: BaseExpression(type), localIndex(localIndex), globalIndex(globalIndex), variableName(variableName) {
+        // Nothing to do here.
 	}
+    
+    VariableExpression(VariableExpression const& oldExpression, std::string const& newName, uint_fast64_t newGlobalIndex)
+        : BaseExpression(oldExpression.getType()), localIndex(oldExpression.localIndex), globalIndex(newGlobalIndex), variableName(newName) {
+        // Nothing to do here.
+    }
 
 	virtual ~VariableExpression() {
+        // Nothing to do here.
 	}
 
-	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) {
-		std::shared_ptr<BaseExpression> lower = this->lowerBound, upper = this->upperBound;
-		if (lower != nullptr) lower = lower->clone(renaming, bools, ints);
-		if (upper != nullptr) upper = upper->clone(renaming, bools, ints);
-		if (renaming.count(this->variableName) > 0) {
-			std::string newName = renaming.at(this->variableName);
+    virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, std::shared_ptr<VariableStateInterface> const& variableState) {
+        // Perform the proper cloning.
+    }
+    
+	virtual std::shared_ptr<BaseExpression> clone(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) {
+        auto renamingPair = renaming.find(this->variableName);
+        if (renamingPair != renaming.end()) {
 			if (this->getType() == bool_) {
-				return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, bools.at(newName), newName, lower, upper));
+				return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, this->localIndex, booleanVariableToIndexMap.at(renamingPair->second), renamingPair->second));
 			} else if (this->getType() == int_) {
-				return std::shared_ptr<BaseExpression>(new VariableExpression(int_, ints.at(newName), newName, lower, upper));
+				return std::shared_ptr<BaseExpression>(new VariableExpression(int_, this->localIndex, integerVariableToIndexMap.at(renamingPair->second), renamingPair->second));
 			} else {
-				LOG4CPLUS_ERROR(logger, "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int.");
-				return std::shared_ptr<BaseExpression>(nullptr);
+				LOG4CPLUS_ERROR(logger, "Renaming variable " << this->variableName << " that is neither bool nor int.");
+				throw storm::exceptions::InvalidArgumentException() << "Renaming variable " << this->variableName << " that is neither bool nor int.";
 			}
 		} else {
-			return std::shared_ptr<BaseExpression>(new VariableExpression(this->getType(), this->index, this->variableName, lower, upper));
+			return std::shared_ptr<BaseExpression>(new VariableExpression(this->getType(), this->localIndex, this->globalIndex, this->variableName));
 		}
 	}
 
@@ -67,14 +78,6 @@ public:
 	virtual std::string dump(std::string prefix) const {
 		std::stringstream result;
 		result << prefix << this->variableName << " " << index << std::endl;
-		if (this->lowerBound != nullptr) {
-			result << prefix << "lower bound" << std::endl;
-			result << this->lowerBound->dump(prefix + "\t");
-		}
-		if (this->upperBound != nullptr) {
-			result << prefix << "upper bound" << std::endl;
-			result << this->upperBound->dump(prefix + "\t");
-		}
 		return result.str();
 	}
 
@@ -84,7 +87,7 @@ public:
 		}
 
 		if (variableValues != nullptr) {
-			return variableValues->second[index];
+			return variableValues->second[globalIndex];
 		} else {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression"
 					<< " involving variables without variable values.";
@@ -97,7 +100,7 @@ public:
 		}
 
 		if (variableValues != nullptr) {
-			return variableValues->first[index];
+			return variableValues->first[globalIndex];
 		} else {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression"
 					<< " involving variables without variable values.";
@@ -117,24 +120,18 @@ public:
 		return variableName;
 	}
 
-	std::shared_ptr<BaseExpression> const& getLowerBound() const {
-		return lowerBound;
+	uint_fast64_t getLocalVariableIndex() const {
+		return this->localIndex;
 	}
-
-	std::shared_ptr<BaseExpression> const& getUpperBound() const {
-		return upperBound;
-	}
-
-	uint_fast64_t getVariableIndex() const {
-		return this->index;
+    
+    uint_fast64_t getGlobalVariableIndex() const {
+		return this->globalIndex;
 	}
 
 private:
-	uint_fast64_t index;
+	uint_fast64_t localIndex;
+    uint_fast64_t globalIndex;
 	std::string variableName;
-
-	std::shared_ptr<BaseExpression> lowerBound;
-	std::shared_ptr<BaseExpression> upperBound;
 };
 
 }

src/parser/prismparser/PrismGrammar.cpp

@@ -5,6 +5,11 @@
  *      Author: chris
  */
 
+// Needed for file IO.
+#include <fstream>
+#include <iomanip>
+#include <limits>
+
 #include "PrismGrammar.h"
 
 #include "src/utility/OsDetection.h"
@@ -18,11 +23,6 @@
 #include "src/parser/prismparser/IdentifierGrammars.h"
 #include "src/parser/prismparser/VariableState.h"
 
-// Needed for file IO.
-#include <fstream>
-#include <iomanip>
-#include <limits>
-
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 extern log4cplus::Logger logger;
@@ -41,37 +41,39 @@ void dump(const std::string& s) {
 	std::cerr << "Dump: " << s << std::endl;
 }
 
-std::shared_ptr<BaseExpression> PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value) {
+std::shared_ptr<BaseExpression> PrismGrammar::addIntegerConstant(std::string const& name, std::shared_ptr<BaseExpression> const& value) {
 	this->state->integerConstants_.add(name, value);
 	this->state->allConstantNames_.add(name, name);
 	return value;
 }
 
-void PrismGrammar::addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping) {
+void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::shared_ptr<BaseExpression>>& nameToExpressionMap) {
 	this->state->labelNames_.add(name, name);
-	mapping[name] = value;
+	nameToExpressionMap[name] = value;
 }
-void PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) {
-	//std::cout << "Adding int assignment for " << variable << std::endl;
+    
+void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
 	this->state->assignedLocalIntegerVariables_.add(variable, variable);
-	mapping[variable] = Assignment(variable, value);
+	variableToAssignmentMap[variable] = Assignment(variable, value);
 }
-void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) {
-	//std::cout << "Adding bool assignment for " << variable << std::endl;
+    
+void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
 	this->state->assignedLocalBooleanVariables_.add(variable, variable);
-	mapping[variable] = Assignment(variable, value);
+	variableToAssigmentMap[variable] = Assignment(variable, value);
 }
-Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping) {
+    
+Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string>& renaming) {
 	this->state->moduleNames_.add(name, name);
 	Module* old = this->moduleMap_.find(oldname);
 	if (old == nullptr) {
-		LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!");
-		throw "Renaming module failed";
+		LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist.");
+		throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist.";
 	}
-	Module res(*old, name, mapping, this->state);
+	Module res(*old, newName, renaming, this->state);
 	this->moduleMap_.at(name) = res;
 	return res;
 }
+    
 Module PrismGrammar::createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands) {
 	this->state->moduleNames_.add(name, name);
 	Module res(name, bools, ints, boolids, intids, commands);
@@ -80,14 +82,12 @@ Module PrismGrammar::createModule(const std::string name, std::vector<BooleanVar
 }
 
 void PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
-	//std::cout << "Creating int " << name << " = " << init << std::endl;
 	uint_fast64_t id = this->state->addIntegerVariable(name);
 	vars.emplace_back(id, name, lower, upper, init);
 	varids[name] = id;
 	this->state->localIntegerVariables_.add(name, name);
 }
 void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
-	//std::cout << "Creating bool " << name << std::endl;
 	uint_fast64_t id = this->state->addBooleanVariable(name);
 	vars.emplace_back(id, name, init);
 	varids[name] = id;

src/parser/prismparser/PrismGrammar.h

@@ -47,8 +47,21 @@ class PrismGrammar : public qi::grammar<
 	>,
 	Skipper> {
 public:
+    /*!
+     * Default constructor that creates an empty and functional grammar.
+     */
 	PrismGrammar();
+        
+    /*!
+     * Puts all sub-grammars into the mode for performing the second run. A two-run model was chosen
+     * because modules can involve variables that are only declared afterwards, so the first run
+     * creates all variables and the second one tries to parse the full model.
+     */
 	void prepareForSecondRun();
+        
+    /*!
+     * Resets all sub-grammars, i.e. puts them into an initial state.
+     */
 	void resetGrammars();
 
 private:
@@ -122,15 +135,88 @@ private:
 	storm::parser::prism::modelTypeStruct modelType_;
 	storm::parser::prism::relationalOperatorStruct relations_;
 
-	std::shared_ptr<BaseExpression> addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value);
-	void addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping);
-	void addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping);
-	void addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping);
-	Module renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping);
-	Module createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands);
-
-	void createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids);
-	void createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids);
+    /*!
+     * Adds a constant of type integer with the given name and value.
+     *
+     * @param name The name of the constant.
+     * @param value An expression definining the value of the constant.
+     */
+	std::shared_ptr<BaseExpression> addIntegerConstant(std::string const& name, std::shared_ptr<BaseExpression> const& value);
+    
+    /*!
+     * Adds a label with the given name and expression to the given label-to-expression map.
+     *
+     * @param name The name of the label.
+     * @param expression The expression associated with the label.
+     * @param nameToExpressionMap The map to which the label is added.
+     */
+	void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::shared_ptr<BaseExpression>>& nameToExpressionMap);
+        
+    /*!
+     * Adds a boolean assignment for the given variable with the given expression and adds it to the
+     * provided variable-to-assignment map.
+     *
+     * @param variable The name of the variable that the assignment targets.
+     * @param expression The expression that is assigned to the variable.
+     * @param variableToAssignmentMap The map to which the assignment is added.
+     */
+	void addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
+        
+    /*!
+    * Adds a boolean assignment for the given variable with the given expression and adds it to the
+    * provided variable-to-assignment map.
+    *
+    * @param variable The name of the variable that the assignment targets.
+    * @param expression The expression that is assigned to the variable.
+    * @param variableToAssignmentMap The map to which the assignment is added.
+    */
+	void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap);
+        
+    /*!
+     * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module
+     * with the given name which renames all identifiers according to the given mapping.
+     *
+     * @param name The name of the new module.
+     * @param oldName The name of the module that is to be copied (modulo renaming).
+     * @param renaming A mapping from identifiers to their new names.
+     */
+	Module renameModule(std::string const& name, std::string const& oldName, std::map<std::string, std::string>& renaming);
+        
+    /*!
+     * Creates a new module with the given name, boolean and integer variables and commands.
+     *
+     * @param name The name of the module to create.
+     * @param booleanVariables The boolean variables of the module.
+     * @param integerVariables The integer variables of the module.
+     * @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
+     * @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
+     * @param commands The commands associated with this module.
+     */
+	Module createModule(std::string const& name, std::vector<BooleanVariable> const& booleanVariables, std::vector<IntegerVariable> const& integerVariables, std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, std::map<std::string, uint_fast64_t> integerVariableToLocalIndexMap, std::vector<storm::ir::Command> const& commands);
+
+    /*!
+     * Creates an integer variable with the given name, domain and initial value and adds it to the
+     * provided list of integer variables and the given mappings.
+     *
+     * @param name The name of the integer variable.
+     * @param lower The expression that defines the lower bound of the domain.
+     * @param upper The expression that defines the upper bound of the domain.
+     * @param init The expression that defines the initial value of the variable.
+     * @param integerVariableToLocalIndexMap A mapping of integer variables to local indices.
+     * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices.
+     */
+	void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToLocalIndexMap, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap);
+        
+    /*!
+    * Creates an boolean variable with the given name and initial value and adds it to the
+    * provided list of boolean variables and the given mappings.
+    *
+    * @param name The name of the boolean variable.
+    * @param init The expression that defines the initial value of the variable.
+    * @param booleanVariableToLocalIndexMap A mapping of boolean variables to local indices.
+    * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices.
+    */
+	void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToLocalIndexMap, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap);
 };
 
 

src/parser/prismparser/VariableState.cpp

@@ -31,10 +31,18 @@ std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct&
 }
 
 
-VariableState::VariableState(bool firstRun)	: firstRun(firstRun), keywords(), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0) {
+VariableState::VariableState(bool firstRun)	: firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0) {
     // Nothing to do here.
 }
 
+uint_fast64_t VariableState::getNextLocalBooleanVariableIndex() const {
+    return this->nextLocalBooleanVariableIndex;
+}
+    
+uint_fast64_t VariableState::getNextLocalIntegerVariableIndex() const {
+    return this->nextLocalIntegerVariableIndex;
+}
+    
 uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const {
     return this->nextGlobalBooleanVariableIndex;
 }
@@ -43,17 +51,18 @@ uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const {
     return this->nextGlobalIntegerVariableIndex;
 }
     
-uint_fast64_t VariableState::addBooleanVariable(std::string const& name) {
+std::pair<uint_fast64_t, uint_fast64_t> VariableState::addBooleanVariable(std::string const& name) {
 	if (firstRun) {
 		LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << ".");
-		this->booleanVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name)));
+		this->booleanVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextLocalBooleanVariableIndex, this->nextGlobalBooleanVariableIndex, name)));
 		this->booleanVariableNames_.add(name, name);
 		++this->nextGlobalBooleanVariableIndex;
-		return this->nextGlobalBooleanVariableIndex - 1;
+        ++this->nextLocalBooleanVariableIndex;
+		return std::make_pair(this->nextLocalBooleanVariableIndex - 1, this->nextGlobalBooleanVariableIndex - 1);
 	} else {
-		std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
-		if (res != nullptr) {
-			return res->getVariableIndex();
+		std::shared_ptr<VariableExpression> variableExpression = this->booleanVariables_.at(name);
+		if (variableExpression != nullptr) {
+			return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex());
 		} else {
 			LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist.");
             throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist.";
@@ -61,17 +70,18 @@ uint_fast64_t VariableState::addBooleanVariable(std::string const& name) {
 	}
 }
 
-uint_fast64_t VariableState::addIntegerVariable(std::string const& name) {
+std::pair<uint_fast64_t, uint_fast64_t> VariableState::addIntegerVariable(std::string const& name) {
 	if (firstRun) {
 		LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << ".");
-		this->integerVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name)));
+		this->integerVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex, name)));
 		this->integerVariableNames_.add(name, name);
 		++this->nextGlobalIntegerVariableIndex;
-		return this->nextGlobalIntegerVariableIndex - 1;
+        ++this->nextLocalIntegerVariableIndex;
+		return std::make_pair(this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex - 1);
 	} else {
-		std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
-		if (res != nullptr) {
-			return res->getVariableIndex();
+		std::shared_ptr<VariableExpression> variableExpression = this->integerVariables_.at(name);
+		if (variableExpression != nullptr) {
+			return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex());
 		} else {
 			LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist.");
             throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist.";
@@ -79,14 +89,14 @@ uint_fast64_t VariableState::addIntegerVariable(std::string const& name) {
 	}
 }
 
-std::shared_ptr<VariableExpression> VariableState::getBooleanVariableExpression(std::string const& name) {
-	std::shared_ptr<VariableExpression>* res = this->booleanVariables_.find(name);
-	if (res != nullptr) {
-		return *res;
+std::shared_ptr<VariableExpression> VariableState::getBooleanVariableExpression(std::string const& name) const {
+	std::shared_ptr<VariableExpression>* variableExpression = this->booleanVariables_.find(name);
+	if (variableExpression != nullptr) {
+		return *variableExpression;
 	} else {
 		if (firstRun) {
 			LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead.");
-			return std::shared_ptr<VariableExpression>(BaseExpression::bool_, 0, name);
+			return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::bool_, name));
 		} else {
 			LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist.");
             throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist.";
@@ -94,14 +104,14 @@ std::shared_ptr<VariableExpression> VariableState::getBooleanVariableExpression(
 	}
 }
 
-std::shared_ptr<VariableExpression> VariableState::getIntegerVariableExpression(std::string const& name) {
-	std::shared_ptr<VariableExpression>* res = this->integerVariables_.find(name);
-	if (res != nullptr) {
-		return *res;
+std::shared_ptr<VariableExpression> VariableState::getIntegerVariableExpression(std::string const& name) const {
+	std::shared_ptr<VariableExpression>* variableExpression = this->integerVariables_.find(name);
+	if (variableExpression != nullptr) {
+		return *variableExpression;
 	} else {
 		if (firstRun) {
 			LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead.");
-			return std::shared_ptr<VariableExpression>(BaseExpression::int_, 0, name);
+			return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::int_, name));
 		} else {
 			LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist.");
             throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist.";
@@ -109,10 +119,10 @@ std::shared_ptr<VariableExpression> VariableState::getIntegerVariableExpression(
 	}
 }
     
-std::shared_ptr<VariableExpression> VariableState::getVariableExpression(std::string const& name) {
-	std::shared_ptr<VariableExpression>* res = this->integerVariables_.find(name);
-	if (res != nullptr) {
-		return *res;
+std::shared_ptr<VariableExpression> VariableState::getVariableExpression(std::string const& name) const {
+	std::shared_ptr<VariableExpression>* variableExpression = this->integerVariables_.find(name);
+	if (variableExpression != nullptr) {
+		return *variableExpression;
 	}
     LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist.");
     throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist.";
@@ -121,6 +131,8 @@ std::shared_ptr<VariableExpression> VariableState::getVariableExpression(std::st
 void VariableState::clearLocalVariables() {
 	this->localBooleanVariables_.clear();
 	this->localIntegerVariables_.clear();
+    this->nextLocalBooleanVariableIndex = 0;
+    this->nextLocalIntegerVariableIndex = 0;
 }
 
 bool VariableState::isFreeIdentifier(std::string const& identifier) const {

src/parser/prismparser/VariableState.h

@@ -27,10 +27,18 @@ template<typename T>
 std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols);
 
 /*!
- * This class contains the state that is needed during the parsing of a prism model.
+ * This class contains the internal state that is needed for parsing a PRISM model.
  */
 struct VariableState : public storm::ir::VariableAdder {
 
+    /*!
+     * Creates a new variable state object. By default, this object will be set to a state in which
+     * it is ready for performing a first run on some input. The first run creates all variables
+     * while the second one checks for the correct usage of variables in expressions.
+     *
+     * @param firstRun If set, this object will be in a state ready for performing the first run. If
+     * set to false, this object will assume that it has all variable data already.
+     */
 	VariableState(bool firstRun = true);
 	
 	/*!
@@ -43,6 +51,30 @@ struct VariableState : public storm::ir::VariableAdder {
 	 */
 	keywordsStruct keywords;
 
+    /*!
+     * Internal counter for the local index of the next new boolean variable.
+     */
+    uint_fast64_t nextLocalBooleanVariableIndex;
+    
+    /*!
+     * Retrieves the next free local index for a boolean variable.
+     *
+     * @return The next free local index for a boolean variable.
+     */
+    uint_fast64_t getNextLocalBooleanVariableIndex() const;
+
+    /*!
+     * Internal counter for the local index of the next new integer variable.
+     */
+    uint_fast64_t nextLocalIntegerVariableIndex;
+    
+    /*!
+     * Retrieves the next free global index for a integer variable.
+     *
+     * @return The next free global index for a integer variable.
+     */
+    uint_fast64_t getNextLocalIntegerVariableIndex() const;
+    
 	/*!
 	 * Internal counter for the index of the next new boolean variable.
 	 */
@@ -81,17 +113,17 @@ struct VariableState : public storm::ir::VariableAdder {
 	 * Adds a new boolean variable with the given name.
      *
 	 * @param name The name of the variable.
-	 * @return The global index of the variable.
+	 * @return A pair containing the local and global index of the variable.
 	 */
-	uint_fast64_t addBooleanVariable(std::string const& name);
+    std::pair<uint_fast64_t, uint_fast64_t> addBooleanVariable(std::string const& name);
     
 	/*!
 	 * Adds a new integer variable with the given name.
      *
 	 * @param name The name of the variable.
-	 * @return The global index of the variable.
+	 * @return A pair containing the local and global index of the variable.
 	 */
-	uint_fast64_t addIntegerVariable(std::string const& name);
+    std::pair<uint_fast64_t, uint_fast64_t> addIntegerVariable(std::string const& name);
 
 	/*!
 	 * Retrieves the variable expression for the boolean variable with the given name.
@@ -99,7 +131,7 @@ struct VariableState : public storm::ir::VariableAdder {
 	 * @param name The name of the boolean variable for which to retrieve the variable expression.
 	 * @return The variable expression for the boolean variable with the given name.
 	 */
-	std::shared_ptr<VariableExpression> getBooleanVariableExpression(std::string const& name);
+	std::shared_ptr<VariableExpression> getBooleanVariableExpression(std::string const& name) const;
     
 	/*!
 	 * Retrieves the variable expression for the integer variable with the given name.
@@ -107,7 +139,7 @@ struct VariableState : public storm::ir::VariableAdder {
 	 * @param name The name of the integer variable for which to retrieve the variable expression.
 	 * @return The variable expression for the integer variable with the given name.
 	 */
-	std::shared_ptr<VariableExpression> getIntegerVariableExpression(std::string const& name);
+	std::shared_ptr<VariableExpression> getIntegerVariableExpression(std::string const& name) const;
     
 	/*!
 	 * Retrieve the variable expression for the variable with the given name.
@@ -115,7 +147,7 @@ struct VariableState : public storm::ir::VariableAdder {
 	 * @param name The name of the variable for which to retrieve the variable expression.
 	 * @return The variable expression for the variable with the given name.
 	 */
-	std::shared_ptr<VariableExpression> getVariableExpression(std::string const& name);
+	std::shared_ptr<VariableExpression> getVariableExpression(std::string const& name) const;
 
 	/*!
 	 * Clears all local variables.

src/parser/prismparser/VariableStateInterface.h

@@ -0,0 +1,69 @@
+/*
+ * VariableStateInterface.h
+ *
+ *  Created on: 10.06.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_IR_VARIABLESTATEINTERFACE_H_
+#define STORM_IR_VARIABLESTATEINTERFACE_H_
+
+namespace storm {
+namespace ir {
+    
+struct VariableStateInterface {
+    /*!
+     * Adds an integer variable with the given name, lower and upper bound.
+     *
+     * @param name The name of the boolean variable to add.
+     */
+    virtual uint_fast64_t addBooleanVariable(std::string const& name) = 0;
+    
+    /*!
+     * Adds an integer variable with the given name, lower and upper bound.
+     *
+     * @param name The name of the integer variable to add.
+     * @param lower The lower bound of the integer variable.
+     * @param upper The upper bound of the integer variable.
+     */
+    virtual uint_fast64_t addIntegerVariable(std::string const& name) = 0;
+    
+	/*!
+	 * Retrieves the variable expression for the boolean variable with the given name.
+     *
+	 * @param name The name of the boolean variable for which to retrieve the variable expression.
+	 * @return The variable expression for the boolean variable with the given name.
+	 */
+	std::shared_ptr<VariableExpression> getBooleanVariableExpression(std::string const& name) const = 0;
+    
+	/*!
+	 * Retrieves the variable expression for the integer variable with the given name.
+     *
+	 * @param name The name of the integer variable for which to retrieve the variable expression.
+	 * @return The variable expression for the integer variable with the given name.
+	 */
+	std::shared_ptr<VariableExpression> getIntegerVariableExpression(std::string const& name) const = 0;
+    
+	/*!
+	 * Retrieve the variable expression for the variable with the given name.
+     *
+	 * @param name The name of the variable for which to retrieve the variable expression.
+	 * @return The variable expression for the variable with the given name.
+	 */
+	std::shared_ptr<VariableExpression> getVariableExpression(std::string const& name) const = 0;
+    
+    /*!
+     * Retrieves the next free (global) index for a boolean variable.
+     */
+    virtual uint_fast64_t getNextGlobalBooleanVariableIndex() const = 0;
+    
+    /*!
+     * Retrieves the next free (global) index for a integer variable.
+     */
+    virtual uint_fast64_t getNextGlobalIntegerVariableIndex() const = 0;
+};
+
+} // namespace ir
+} // namespace storm
+
+#endif /* STORM_IR_VARIABLESTATEINTERFACE_H_ */