Added some functionality to IR. Introduced case distinction for boolean/integer assignments in updates. Started writing an IR adapter.

src/adapters/IntermediateRepresentationAdapter.h

@@ -0,0 +1,144 @@
+/*
+ * IntermediateRepresentationAdapter.h
+ *
+ *  Created on: 13.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_
+#define STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_
+
+#include <tuple>
+#include <unordered_map>
+#include <boost/functional/hash.hpp>
+#include <map>
+#include <queue>
+#include <iostream>
+
+typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType;
+
+namespace storm {
+
+namespace adapters {
+
+class StateHash {
+public:
+	std::size_t operator()(StateType* state) const {
+		size_t seed = 0;
+		for (auto it = state->first.begin(); it != state->first.end(); ++it) {
+			boost::hash_combine<bool>(seed, *it);
+		}
+		for (auto it = state->second.begin(); it != state->second.end(); ++it) {
+			boost::hash_combine<int_fast64_t>(seed, *it);
+		}
+		return seed;
+	}
+};
+
+class IntermediateRepresentationAdapter {
+public:
+	template<class T>
+	static storm::storage::SquareSparseMatrix<T>* toSparseMatrix(storm::ir::Program const& program) {
+
+		uint_fast64_t numberOfIntegerVariables = 0;
+		uint_fast64_t numberOfBooleanVariables = 0;
+		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+			numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables();
+			numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables();
+		}
+
+		std::vector<storm::ir::BooleanVariable> booleanVariables;
+		std::vector<storm::ir::IntegerVariable> integerVariables;
+		booleanVariables.resize(numberOfBooleanVariables);
+		integerVariables.resize(numberOfIntegerVariables);
+
+		std::unordered_map<std::string, uint_fast64_t> booleanVariableToIndexMap;
+		std::unordered_map<std::string, uint_fast64_t> integerVariableToIndexMap;
+
+		uint_fast64_t nextBooleanVariableIndex = 0;
+		uint_fast64_t nextIntegerVariableIndex = 0;
+		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+			storm::ir::Module const& module = program.getModule(i);
+
+			for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
+				booleanVariables[nextBooleanVariableIndex] = module.getBooleanVariable(j);
+				booleanVariableToIndexMap[module.getBooleanVariable(j).getName()] = nextBooleanVariableIndex;
+				++nextBooleanVariableIndex;
+			}
+			for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
+				integerVariables[nextIntegerVariableIndex] = module.getIntegerVariable(j);
+				integerVariableToIndexMap[module.getIntegerVariable(j).getName()] = nextIntegerVariableIndex;
+				++nextIntegerVariableIndex;
+			}
+		}
+
+		StateType* initialState = new StateType(std::vector<bool>(), std::vector<int_fast64_t>());
+		std::get<0>(*initialState).resize(numberOfBooleanVariables);
+		std::get<1>(*initialState).resize(numberOfIntegerVariables);
+
+		for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) {
+			bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(std::get<0>(*initialState), std::get<1>(*initialState));
+			std::get<0>(*initialState)[i] = initialValue;
+		}
+
+		for (uint_fast64_t i = 0; i < numberOfIntegerVariables; ++i) {
+			int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(std::get<0>(*initialState), std::get<1>(*initialState));
+			std::get<1>(*initialState)[i] = initialValue;
+		}
+
+		std::cout << "Initial State:" << std::get<0>(*initialState) << " / " << std::get<1>(*initialState) << std::endl;
+
+		uint_fast64_t nextIndex = 1;
+		std::unordered_map<StateType*, uint_fast64_t, StateHash> stateToIndexMap;
+		std::vector<StateType*> allStates;
+		std::queue<StateType*> stateQueue;
+
+		allStates.push_back(initialState);
+		stateQueue.push(initialState);
+		stateToIndexMap[initialState] = 0;
+
+		while (!stateQueue.empty()) {
+			// Get first state in queue.
+			StateType* currentState = stateQueue.front();
+			stateQueue.pop();
+
+			// Iterate over all modules.
+			for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+				storm::ir::Module const& module = program.getModule(i);
+
+				// Iterate over all commands.
+				for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
+					storm::ir::Command const& command = module.getCommand(j);
+
+					// Check if this command is enabled in the current state.
+					if (command.getGuard()->getValueAsBool(std::get<0>(*currentState), std::get<1>(*currentState))) {
+						for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
+							storm::ir::Update const& update = command.getUpdate(k);
+
+							std::map<std::string, storm::ir::Assignment> const& booleanAssignmentMap = update.getBooleanAssignments();
+							for (auto assignedVariable : booleanAssignmentMap) {
+								// Check if the variable that is being assigned is a boolean or an integer.
+								// auto boolIt =
+
+							}
+						}
+					}
+				}
+			}
+		}
+
+		// Now free all the elements we allocated.
+		for (auto element : allStates) {
+			delete element;
+		}
+		return nullptr;
+	}
+
+};
+
+}
+
+}
+
+
+#endif /* STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ */

src/exceptions/ExpressionEvaluationException.h

@@ -0,0 +1,23 @@
+/*
+ * ExpressionEvaluationException.h
+ *
+ *  Created on: 12.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_
+#define STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+
+namespace exceptions {
+
+STORM_EXCEPTION_DEFINE_NEW(ExpressionEvaluationException)
+
+}
+
+}
+
+#endif /* STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ */

src/exceptions/NotImplementedException.h

@@ -0,0 +1,23 @@
+/*
+ * NotImplementedException.h
+ *
+ *  Created on: 12.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_
+#define STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+
+namespace exceptions {
+
+STORM_EXCEPTION_DEFINE_NEW(NotImplementedException)
+
+}
+
+}
+
+#endif /* STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ */

src/ir/BooleanVariable.cpp

@@ -19,16 +19,16 @@ BooleanVariable::BooleanVariable() : Variable() {
 }
 
 // Initializes all members according to the given values.
-BooleanVariable::BooleanVariable(std::string variableName,
+BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName,
 		std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
-		: Variable(variableName,  initialValue) {
+		: Variable(index, variableName,  initialValue) {
 	// Nothing to do here.
 }
 
 // Build a string representation of the variable.
 std::string BooleanVariable::toString() const {
 	std::stringstream result;
-	result << getVariableName() << ": bool";
+	result << this->getName() << ": bool";
 	if (this->getInitialValue() != nullptr) {
 		result << " init " << this->getInitialValue()->toString();
 	}

src/ir/BooleanVariable.h

@@ -8,6 +8,8 @@
 #ifndef STORM_IR_BOOLEANVARIABLE_H_
 #define STORM_IR_BOOLEANVARIABLE_H_
 
+#include "expressions/BooleanLiteral.h"
+
 #include "Variable.h"
 #include <memory>
 
@@ -27,10 +29,11 @@ public:
 
 	/*!
 	 * Creates a boolean variable with the given name and the given 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.
 	 */
-	BooleanVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+	BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(new storm::ir::expressions::BooleanLiteral(false)));
 
 	/*!
 	 * Retrieves a string representation of this variable.

src/ir/Command.cpp

@@ -24,6 +24,21 @@ Command::Command(std::string commandName, std::shared_ptr<storm::ir::expressions
 	// Nothing to do here.
 }
 
+// Return the expression for the guard.
+std::shared_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
+	return guardExpression;
+}
+
+// Return the number of updates.
+uint_fast64_t Command::getNumberOfUpdates() const {
+	return this->updates.size();
+}
+
+// Return the requested update.
+storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const {
+	return this->updates[index];
+}
+
 // Build a string representation of the command.
 std::string Command::toString() const {
 	std::stringstream result;

src/ir/Command.h

@@ -35,6 +35,24 @@ public:
 	 */
 	Command(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates);
 
+	/*!
+	 * Retrieves a reference to the guard of the command.
+	 * @returns a reference to the guard of the command.
+	 */
+	std::shared_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
+
+	/*!
+	 * Retrieves the number of updates associated with this command.
+	 * @returns the number of updates associated with this command.
+	 */
+	uint_fast64_t getNumberOfUpdates() const;
+
+	/*!
+	 * Retrieves a reference to the update with the given index.
+	 * @returns a reference to the update with the given index.
+	 */
+	storm::ir::Update const& getUpdate(uint_fast64_t index) const;
+
 	/*!
 	 * Retrieves a string representation of this command.
 	 * @returns a string representation of this command.

src/ir/IntegerVariable.cpp

@@ -9,6 +9,8 @@
 
 #include <sstream>
 
+#include <iostream>
+
 namespace storm {
 
 namespace ir {
@@ -19,14 +21,16 @@ IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
 }
 
 // Initializes all members according to the given values.
-IntegerVariable::IntegerVariable(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) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
-	// Nothing to do here.
+IntegerVariable::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) : Variable(index, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
+	if (this->getInitialValue() == nullptr) {
+		this->setInitialValue(lowerBound);
+	}
 }
 
 // Build a string representation of the variable.
 std::string IntegerVariable::toString() const {
 	std::stringstream result;
-	result << this->getVariableName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
+	result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
 	if (this->getInitialValue() != nullptr) {
 		result << " init " + this->getInitialValue()->toString();
 	}

src/ir/IntegerVariable.h

@@ -29,12 +29,13 @@ public:
 	/*!
 	 * Creates an integer variable with the given name, lower and upper bounds and the given initial
 	 * value.
+	 * @param index A unique (among the variables of equal type) index for the variable.
 	 * @param variableName the name of the variable.
 	 * @param lowerBound the lower bound of the domain of the variable.
 	 * @param upperBound the upper bound of the domain of the variable.
 	 * @param initialValue the expression that defines the initial value of the variable.
 	 */
-	IntegerVariable(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>());
+	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));
 
 	/*!
 	 * Retrieves a string representation of this variable.

src/ir/Module.cpp

@@ -14,25 +14,62 @@ namespace storm {
 namespace ir {
 
 // Initializes all members with their default constructors.
-Module::Module() : moduleName(), booleanVariables(), integerVariables(), commands() {
+Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariablesToIndexMap(),
+		  integerVariablesToIndexMap(), commands() {
 	// Nothing to do here.
 }
 
 // Initializes all members according to the given values.
-Module::Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands)
-	: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) {
+Module::Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> booleanVariables,
+		std::vector<storm::ir::IntegerVariable> integerVariables,
+		std::map<std::string, uint_fast64_t> booleanVariableToIndexMap,
+		std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
+		std::vector<storm::ir::Command> commands)
+	: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables),
+	  booleanVariablesToIndexMap(booleanVariableToIndexMap),
+	  integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands) {
 	// Nothing to do here.
 }
 
+// Return the number of boolean variables.
+uint_fast64_t Module::getNumberOfBooleanVariables() const {
+	return this->booleanVariables.size();
+}
+
+// Return the requested boolean variable.
+storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const {
+	return this->booleanVariables[index];
+}
+
+// Return the number of integer variables.
+uint_fast64_t Module::getNumberOfIntegerVariables() const {
+	return this->integerVariables.size();
+}
+
+// Return the requested integer variable.
+storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const {
+	return this->integerVariables[index];
+}
+
+// Return the number of commands.
+uint_fast64_t Module::getNumberOfCommands() const {
+	return this->commands.size();
+}
+
+// Return the requested command.
+storm::ir::Command const& Module::getCommand(uint_fast64_t index) const {
+	return this->commands[index];
+}
+
 // Build a string representation of the variable.
 std::string Module::toString() const {
 	std::stringstream result;
 	result << "module " << moduleName << std::endl;
 	for (auto variable : booleanVariables) {
-		result << "\t" << variable.second.toString() << std::endl;
+		result << "\t" << variable.toString() << std::endl;
 	}
 	for (auto variable : integerVariables) {
-		result << "\t" << variable.second.toString() << std::endl;
+		result << "\t" << variable.toString() << std::endl;
 	}
 	for (auto command : commands) {
 		result << "\t" << command.toString() << std::endl;

src/ir/Module.h

@@ -37,7 +37,47 @@ public:
 	 * @param integerVariables a map of integer variables.
 	 * @param commands the vector of commands.
 	 */
-	Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands);
+	Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> booleanVariables,
+			std::vector<storm::ir::IntegerVariable> integerVariables,
+			std::map<std::string, uint_fast64_t> booleanVariableToIndexMap,
+			std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
+			std::vector<storm::ir::Command> commands);
+
+	/*!
+	 * Retrieves the number of boolean variables in the module.
+	 * @returns the number of boolean variables in the module.
+	 */
+	uint_fast64_t getNumberOfBooleanVariables() const;
+
+	/*!
+	 * Retrieves a reference to the boolean variable with the given index.
+	 * @returns a reference to the boolean variable with the given index.
+	 */
+	storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const;
+
+	/*!
+	 * Retrieves the number of integer variables in the module.
+	 * @returns the number of integer variables in the module.
+	 */
+	uint_fast64_t getNumberOfIntegerVariables() const;
+
+	/*!
+	 * Retrieves a reference to the integer variable with the given index.
+	 * @returns a reference to the integer variable with the given index.
+	 */
+	storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const;
+
+	/*!
+	 * Retrieves the number of commands of this module.
+	 * @returns the number of commands of this module.
+	 */
+	uint_fast64_t getNumberOfCommands() const;
+
+	/*!
+	 * Retrieves a reference to the command with the given index.
+	 * @returns a reference to the command with the given index.
+	 */
+	storm::ir::Command const& getCommand(uint_fast64_t index) const;
 
 	/*!
 	 * Retrieves a string representation of this variable.
@@ -49,11 +89,17 @@ private:
 	// The name of the module.
 	std::string moduleName;
 
-	// A map of boolean variable names to their details.
-	std::map<std::string, storm::ir::BooleanVariable> booleanVariables;
+	// A list of boolean variables.
+	std::vector<storm::ir::BooleanVariable> booleanVariables;
+
+	// A list of integer variables.
+	std::vector<storm::ir::IntegerVariable> integerVariables;
+
+	// A map of boolean variable names to their index.
+	std::map<std::string, uint_fast64_t> booleanVariablesToIndexMap;
 
 	// A map of integer variable names to their details.
-	std::map<std::string, storm::ir::IntegerVariable> integerVariables;
+	std::map<std::string, uint_fast64_t> integerVariablesToIndexMap;
 
 	// The commands associated with the module.
 	std::vector<storm::ir::Command> commands;

src/ir/Program.cpp

@@ -62,6 +62,15 @@ std::string Program::toString() const {
 	return result.str();
 }
 
+uint_fast64_t Program::getNumberOfModules() const {
+	return this->modules.size();
+}
+
+storm::ir::Module const& Program::getModule(uint_fast64_t index) const {
+	return this->modules[index];
+}
+
+
 } // namespace ir
 
 } // namepsace storm

src/ir/Program.h

@@ -54,6 +54,18 @@ public:
 	 */
 	Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels);
 
+	/*!
+	 * Retrieves the number of modules in the program.
+	 * @returns the number of modules in the program.
+	 */
+	uint_fast64_t getNumberOfModules() const;
+
+	/*!
+	 * Retrieves a reference to the module with the given index.
+	 * @param index the index of the module to retrieve.
+	 */
+	storm::ir::Module const& getModule(uint_fast64_t index) const;
+
 	/*!
 	 * Retrieves a string representation of this program.
 	 * @returns a string representation of this program.

src/ir/Update.cpp

@@ -7,6 +7,8 @@
 
 #include "Update.h"
 
+#include "src/exceptions/OutOfRangeException.h"
+
 #include <sstream>
 
 namespace storm {
@@ -14,28 +16,81 @@ namespace storm {
 namespace ir {
 
 // Initializes all members with their default constructors.
-Update::Update() : likelihoodExpression(), assignments() {
+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> assignments)
-	: likelihoodExpression(likelihoodExpression), assignments(assignments) {
+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.
 }
 
+// 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();
+}
+
+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()) {
+		throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '"
+				<< variableName << "' in update " << this->toString() << ".";
+	}
+
+	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()) {
+		throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '"
+				<< variableName << "' in update " << this->toString() << ".";
+	}
+
+	return (*it).second;
+}
+
 // Build a string representation of the update.
 std::string Update::toString() const {
 	std::stringstream result;
 	result << likelihoodExpression->toString() << " : ";
 	uint_fast64_t i = 0;
-	for (auto assignment : assignments) {
+	for (auto assignment : booleanAssignments) {
 		result << assignment.second.toString();
 		++i;
-		if (i < assignments.size() - 1) {
+		if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) {
+			result << " & ";
+		}
+	}
+	i = 0;
+	for (auto assignment : integerAssignments) {
+		result << assignment.second.toString();
+		++i;
+		if (i < integerAssignments.size() - 1) {
 			result << " & ";
 		}
-
 	}
 	return result.str();
 }

src/ir/Update.h

@@ -34,7 +34,49 @@ public:
 	 * @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> 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);
+
+	/*!
+	 * Retrieves the expression for the likelihood of this update.
+	 * @returns 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.
+	 */
+	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.
+	 */
+	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.
+	 */
+	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.
+	 */
+	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.
+	 */
+	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.
+	 */
+	storm::ir::Assignment const& getIntegerAssignment(std::string variableName) const;
 
 	/*!
 	 * Retrieves a string representation of this update.
@@ -46,8 +88,11 @@ private:
 	// An expression specifying the likelihood of taking this update.
 	std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
 
-	// A mapping of variable names to their assignments in this update.
-	std::map<std::string, storm::ir::Assignment> assignments;
+	// A mapping of boolean variable names to their assignments in this update.
+	std::map<std::string, storm::ir::Assignment> booleanAssignments;
+
+	// A mapping of integer variable names to their assignments in this update.
+	std::map<std::string, storm::ir::Assignment> integerAssignments;
 };
 
 } // namespace ir

src/ir/Variable.cpp

@@ -14,17 +14,17 @@ namespace storm {
 namespace ir {
 
 // Initializes all members with their default constructors.
-Variable::Variable() : variableName(), initialValue() {
+Variable::Variable() : index(0), variableName(), initialValue() {
 	// Nothing to do here.
 }
 
 // Initializes all members according to the given values.
-Variable::Variable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : variableName(variableName), initialValue(initialValue) {
+Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : index(index), variableName(variableName), initialValue(initialValue) {
 	// Nothing to do here.
 }
 
 // Return the name of the variable.
-std::string const& Variable::getVariableName() const {
+std::string const& Variable::getName() const {
 	return variableName;
 }
 
@@ -33,6 +33,12 @@ std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInit
 	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

@@ -28,16 +28,17 @@ 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(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+	Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
 
 	/*!
 	 * Retrieves the name of the variable.
 	 * @returns the name of the variable.
 	 */
-	std::string const& getVariableName() const;
+	std::string const& getName() const;
 
 	/*!
 	 * Retrieves the expression defining the initial value of the variable.
@@ -45,7 +46,16 @@ public:
 	 */
 	std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
 
+	/*!
+	 * Sets the initial value to the given expression.
+	 * @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;
+
 	// The name of the variable.
 	std::string variableName;
 

src/ir/expressions/BaseExpression.h

@@ -2,13 +2,17 @@
  * Expression.h
  *
  *  Created on: 03.01.2013
- *      Author: chris
+ *      Author: Christian Dehnert
  */
 
-#ifndef EXPRESSION_H_
-#define EXPRESSION_H_
+#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_
+#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_
+
+#include "src/exceptions/ExpressionEvaluationException.h"
+#include "src/exceptions/NotImplementedException.h"
 
 #include <string>
+#include <vector>
 
 namespace storm {
 
@@ -19,19 +23,70 @@ namespace expressions {
 class BaseExpression {
 
 public:
+	enum ReturnType {undefined, bool_, int_, double_};
+
+	BaseExpression() : type(undefined) {
+
+	}
+
+	BaseExpression(ReturnType type) : type(type) {
+
+	}
+
 	virtual ~BaseExpression() {
 
 	}
 
-	virtual std::string toString() const {
-		return "expr here!";
+	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (type != int_) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
+					<< this->getTypeName() << "' as 'int'.";
+		}
+		throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '"
+					<< this->getTypeName() << " because evaluation implementation is missing.";
+	}
+
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (type != bool_) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
+					<< this->getTypeName() << "' as 'bool'.";
+		}
+		throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '"
+					<< this->getTypeName() << " because evaluation implementation is missing.";
+	}
+
+	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (type != bool_) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
+					<< this->getTypeName() << "' as 'double'.";
+		}
+		throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '"
+					<< this->getTypeName() << " because evaluation implementation is missing.";
 	}
+
+	virtual std::string toString() const = 0;
+
+	std::string getTypeName() const {
+		switch(type) {
+		case bool_: return std::string("bool");
+		case int_: return std::string("int");
+		case double_: return std::string("double");
+		default: return std::string("undefined");
+		}
+	}
+
+	ReturnType getType() const {
+		return type;
+	}
+
+private:
+	ReturnType type;
 };
 
-}
+} // namespace expressions
 
-}
+} // namespace ir
 
-}
+} // namespace storm
 
-#endif /* EXPRESSION_H_ */
+#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */

src/ir/expressions/BinaryBooleanFunctionExpression.h

@@ -5,11 +5,13 @@
  *      Author: chris
  */
 
-#ifndef BINARYBOOLEANFUNCTIONEXPRESSION_H_
-#define BINARYBOOLEANFUNCTIONEXPRESSION_H_
+#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
+#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
 
 #include "src/ir/expressions/BaseExpression.h"
-#include <boost/fusion/include/adapt_struct.hpp>
+
+#include <memory>
+#include <sstream>
 
 namespace storm {
 
@@ -19,38 +21,49 @@ namespace expressions {
 
 class BinaryBooleanFunctionExpression : public BaseExpression {
 public:
-	enum FunctorType {AND, OR, XOR, IMPLIES} functor;
-	std::shared_ptr<storm::ir::expressions::BaseExpression> left;
-	std::shared_ptr<BaseExpression> right;
+	enum FunctionType {AND, OR};
+
+	BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctionType functionType) : BaseExpression(bool_), left(left), right(right), functionType(functionType) {
 
-	BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctorType functor) {
-		this->left = left;
-		this->right = right;
-		this->functor = functor;
 	}
 
 	virtual ~BinaryBooleanFunctionExpression() {
 
 	}
 
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		bool resultLeft = left->getValueAsBool(booleanVariableValues, integerVariableValues);
+		bool resultRight = right->getValueAsBool(booleanVariableValues, integerVariableValues);
+		switch(functionType) {
+		case AND: return resultLeft & resultRight; break;
+		case OR: return resultLeft | resultRight; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown boolean binary operator: '" << functionType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
-		std::string result = left->toString();
-		switch (functor) {
-		case AND: result += " & "; break;
-		case OR: result += " | "; break;
-		case XOR: result += " ^ "; break;
-		case IMPLIES: result += " => "; break;
+		std::stringstream result;
+		result << left->toString();
+		switch (functionType) {
+		case AND: result << " & "; break;
+		case OR: result << " | "; break;
 		}
-		result += right->toString();
+		result << right->toString();
 
-		return result;
+		return result.str();
 	}
+
+private:
+	std::shared_ptr<BaseExpression> left;
+	std::shared_ptr<BaseExpression> right;
+	FunctionType functionType;
 };
 
-}
+} // namespace expressions
 
-}
+} // namespace ir
 
-}
+} // namespace storm
 
-#endif /* BINARYBOOLEANFUNCTIONEXPRESSION_H_ */
+#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */

src/ir/expressions/BinaryNumericalFunctionExpression.h

@@ -18,23 +18,53 @@ namespace expressions {
 
 class BinaryNumericalFunctionExpression : public BaseExpression {
 public:
-	std::shared_ptr<BaseExpression> left;
-	std::shared_ptr<BaseExpression> right;
-	enum FunctorType {PLUS, MINUS, TIMES, DIVIDE} functor;
+	enum FunctionType {PLUS, MINUS, TIMES, DIVIDE};
+
+	BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctionType functionType) : BaseExpression(type), left(left), right(right), functionType(functionType) {
 
-	BinaryNumericalFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctorType functor) {
-		this->left = left;
-		this->right = right;
-		this->functor = functor;
 	}
 
 	virtual ~BinaryNumericalFunctionExpression() {
 
 	}
 
+	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != int_) {
+			BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues);
+		}
+
+		int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues);
+		int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues);
+		switch(functionType) {
+		case PLUS: return resultLeft + resultRight; break;
+		case MINUS: return resultLeft - resultRight; break;
+		case TIMES: return resultLeft * resultRight; break;
+		case DIVIDE: return resultLeft / resultRight; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown numeric binary operator: '" << functionType << "'.";
+		}
+	}
+
+	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != double_) {
+			BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+		}
+
+		double resultLeft = left->getValueAsDouble(booleanVariableValues, integerVariableValues);
+		double resultRight = right->getValueAsDouble(booleanVariableValues, integerVariableValues);
+		switch(functionType) {
+		case PLUS: return resultLeft + resultRight; break;
+		case MINUS: return resultLeft - resultRight; break;
+		case TIMES: return resultLeft * resultRight; break;
+		case DIVIDE: return resultLeft / resultRight; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown numeric binary operator: '" << functionType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = left->toString();
-		switch (functor) {
+		switch (functionType) {
 		case PLUS: result += " + "; break;
 		case MINUS: result += " - "; break;
 		case TIMES: result += " * "; break;
@@ -44,7 +74,10 @@ public:
 
 		return result;
 	}
-
+private:
+	std::shared_ptr<BaseExpression> left;
+	std::shared_ptr<BaseExpression> right;
+	FunctionType functionType;
 };
 
 }

src/ir/expressions/BinaryRelationExpression.h

@@ -18,23 +18,33 @@ namespace expressions {
 
 class BinaryRelationExpression : public BaseExpression {
 public:
-	std::shared_ptr<BaseExpression> left;
-	std::shared_ptr<BaseExpression> right;
-	enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL} relation;
+	enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
+
+	BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relationType) : BaseExpression(bool_), left(left), right(right), relationType(relationType) {
 
-	BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relation) {
-		this->left = left;
-		this->right = right;
-		this->relation = relation;
 	}
 
 	virtual ~BinaryRelationExpression() {
 
 	}
 
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues);
+		int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues);
+		switch(relationType) {
+		case EQUAL: return resultLeft == resultRight; break;
+		case LESS: return resultLeft < resultRight; break;
+		case LESS_OR_EQUAL: return resultLeft <= resultRight; break;
+		case GREATER: return resultLeft > resultRight; break;
+		case GREATER_OR_EQUAL: return resultLeft >= resultRight; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown boolean binary relation: '" << relationType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = left->toString();
-		switch (relation) {
+		switch (relationType) {
 		case EQUAL: result += " = "; break;
 		case LESS: result += " < "; break;
 		case LESS_OR_EQUAL: result += " <= "; break;
@@ -46,6 +56,10 @@ public:
 		return result;
 	}
 
+private:
+	std::shared_ptr<BaseExpression> left;
+	std::shared_ptr<BaseExpression> right;
+	RelationType relationType;
 };
 
 }

src/ir/expressions/BooleanConstantExpression.h

@@ -20,7 +20,7 @@ namespace expressions {
 
 class BooleanConstantExpression : public ConstantExpression {
 public:
-	BooleanConstantExpression(std::string constantName) : ConstantExpression(constantName) {
+	BooleanConstantExpression(std::string constantName) : ConstantExpression(bool_, constantName) {
 		defined = false;
 		value = false;
 	}
@@ -29,6 +29,15 @@ public:
 
 	}
 
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (!defined) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+					<< "Boolean constant '" << this->getConstantName() << "' is undefined.";
+		} else {
+			return value;
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = this->constantName;
 		if (defined) {

src/ir/expressions/BooleanLiteral.h

@@ -20,14 +20,18 @@ class BooleanLiteral : public BaseExpression {
 public:
 	bool value;
 
-	BooleanLiteral(bool value) {
-		this->value = value;
+	BooleanLiteral(bool value) : BaseExpression(bool_), value(value) {
+
 	}
 
 	virtual ~BooleanLiteral() {
 
 	}
 
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		return value;
+	}
+
 	virtual std::string toString() const {
 		if (value) {
 			return std::string("true");

src/ir/expressions/ConstantExpression.h

@@ -20,14 +20,18 @@ class ConstantExpression : public BaseExpression {
 public:
 	std::string constantName;
 
-	ConstantExpression(std::string constantName) {
-		this->constantName = constantName;
+	ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) {
+
 	}
 
 	virtual ~ConstantExpression() {
 
 	}
 
+	std::string const& getConstantName() const {
+		return constantName;
+	}
+
 	virtual std::string toString() const {
 		return constantName;
 	}

src/ir/expressions/DoubleConstantExpression.h

@@ -18,15 +18,23 @@ namespace expressions {
 
 class DoubleConstantExpression : public ConstantExpression {
 public:
-	DoubleConstantExpression(std::string constantName) : ConstantExpression(constantName) {
-		defined = false;
-		value = 0.0;
+	DoubleConstantExpression(std::string constantName) : ConstantExpression(double_, constantName), defined(false), value(0) {
+
 	}
 
 	virtual ~DoubleConstantExpression() {
 
 	}
 
+	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (!defined) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+					<< "Double constant '" << this->getConstantName() << "' is undefined.";
+		} else {
+			return value;
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = this->constantName;
 		if (defined) {
@@ -48,8 +56,9 @@ public:
 		this->value = value;
 	}
 
-	double value;
+private:
 	bool defined;
+	double value;
 };
 
 }

src/ir/expressions/DoubleLiteral.h

@@ -22,14 +22,18 @@ class DoubleLiteral : public BaseExpression {
 public:
 	double value;
 
-	DoubleLiteral(double value) {
-		this->value = value;
+	DoubleLiteral(double value) : BaseExpression(double_), value(value) {
+
 	}
 
 	virtual ~DoubleLiteral() {
 
 	}
 
+	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		return value;
+	}
+
 	virtual std::string toString() const {
 		return boost::lexical_cast<std::string>(value);
 	}

src/ir/expressions/IntegerConstantExpression.h

@@ -18,15 +18,23 @@ namespace expressions {
 
 class IntegerConstantExpression : public ConstantExpression {
 public:
-	IntegerConstantExpression(std::string constantName) : ConstantExpression(constantName) {
-		defined = false;
-		value = 0;
+	IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) {
+
 	}
 
 	virtual ~IntegerConstantExpression() {
 
 	}
 
+	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (!defined) {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+					<< "Integer constant '" << this->getConstantName() << "' is undefined.";
+		} else {
+			return value;
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = this->constantName;
 		if (defined) {
@@ -43,13 +51,14 @@ public:
 		return value;
 	}
 
-	void define(int value) {
+	void define(int_fast64_t value) {
 		defined = true;
 		this->value = value;
 	}
 
-	int value;
+private:
 	bool defined;
+	int_fast64_t value;
 };
 
 }

src/ir/expressions/IntegerLiteral.h

@@ -18,16 +18,20 @@ namespace expressions {
 
 class IntegerLiteral : public BaseExpression {
 public:
-	int value;
+	int_fast64_t value;
+
+	IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) {
 
-	IntegerLiteral(int value) {
-		this->value = value;
 	}
 
 	virtual ~IntegerLiteral() {
 
 	}
 
+	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		return value;
+	}
+
 	virtual std::string toString() const {
 		return boost::lexical_cast<std::string>(value);
 	}

src/ir/expressions/UnaryBooleanFunctionExpression.h

@@ -18,27 +18,38 @@ namespace expressions {
 
 class UnaryBooleanFunctionExpression : public BaseExpression {
 public:
-	std::shared_ptr<BaseExpression> child;
-	enum FunctorType {NOT} functor;
+	enum FunctionType {NOT};
+
+	UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : BaseExpression(bool_), child(child), functionType(functionType) {
 
-	UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctorType functor) {
-		this->child = child;
-		this->functor = functor;
 	}
 
 	virtual ~UnaryBooleanFunctionExpression() {
 
 	}
 
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		bool resultChild = child->getValueAsBool(booleanVariableValues, integerVariableValues);
+		switch(functionType) {
+		case NOT: return !resultChild; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown boolean unary operator: '" << functionType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = "";
-		switch (functor) {
+		switch (functionType) {
 		case NOT: result += "!"; break;
 		}
 		result += child->toString();
 
 		return result;
 	}
+
+private:
+	std::shared_ptr<BaseExpression> child;
+	FunctionType functionType;
 };
 
 }

src/ir/expressions/UnaryNumericalFunctionExpression.h

@@ -18,27 +18,55 @@ namespace expressions {
 
 class UnaryNumericalFunctionExpression : public BaseExpression {
 public:
-	std::shared_ptr<BaseExpression> child;
-	enum FunctorType {MINUS} functor;
+	enum FunctionType {MINUS};
+
+	UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : BaseExpression(type), child(child), functionType(functionType) {
 
-	UnaryNumericalFunctionExpression(std::shared_ptr<BaseExpression> child, FunctorType functor) {
-		this->child = child;
-		this->functor = functor;
 	}
 
 	virtual ~UnaryNumericalFunctionExpression() {
 
 	}
 
+	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != int_) {
+			BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues);
+		}
+
+		int_fast64_t resultChild = child->getValueAsInt(booleanVariableValues, integerVariableValues);
+		switch(functionType) {
+		case MINUS: return -resultChild; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown numerical unary operator: '" << functionType << "'.";
+		}
+	}
+
+	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != double_) {
+			BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+		}
+
+		double resultChild = child->getValueAsDouble(booleanVariableValues, integerVariableValues);
+		switch(functionType) {
+		case MINUS: return -resultChild; break;
+		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+				<< "Unknown numerical unary operator: '" << functionType << "'.";
+		}
+	}
+
 	virtual std::string toString() const {
 		std::string result = "";
-		switch (functor) {
+		switch (functionType) {
 		case MINUS: result += "-"; break;
 		}
 		result += child->toString();
 
 		return result;
 	}
+
+private:
+	std::shared_ptr<BaseExpression> child;
+	FunctionType functionType;
 };
 
 }

src/ir/expressions/VariableExpression.h

@@ -20,9 +20,7 @@ namespace expressions {
 
 class VariableExpression : public BaseExpression {
 public:
-	std::string variableName;
-
-	VariableExpression(std::string variableName) : variableName(variableName) {
+	VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName) : BaseExpression(type), index(index), variableName(variableName) {
 
 	}
 
@@ -33,6 +31,35 @@ public:
 	virtual std::string toString() const {
 		return variableName;
 	}
+
+	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != int_) {
+			BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues);
+		}
+
+		return integerVariableValues[index];
+	}
+
+	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != bool_) {
+			BaseExpression::getValueAsBool(booleanVariableValues, integerVariableValues);
+		}
+
+		return booleanVariableValues[index];
+	}
+
+	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+		if (this->getType() != double_) {
+			BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+		}
+
+		throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with "
+				<< " variable '" << variableName << "' of type double.";
+	}
+
+private:
+	uint_fast64_t index;
+	std::string variableName;
 };
 
 }

src/parser/PrismParser.cpp

@@ -51,7 +51,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 	 * TODO: It should be ensured that updates of a command only refer to variables of the
 	 * current module.
 	 */
-	PrismGrammar() : PrismGrammar::base_type(start) {
+	PrismGrammar() : PrismGrammar::base_type(start), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) {
 		// This rule defines all identifiers that have not been previously used.
 		freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariableNames_ - integerVariableNames_ - allConstantNames_ - labelNames_ - moduleNames_ - keywords_]];
 		freeIdentifierName.name("unused identifier");
@@ -87,9 +87,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		// This block defines all expressions of integral type.
 		atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression);
 		atomicIntegerExpression.name("integer expression");
-		integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+		integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
 		integerMultExpression.name("integer expression");
-		integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+		integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
 		integerPlusExpression.name("integer expression");
 		integerExpression %= integerPlusExpression;
 		integerExpression.name("integer expression");
@@ -97,9 +97,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		// This block defines all expressions of integral type that are by syntax constant. That is, they are evaluable given the values for all constants.
 		constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
 		constantAtomicIntegerExpression.name("constant integer expression");
-		constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+		constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
 		constantIntegerMultExpression.name("constant integer expression");
-		constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+		constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
 		constantIntegerPlusExpression.name("constant integer expression");
 		constantIntegerExpression %= constantIntegerPlusExpression;
 		constantIntegerExpression.name("constant integer expression");
@@ -107,9 +107,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		// This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants.
 		constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression);
 		constantAtomicDoubleExpression.name("constant double expression");
-		constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+		constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
 		constantDoubleMultExpression.name("constant double expression");
-		constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+		constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
 		constantDoublePlusExpression.name("constant double expression");
 		constantDoubleExpression %= constantDoublePlusExpression;
 		constantDoubleExpression.name("constant double expression");
@@ -119,7 +119,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		relativeExpression.name("boolean expression");
 		atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression);
 		atomicBooleanExpression.name("boolean expression");
-		notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
+		notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::NOT))];
 		notExpression.name("boolean expression");
 		andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
 		andExpression.name("boolean expression");
@@ -133,7 +133,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		constantRelativeExpression.name("constant boolean expression");
 		constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
 		constantAtomicBooleanExpression.name("constant boolean expression");
-		constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
+		constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::NOT))];
 		constantNotExpression.name("constant boolean expression");
 		constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
 		constantAndExpression.name("constant boolean expression");
@@ -175,11 +175,11 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		unassignedLocalIntegerVariableName.name("unassigned local integer variable");
 
 		// This block defines all entities that are needed for parsing a single command.
-		assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))];
+		assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))];
 		assignmentDefinition.name("assignment");
-		assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&";
+		assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
 		assignmentDefinitionList.name("assignment list");
-		updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a))[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_a)];
+		updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_a, qi::_b)];
 		updateDefinition.name("update");
 		updateListDefinition = +updateDefinition % "+";
 		updateListDefinition.name("update list");
@@ -187,15 +187,15 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		commandDefinition.name("command");
 
 		// This block defines all entities that are neede for parsing variable definitions.
-		booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::BooleanVariable>>(qi::_1, phoenix::construct<storm::ir::BooleanVariable>(phoenix::val(qi::_1), qi::_b))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1)];
+		booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::BooleanVariable>(phoenix::val(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::val(nextBooleanVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::bool_, phoenix::val(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex)++];
 		booleanVariableDefinition.name("boolean variable declaration");
-		integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::IntegerVariable>>(qi::_1, phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3, qi::_b))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1)];
+		integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::IntegerVariable>(phoenix::val(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::val(nextIntegerVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::int_, phoenix::val(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex)++];
 		integerVariableDefinition.name("integer variable declaration");
-		variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2));
+		variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4));
 		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)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_a, qi::_b, 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<storm::ir::Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
 		moduleDefinition.name("module");
 		moduleDefinitionList %= +moduleDefinition;
 		moduleDefinitionList.name("module list");
@@ -234,19 +234,19 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 	qi::rule<Iterator, std::vector<storm::ir::Module>(), Skipper> moduleDefinitionList;
 
 	// Rules for module definition.
-	qi::rule<Iterator, storm::ir::Module(), qi::locals<std::map<std::string, storm::ir::BooleanVariable>, std::map<std::string, storm::ir::IntegerVariable>>, Skipper> moduleDefinition;
+	qi::rule<Iterator, storm::ir::Module(), qi::locals<std::vector<storm::ir::BooleanVariable>, std::vector<storm::ir::IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
 
 	// Rules for variable definitions.
-	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::BooleanVariable>&, std::map<std::string, storm::ir::IntegerVariable>&), Skipper> variableDefinition;
-	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::BooleanVariable>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> booleanVariableDefinition;
-	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::IntegerVariable>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> integerVariableDefinition;
+	qi::rule<Iterator, qi::unused_type(std::vector<storm::ir::BooleanVariable>&, std::vector<storm::ir::IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
+	qi::rule<Iterator, qi::unused_type(std::vector<storm::ir::BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> booleanVariableDefinition;
+	qi::rule<Iterator, qi::unused_type(std::vector<storm::ir::IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> integerVariableDefinition;
 
 	// Rules for command definitions.
 	qi::rule<Iterator, storm::ir::Command(), qi::locals<std::string>, Skipper> commandDefinition;
 	qi::rule<Iterator, std::vector<storm::ir::Update>(), Skipper> updateListDefinition;
-	qi::rule<Iterator, storm::ir::Update(), qi::locals<std::map<std::string, storm::ir::Assignment>>, Skipper> updateDefinition;
-	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinitionList;
-	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinition;
+	qi::rule<Iterator, storm::ir::Update(), qi::locals<std::map<std::string, storm::ir::Assignment>, std::map<std::string, storm::ir::Assignment>>, Skipper> updateDefinition;
+	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&, std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinitionList;
+	qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&, std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinition;
 
 	// Rules for variable/command names.
 	qi::rule<Iterator, std::string(), Skipper> integerVariableName;
@@ -377,6 +377,10 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
 		}
 	} relations_;
 
+	// Used for indexing the variables.
+	uint_fast64_t nextBooleanVariableIndex;
+	uint_fast64_t nextIntegerVariableIndex;
+
 	// Structures mapping variable and constant names to the corresponding expression nodes of
 	// the intermediate representation.
 	struct qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> integerVariables_, booleanVariables_;

src/storm.cpp

@@ -36,6 +36,7 @@
 #include "log4cplus/fileappender.h"
 
 #include "src/parser/PrismParser.h"
+#include "src/adapters/IntermediateRepresentationAdapter.h"
 
 #include "src/exceptions/InvalidSettingsException.h"
 
@@ -241,7 +242,8 @@ int main(const int argc, const char* argv[]) {
 	// testChecking();
 
 	storm::parser::PrismParser parser;
-	parser.parseFile("test.input");
+	std::shared_ptr<storm::ir::Program> program = parser.parseFile("test.input");
+	storm::storage::SquareSparseMatrix<double>* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix<double>(*program);
 
 	cleanUp();
 	return 0;

test.input

@@ -1,24 +1,24 @@
+// Knuth's model of a fair die using only fair coins
 dtmc
 
 module die
-// local state
-s : [0..7] init 0;
-// value of the dice
-d : [0..6] init 0;
+
+	// local state
+	s : [0..7] init 0;
+	// value of the dice
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> 1: (s'=7);
 	
-[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
-[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
-[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
-[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
-[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
-[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
-[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
-[] s=7 -> 1 : (s'=7);
 endmodule
 
 rewards "coin_flips"
 	[] s<7 : 1;
-	s>3 : 1;
 endrewards
-
-label test = s>2;