Changed internal data structures of PRISM classes slightly. Added classs for certain ingredients that were represented as primitives before.

Former-commit-id: bdc61e88a5

src/parser/PrismParser.cpp

@@ -1,13 +1,4 @@
-/*
- * PrismParser.cpp
- *
- *  Created on: 11.01.2013
- *      Author: chris
- */
-
-#include "PrismParser.h"
-
-#include "src/utility/OsDetection.h"
+#include "src/parser/PrismParser.h"
 
 #include "src/parser/prismparser/PrismGrammar.h"
 
@@ -21,108 +12,87 @@
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
-extern log4cplus::Logger logger;
-
+#include "log4cplus/consoleappender.h"
+#include "log4cplus/fileappender.h"
+log4cplus::Logger logger;
 
 namespace storm {
-namespace parser {
-
-/*!
- * Opens the given file for parsing, invokes the helper function to parse the actual content and
- * closes the file properly, even if an exception is thrown in the parser. In this case, the
- * exception is passed on to the caller.
- */
-storm::ir::Program PrismParserFromFile(std::string const& filename) {
-	// Open file and initialize result.
-	std::ifstream inputFileStream(filename, std::ios::in);
-	storm::ir::Program result;
-
-	// Now try to parse the contents of the file.
-	try {
-		result = PrismParser(inputFileStream, filename);
-	} catch(std::exception& e) {
-		// In case of an exception properly close the file before passing exception.
-		inputFileStream.close();
-		throw e;
-	}
-
-	// Close the stream in case everything went smoothly and return result.
-	inputFileStream.close();
-	return result;
-}
-
-/*!
- * Passes iterators to the input stream to the Boost spirit parser and thereby parses the input.
- * If the parser throws an expectation failure exception, i.e. expected input different than the one
- * provided, this is caught and displayed properly before the exception is passed on.
- */
-storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename) {
-	// Prepare iterators to input.
-	// TODO: Right now, this parses the whole contents of the file into a string first.
-	// While this is usually not necessary, because there exist adapters that make an input stream
-	// iterable in both directions without storing it into a string, using the corresponding
-	// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
-	std::string fileContent((std::istreambuf_iterator<char>(inputStream)), (std::istreambuf_iterator<char>()));
-	BaseIteratorType stringIteratorBegin = fileContent.begin();
-	BaseIteratorType stringIteratorEnd = fileContent.end();
-	PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename);
-	PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename);
-	PositionIteratorType positionIteratorEnd;
-
-	// Prepare resulting intermediate representation of input.
-	storm::ir::Program result;
-
-	// In order to instantiate the grammar, we have to pass the type of the skipping parser.
-	// As this is more complex, we let Boost figure out the actual type for us.
-	prism::PrismGrammar grammar;
-	try {
-		// Now parse the content using phrase_parse in order to be able to supply a skipping parser.
-		// First run.
-		LOG4CPLUS_INFO(logger, "Start parsing...");
-		qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
-		grammar.prepareForSecondRun();
-		result = storm::ir::Program();
-		LOG4CPLUS_INFO(logger, "Start second parsing run...");
-		// Second run.
-		qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
-		LOG4CPLUS_INFO(logger, "Finished parsing, here is the parsed program:" << std::endl << result.toString());
-		// Reset grammars.
-		grammar.resetGrammars();
-	} catch(const qi::expectation_failure<PositionIteratorType>& e) {
-		// If the parser expected content different than the one provided, display information
-		// about the location of the error.
-		const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
-
-		// Construct the error message including a caret display of the position in the
-		// erroneous line.
-		std::stringstream msg;
-		std::string line = e.first.get_currentline();
-		while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," ");
-		msg << pos.file << ", line " << pos.line << ", column " << pos.column
+    namespace parser {
+        storm::prism::Program PrismParserFromFile(std::string const& filename) {
+            // Open file and initialize result.
+            std::ifstream inputFileStream(filename, std::ios::in);
+            storm::prism::Program result;
+            
+            // Now try to parse the contents of the file.
+            try {
+                result = PrismParser(inputFileStream, filename);
+            } catch(std::exception& e) {
+                // In case of an exception properly close the file before passing exception.
+                inputFileStream.close();
+                throw e;
+            }
+            
+            // Close the stream in case everything went smoothly and return result.
+            inputFileStream.close();
+            return result;
+        }
+        
+        storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename) {
+            // Prepare iterators to input.
+            // TODO: Right now, this parses the whole contents of the file into a string first.
+            // While this is usually not necessary, because there exist adapters that make an input stream
+            // iterable in both directions without storing it into a string, using the corresponding
+            // Boost classes gives an awful output under valgrind and is thus disabled for the time being.
+            std::string fileContent((std::istreambuf_iterator<char>(inputStream)), (std::istreambuf_iterator<char>()));
+            BaseIteratorType stringIteratorBegin = fileContent.begin();
+            BaseIteratorType stringIteratorEnd = fileContent.end();
+            PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename);
+            PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename);
+            PositionIteratorType positionIteratorEnd;
+            
+            // Prepare resulting intermediate representation of input.
+            storm::prism::Program result;
+            
+            // In order to instantiate the grammar, we have to pass the type of the skipping parser.
+            // As this is more complex, we let Boost figure out the actual type for us.
+            storm::parser::prism::PrismGrammar grammar;
+            try {
+                // Now parse the content using phrase_parse in order to be able to supply a skipping parser.
+                // First run.
+                LOG4CPLUS_INFO(logger, "Start parsing...");
+                qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
+                LOG4CPLUS_INFO(logger, "Finished parsing, here is the parsed program:" << std::endl << result);
+
+            } catch(const qi::expectation_failure<PositionIteratorType>& e) {
+                // If the parser expected content different than the one provided, display information
+                // about the location of the error.
+                const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
+                
+                // Construct the error message including a caret display of the position in the
+                // erroneous line.
+                std::stringstream msg;
+                std::string line = e.first.get_currentline();
+                while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," ");
+                msg << pos.file << ", line " << pos.line << ", column " << pos.column
 				<< ": parse error: expected " << e.what_ << std::endl << "\t"
 				<< line << std::endl << "\t";
-		int i = 0;
-		for (i = 1; i < pos.column; ++i) {
-			msg << "-";
-		}
-		msg << "^";
-		for (; i < 80; ++i) {
-			msg << "-";
-		}
-		msg << std::endl;
-
-		std::cerr << msg.str();
-		
-		// Reset grammars in any case.
-		grammar.resetGrammars();
-
-		// Now propagate exception.
-		throw storm::exceptions::WrongFormatException() << msg.str();
-	}
-
-	return result;
-}
-
-} // namespace parser
-
+                int i = 0;
+                for (i = 1; i < pos.column; ++i) {
+                    msg << "-";
+                }
+                msg << "^";
+                for (; i < 80; ++i) {
+                    msg << "-";
+                }
+                msg << std::endl;
+                
+                std::cerr << msg.str();
+                
+                // Now propagate exception.
+                throw storm::exceptions::WrongFormatException() << msg.str();
+            }
+            
+            return result;
+        }
+    } // namespace parser
 } // namespace storm

src/parser/prismparser/PrismGrammar.cpp

@@ -46,146 +46,108 @@ namespace storm {
                 atomicNumericalExpression %= minMaxExpression | floorCeilExpression | numericalVariableExpression | qi::lit("(") >> numericalExpression >> qi::lit(")");
                 atomicNumericalExpression.name("numerical expression");
                 
-                minMaxExpression %= ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(",") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::minimum, qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::maximum, qi::_1, qi::_2)]];
+                minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(",") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::minimum, qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::maximum, qi::_1, qi::_2)]];
                 minMaxExpression.name("min/max expression");
                 
-                floorCeilExpression %= ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::floor, qi::_1)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::ceil, qi::_1)]];
+                floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::floor, qi::_1)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::ceil, qi::_1)]];
                 floorCeilExpression.name("integer floor/ceil expression");
 
                 numericalVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleVariable, qi::_1)];
                 numericalVariableExpression.name("numerical variable");
                 
-                // Parse a model type.
                 modelTypeDefinition = modelType_;
                 modelTypeDefinition.name("model type");
+                
+                undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r1) | undefinedDoubleConstantDefinition(qi::_r1));
+                undefinedConstantDefinition.name("undefined constant definition");
 
-                programHeader =         modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1]
-                                >   *(  undefinedConstantDefinition(qi::_r1)
-                                    |   definedConstantDefinition(qi::_r1)
-                                    |   formulaDefinition(qi::_r1)
-                                    |   globalVariableDefinition(qi::_r1)
-                                    );
-                programHeader.name("program header");
+                undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, phoenix::bind(&GlobalProgramInformation::undefinedBooleanConstants, qi::_r1), qi::_1)];
+                undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
 
-                // This block defines all entities that are needed for parsing global variable definitions.
-                globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
-                globalVariableDefinitionList.name("global variable declaration list");
+                undefinedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, phoenix::bind(&GlobalProgramInformation::undefinedIntegerConstants, qi::_r1), qi::_1)];
+                undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
                 
-                // This block defines all entities that are needed for parsing constant definitions.
-                definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
+                undefinedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, phoenix::bind(&GlobalProgramInformation::undefinedDoubleConstants, qi::_r1), qi::_1)];
+                undefinedDoubleConstantDefinition.name("undefined double constant definition");
+
+                definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r1) | definedDoubleConstantDefinition(qi::_r1));
+                definedConstantDefinition.name("defined constant definition");
+
+                definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedBooleanConstant, phoenix::bind(&GlobalProgramInformation::definedBooleanConstants, qi::_r1), qi::_1, qi::_2)];
                 definedBooleanConstantDefinition.name("defined boolean constant declaration");
-                
-                definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
+
+                definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedIntegerConstant, phoenix::bind(&GlobalProgramInformation::definedIntegerConstants, qi::_r1), qi::_1, qi::_2)];
                 definedIntegerConstantDefinition.name("defined integer constant declaration");
-                definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
+
+                definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedDoubleConstant, phoenix::bind(&GlobalProgramInformation::definedDoubleConstants, qi::_r1), qi::_1, qi::_2)];
                 definedDoubleConstantDefinition.name("defined double constant declaration");
-                undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)];
-                undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
-                undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)];
-                undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
-                undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)];
-                undefinedDoubleConstantDefinition.name("undefined double constant definition");
-                definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r2) | definedDoubleConstantDefinition(qi::_r3));
-                definedConstantDefinition.name("defined constant definition");
-                undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
-                undefinedConstantDefinition.name("undefined constant definition");
                 
-                // Parse the ingredients of a probabilistic program.
-                start = (qi::eps >
-                         programHeader(qi::_a) >
-                         formulaDefinitionList >
-                         globalVariableDefinitionList(qi::_d) >
-                         moduleDefinitionList >
-                         rewardDefinitionList(qi::_e) >
-                         labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
-                start.name("probabilistic program declaration");
-
+                formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addFormula, phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1, qi::_2)];
+                formulaDefinition.name("formula definition");
                 
-                labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))
-                [phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)];
-                labelDefinition.name("label declaration");
-                labelDefinitionList %= *labelDefinition(qi::_r1);
-                labelDefinitionList.name("label declaration list");
+                globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1)) | integerVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1))));
+                globalVariableDefinition.name("global variable declaration list");
                 
-                // This block defines all entities that are needed for parsing a reward model.
-                stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)];
+                programHeader =         modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1]
+                                >   *(  undefinedConstantDefinition(qi::_r1)
+                                    |   definedConstantDefinition(qi::_r1)
+                                    |   formulaDefinition(qi::_r1)
+                                    |   globalVariableDefinition(qi::_r1)
+                                    );
+                programHeader.name("program header");
+ 
+                rewardModelDefinition = (qi::lit("rewards") > qi::lit("\"") > identifier > qi::lit("\"")
+                                         > +(   stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)]
+                                            |   transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]
+                                            )
+                                         >> qi::lit("endrewards"))[phoenix::bind(&PrismGrammar::addRewardModel, phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_r1), qi::_1, qi::_a, qi::_b)];
+                rewardModelDefinition.name("reward model definition");
+                
+                stateRewardDefinition = (booleanExpression > qi::lit(":") > numericalExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createStateReward, qi::_1, qi::_2)];
                 stateRewardDefinition.name("state reward definition");
-                transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)];
+                
+                transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createTransitionReward, qi::_a, qi::_2, qi::_3)];
                 transitionRewardDefinition.name("transition reward definition");
-                rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))
-                [phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)];
-                rewardDefinition.name("reward definition");
-                rewardDefinitionList = *rewardDefinition(qi::_r1);
-                rewardDefinitionList.name("reward definition list");
-                
-                commandName %= this->state->commandNames_;
-                commandName.name("command name");
-                unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_;
-                unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable");
-                unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_;
-                unassignedLocalIntegerVariableName.name("unassigned local/global integer variable");
-                
-                // This block defines all entities that are needed for parsing a single command.
-                assignmentDefinition =
-                (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntegerAssignment, this, qi::_1, qi::_2, qi::_r2)] |
-                (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBooleanAssignment, this, qi::_1, qi::_2, qi::_r1)];
+
+                labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > booleanExpression >> qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addLabel, phoenix::bind(&GlobalProgramInformation::labels, qi::_r1), qi::_1, qi::_2)];
+                labelDefinition.name("label definition");
+
+                assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_pass = phoenix::bind(&PrismGrammar::addAssignment, qi::_r1, qi::_1, qi::_2)];
                 assignmentDefinition.name("assignment");
-                assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
+                assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&";
                 assignmentDefinitionList.name("assignment list");
-                updateDefinition = (((ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(":"))
-                                     | qi::attr(std::shared_ptr<BaseExpression>(new storm::ir::expressions::DoubleLiteralExpression(1))))[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))]
-                                    >> assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
+                
+                moduleDefinitionList %= +(moduleDefinition(qi::_r1) | moduleRenaming(qi::_r1));
+                moduleDefinitionList.name("module list");
+
+                updateDefinition = (((numericalExpression >> qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList(qi::_a))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, qi::_1, qi::_a)];
                 updateDefinition.name("update");
-                updateListDefinition = +updateDefinition % "+";
+                
+                updateListDefinition %= +updateDefinition % "+";
                 updateListDefinition.name("update list");
-                commandDefinition = (
-                                     qi::lit("[") > -(
-                                                      (FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]
-                                                      ) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";")
-                                     )[qi::_val = phoenix::bind(&PrismGrammar::createCommand, this, qi::_a, qi::_2, qi::_3)];
-                commandDefinition.name("command");
-                
-                // This block defines all entities that are needed for parsing variable definitions.
-                booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
-                [phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
-                booleanVariableDefinition.name("boolean variable declaration");
-                
-                integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
-                [phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
-                integerVariableDefinition.name("integer variable declaration");
-                variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false));
-                variableDefinition.name("variable declaration");
                 
-                // This block defines all entities that are needed for parsing a module.
-                moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::clearLocalVariables, *this->state)]
-                                    >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
-                [qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
-                
-                moduleDefinition.name("module");
-                moduleRenaming = (qi::lit("module")	>> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=")
-                                  > this->state->moduleNames_ > qi::lit("[") > *(
-                                                                                 (IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
-                                                                                 ) > qi::lit("]") > qi::lit("endmodule"))
-                [qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
-                moduleRenaming.name("renamed module");
-                moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
-                moduleDefinitionList.name("module list");
+                commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createCommand, qi::_a, qi::_2, qi::_3)];
+                commandDefinition.name("command definition");
+
+                booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > booleanExpression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addBooleanVariable, qi::_r1, qi::_1, qi::_2)];
+                booleanVariableDefinition.name("boolean variable definition");
                 
+                integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")) > numericalExpression[qi::_a = qi::_1] > qi::lit("..") > numericalExpression > qi::lit("]") > -(qi::lit("init") > numericalExpression[qi::_a = qi::_1]) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addIntegerVariable, qi::_r1, qi::_1, qi::_2, qi::_3, qi::_a)];
+                integerVariableDefinition.name("integer variable definition");
                 
-                constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)];
-                constantBooleanFormulaDefinition.name("constant boolean formula definition");
-                booleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->booleanFormulas_.add, qi::_1, qi::_2)];
-                booleanFormulaDefinition.name("boolean formula definition");
-                constantIntegerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantIntegerFormulas_.add, qi::_1, qi::_2)];
-                constantIntegerFormulaDefinition.name("constant integer formula definition");
-                integerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> IntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerFormulas_.add, qi::_1, qi::_2)];
-                integerFormulaDefinition.name("integer formula definition");
-                constantDoubleFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantDoubleFormulas_.add, qi::_1, qi::_2)];
-                constantDoubleFormulaDefinition.name("constant double formula definition");
-                formulaDefinition = constantBooleanFormulaDefinition | booleanFormulaDefinition | constantIntegerFormulaDefinition | integerFormulaDefinition | constantDoubleFormulaDefinition;
-                formulaDefinition.name("formula definition");
-                formulaDefinitionList = *formulaDefinition;
-                formulaDefinitionList.name("formula definition list");
+                variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2));
+                variableDefinition.name("variable declaration");
+
+                moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createModule, qi::_1, qi::_a, qi::_b, qi::_2)];
+                moduleDefinition.name("module definition");
+                
+                moduleRenaming = ((qi::lit("module")	>> identifier >> qi::lit("=")) > identifier > qi::lit("[")
+                                  > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] % ",") > qi::lit("]")
+                                  > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createRenamedModule, qi::_1, qi::_2, qi::_a, qi::_r1)];
+                moduleRenaming.name("module definition via renaming");
+                
+                start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(rewardModelDefinition(qi::_a) | labelDefinition(qi::_a)))[qi::_val = phoenix::bind(&PrismGrammar::createProgram, qi::_a, qi::_1)];
+                start.name("probabilistic program");
             }
         } // namespace prism
     } // namespace parser

src/parser/prismparser/PrismGrammar.h

@@ -16,7 +16,6 @@
 
 namespace qi = boost::spirit::qi;
 namespace phoenix = boost::phoenix;
-namespace prism = storm::prism;
 
 typedef std::string::const_iterator BaseIteratorType;
 typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
@@ -25,22 +24,51 @@ typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_
 typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
 typedef boost::spirit::unused_type Unused;
 
-#include "src/parser/prismparser/Tokens.h"
-
 #include "src/storage/prism/Program.h"
 #include "src/storage/expressions/Expression.h"
-using namespace storm::expressions;
 
 namespace storm {
     namespace parser {
         namespace prism {
+            
+            struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
+                modelTypeStruct() {
+                    add
+                    ("dtmc", storm::prism::Program::ModelType::DTMC)
+                    ("ctmc", storm::prism::Program::ModelType::CTMC)
+                    ("mdp", storm::prism::Program::ModelType::MDP)
+                    ("ctmdp", storm::prism::Program::ModelType::CTMDP)
+                    ("ma", storm::prism::Program::ModelType::MA);
+                }
+            };
+            
+            struct keywordsStruct : qi::symbols<char, unsigned> {
+                keywordsStruct() {
+                    add
+                    ("dtmc", 1)
+                    ("ctmc", 2)
+                    ("mdp", 3)
+                    ("ctmdp", 4)
+                    ("ma", 5)
+                    ("const", 6)
+                    ("int", 7)
+                    ("bool", 8)
+                    ("module", 9)
+                    ("endmodule", 10)
+                    ("rewards", 11)
+                    ("endrewards", 12)
+                    ("true", 13)
+                    ("false", 14);
+                }
+            };
+            
             class GlobalProgramInformation {
             public:
                 // Default construct the header information.
                 GlobalProgramInformation() = default;
                 
                 // Members for all essential information that needs to be collected.
-                prism::Program::ModelType modelType;
+                storm::prism::Program::ModelType modelType;
                 std::set<std::string> undefinedBooleanConstants;
                 std::set<std::string> undefinedIntegerConstants;
                 std::set<std::string> undefinedDoubleConstants;
@@ -48,13 +76,18 @@ namespace storm {
                 std::map<std::string, storm::expressions::Expression> definedIntegerConstants;
                 std::map<std::string, storm::expressions::Expression> definedDoubleConstants;
                 std::map<std::string, storm::expressions::Expression> formulas;
-                std::map<std::string, BooleanVariable> globalBooleanVariables;
-                std::map<std::string, IntegerVariable> globalIntegerVariables;
-                std::map<std::string, Module> modules;
-                std::map<std::string, RewardModel> rewardModels;
+                std::map<std::string, storm::prism::BooleanVariable> globalBooleanVariables;
+                std::map<std::string, storm::prism::IntegerVariable> globalIntegerVariables;
+                std::map<std::string, storm::prism::Module> modules;
+                std::map<std::string, storm::prism::RewardModel> rewardModels;
+                std::map<std::string, storm::expressions::Expression> labels;
+                
+                // Counters to provide unique indexing for commands and updates.
+                uint_fast64_t currentCommandIndex;
+                uint_fast64_t currentUpdateIndex;
             };
             
-            class PrismGrammar : public qi::grammar<Iterator, Program(), qi::locals<GlobalProgramInformation>, Skipper> {
+            class PrismGrammar : public qi::grammar<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> {
             public:
                 /*!
                  * Default constructor that creates an empty and functional grammar.
@@ -63,46 +96,48 @@ namespace storm {
                 
             private:
                 // The starting point of the grammar.
-                qi::rule<Iterator, Program(), qi::locals<GlobalProgramInformation>, Skipper> start;
+                qi::rule<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> start;
                 
                 // Rules for model type.
-                qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
+                qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;
                 
                 // Rules for parsing the program header.
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> programHeader;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedConstantDefinition;
-                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedConstantDefinition;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedBooleanConstantDefinition;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedIntegerConstantDefinition;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedDoubleConstantDefinition;
+                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedConstantDefinition;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedBooleanConstantDefinition;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedIntegerConstantDefinition;
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedDoubleConstantDefinition;
                 
                 // Rules for global variable definitions.
-                qi::rule<Iterator, qi::unused_type(ProgramHeaderInformation&), Skipper> globalVariableDefinition;
+                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalVariableDefinition;
+                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalBooleanVariableDefinition;
+                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalIntegerVariableDefinition;
                 
                 // Rules for modules definition.
-                qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
-                qi::rule<Iterator, Module(), qi::locals<std::map<std::string, BooleanVariable>, std::map<std::string, IntegerVariable>>, Skipper> moduleDefinition;
-                qi::rule<Iterator, Module(GlobalProgramInformation&>, Skipper> moduleRenaming;
+                qi::rule<Iterator, std::vector<storm::prism::Module>(GlobalProgramInformation&), Skipper> moduleDefinitionList;
+                qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, storm::prism::BooleanVariable>, std::map<std::string, storm::prism::IntegerVariable>>, Skipper> moduleDefinition;
+                qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
                 
                 // Rules for variable definitions.
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&, std::map<std::string, IntegerVariable>&), Skipper> variableDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&), Skipper> booleanVariableDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, IntegerVariable>&), Skipper> integerVariableDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::BooleanVariable>&, std::map<std::string, storm::prism::IntegerVariable>&), Skipper> variableDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::BooleanVariable>&), Skipper> booleanVariableDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::IntegerVariable>&), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
                 
                 // Rules for command definitions.
-                qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
-                qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
-                qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>>, Skipper> updateDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
-                qi::rule<Iterator, Assignment(), Skipper> assignmentDefinition;
+                qi::rule<Iterator, storm::prism::Command(), qi::locals<std::string>, Skipper> commandDefinition;
+                qi::rule<Iterator, std::vector<storm::prism::Update>(), Skipper> updateListDefinition;
+                qi::rule<Iterator, storm::prism::Update(), qi::locals<std::map<std::string, storm::prism::Assignment>>, Skipper> updateDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::Assignment>&), Skipper> assignmentDefinitionList;
+                qi::rule<Iterator, storm::prism::Assignment(std::map<std::string, storm::prism::Assignment>&), Skipper> assignmentDefinition;
                 
                 // Rules for reward definitions.
-                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardModelDefinition;
-                qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
-                qi::rule<Iterator, TransitionReward(), Skipper> transitionRewardDefinition;
+                qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
+                qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition;
+                qi::rule<Iterator, storm::prism::TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
                 
                 // Rules for label definitions.
                 qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> labelDefinition;
@@ -130,17 +165,35 @@ namespace storm {
                 qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
                 qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
                 
-                // Parsers that recognize special keywords and operations.
+                // Parsers that recognize special keywords and model types.
                 storm::parser::prism::keywordsStruct keywords_;
                 storm::parser::prism::modelTypeStruct modelType_;
-                storm::parser::prism::BinaryRelationOperatorStruct relationOperator_;
-                storm::parser::prism::BinaryBooleanOperatorStruct binaryBooleanOperator_;
-                storm::parser::prism::UnaryBooleanOperatorStruct unaryBooleanOperator_;
-                storm::parser::prism::BinaryNumericalOperatorStruct binaryNumericalOperator_;
-                storm::parser::prism::UnaryNumericalOperatorStruct unaryNumericalOperator_;
                 
                 // Helper methods that add data to data structures.
+                static bool addUndefinedBooleanConstant(std::set<std::string>& undefinedBooleanConstants, std::string const& newUndefinedBooleanConstant);
+                static bool addUndefinedIntegerConstant(std::set<std::string>& undefinedIntegerConstants, std::string const& newUndefinedIntegerConstant);
+                static bool addUndefinedDoubleConstant(std::set<std::string>& undefinedDoubleConstants, std::string const& newUndefinedDoubleConstant);
                 
+                static bool addDefinedBooleanConstant(std::map<std::string, storm::expressions::Expression>& definedBooleanConstants, std::string const& newDefinedBooleanConstant, storm::expressions::Expression expression);
+                static bool addDefinedIntegerConstant(std::map<std::string, storm::expressions::Expression>& definedIntegerConstants, std::string const& newDefinedIntegerConstant, storm::expressions::Expression expression);
+                static bool addDefinedDoubleConstant(std::map<std::string, storm::expressions::Expression>& definedDoubleConstants, std::string const& newDefinedDoubleConstant, storm::expressions::Expression expression);
+
+                static bool addFormula(std::map<std::string, storm::expressions::Expression>& formulas, std::string const& formulaName, storm::expressions::Expression expression);
+                
+                static storm::prism::RewardModel addRewardModel(std::map<std::string, storm::prism::RewardModel>& rewardModels, std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards);
+                static storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression);
+                static storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression);
+                
+                static bool addLabel(std::map<std::string, storm::expressions::Expression>& labels, std::string const& labelName, storm::expressions::Expression expression);
+                
+                static bool addAssignment(std::map<std::string, storm::prism::Assignment>& assignments, std::string const& variableName, storm::expressions::Expression assignedExpression);
+                static storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::map<std::string, storm::prism::Assignment>& assignments);
+                static storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates);
+                static bool addBooleanVariable(std::map<std::string, storm::prism::BooleanVariable>& booleanVariables, std::string const& variableName, storm::expressions::Expression initialValueExpression);
+                static bool addIntegerVariable(std::map<std::string, storm::prism::IntegerVariable>& integerVariables, std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression);
+                static storm::prism::Module createModule(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands);
+                static storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation const& globalProgramInformation);
+                static storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation, std::vector<storm::prism::Module> const& modules);
             };
         } // namespace prism
     } // namespace parser

src/parser/prismparser/Tokens.h

@@ -1,113 +0,0 @@
-#ifndef STORM_PARSER_PRISMPARSER_TOKENS_H_
-#define	STORM_PARSER_PRISMPARSER_TOKENS_H_
-
-#include "src/storage/prism/Program.h"
-#include "src/storage/expressions/Expressions.h"
-
-namespace storm {
-    namespace parser {
-        namespace prism {
-            /*!
-             * A structure mapping the textual representation of a model type to the model type
-             * representation of the intermediate representation.
-             */
-            struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
-                modelTypeStruct() {
-                    add
-                    ("dtmc", storm::prism::Program::ModelType::DTMC)
-                    ("ctmc", storm::prism::Program::ModelType::CTMC)
-                    ("mdp", storm::prism::Program::ModelType::MDP)
-                    ("ctmdp", storm::prism::Program::ModelType::CTMDP)
-                    ("ma", storm::prism::Program::ModelType::MA);
-                }
-            };
-            
-            /*!
-             * A structure defining the keywords that are not allowed to be chosen as identifiers.
-             */
-            struct keywordsStruct : qi::symbols<char, unsigned> {
-                keywordsStruct() {
-                    add
-                    ("dtmc", 1)
-                    ("ctmc", 2)
-                    ("mdp", 3)
-                    ("ctmdp", 4)
-                    ("ma", 5)
-                    ("const", 6)
-                    ("int", 7)
-                    ("bool", 8)
-                    ("module", 9)
-                    ("endmodule", 10)
-                    ("rewards", 11)
-                    ("endrewards", 12)
-                    ("true", 13)
-                    ("false", 14);
-                }
-            };
-            
-            /*!
-             * A structure mapping the textual representation of binary relations to the corresponding enum values.
-             */
-            struct BinaryRelationOperatorStruct : qi::symbols<char, storm::expressions::BinaryRelationExpression::RelationType> {
-                BinaryRelationOperatorStruct() {
-                    add
-                    ("=", storm::expressions::BinaryRelationExpression::RelationType::Equal)
-                    ("!=", storm::expressions::BinaryRelationExpression::RelationType::NotEqual)
-                    ("<", storm::expressions::BinaryRelationExpression::RelationType::Less)
-                    ("<=", storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual)
-                    (">", storm::expressions::BinaryRelationExpression::RelationType::Greater)
-                    (">=", storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual);
-                }
-            };
-            
-            /*!
-             * A structure mapping the textual representation of binary operators to the corresponding enum values.
-             */
-            struct BinaryBooleanOperatorStruct : qi::symbols<char, storm::expressions::BinaryBooleanFunctionExpression::OperatorType> {
-                BinaryBooleanOperatorStruct() {
-                    add
-                    ("&", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And)
-                    ("|", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or)
-                    ("=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies)
-                    ("<=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff);
-                }
-            };
-
-            /*!
-             * A structure mapping the textual representation of binary operators to the corresponding enum values.
-             */
-            struct UnaryBooleanOperatorStruct : qi::symbols<char, storm::expressions::UnaryBooleanFunctionExpression::OperatorType> {
-                UnaryBooleanOperatorStruct() {
-                    add
-                    ("!", storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not);
-                }
-            };
-            
-            /*!
-             * A structure mapping the textual representation of binary boolean operators to the corresponding enum values.
-             */
-            struct BinaryNumericalOperatorStruct : qi::symbols<char, storm::expressions::BinaryNumericalFunctionExpression::OperatorType> {
-                BinaryNumericalOperatorStruct() {
-                    add
-                    ("+", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus)
-                    ("-", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus)
-                    ("*", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times)
-                    ("/", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide);
-                }
-            };
-            
-            /*!
-             * A structure mapping the textual representation of binary operators to the corresponding enum values.
-             */
-            struct UnaryNumericalOperatorStruct : qi::symbols<char, storm::expressions::UnaryNumericalFunctionExpression::OperatorType> {
-                UnaryNumericalOperatorStruct() {
-                    add
-                    ("!", storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus);
-                }
-            };
-        }
-    }
-}
-
-#endif	/* STORM_PARSER_PRISMPARSER_TOKENS_H_ */
-

src/storage/prism/Constant.cpp

@@ -0,0 +1,43 @@
+#include "src/storage/prism/Constant.h"
+
+namespace storm {
+    namespace prism {
+        Constant::Constant(ConstantType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(true), expression(expression) {
+            // Intentionally left empty.
+        }
+        
+        Constant::Constant(ConstantType constantType, std::string const& constantName, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(false), expression() {
+            // Intentionally left empty.
+        }
+        
+        std::string const& Constant::getConstantName() const {
+            return this->constantName;
+        }
+        
+        Constant::ConstantType Constant::getConstantType() const {
+            return this->constantType;
+        }
+        
+        bool Constant::isDefined() const {
+            return this->defined;
+        }
+        
+        storm::expressions::Expression const& Constant::getExpression() const {
+            return this->expression;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
+            stream << "const ";
+            switch (constant.getConstantType()) {
+                case Constant::ConstantType::Bool: stream << "bool "; break;
+                case Constant::ConstantType::Integer: stream << "int "; break;
+                case Constant::ConstantType::Double: stream << "double "; break;
+            }
+            stream << constant.getConstantName();
+            if (constant.isDefined()) {
+                stream << " = " << constant.getExpression() << ";";
+            }
+            return stream;
+        }
+    }
+}

src/storage/prism/Constant.h

@@ -0,0 +1,91 @@
+#ifndef STORM_STORAGE_PRISM_CONSTANT_H_
+#define STORM_STORAGE_PRISM_CONSTANT_H_
+
+#include "src/storage/prism/LocatedInformation.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace prism {
+        class Constant : public LocatedInformation {
+        public:
+            /*!
+             * The possible constant types.
+             */
+            enum class ConstantType {Bool, Integer, Double};
+            
+            /*!
+             * Creates a constant with the given type, name and defining expression.
+             *
+             * @param constantType The type of the constant.
+             * @param constantName The name of the constant.
+             * @param expression The expression that defines the constant.
+             * @param filename The filename in which the transition reward is defined.
+             * @param lineNumber The line number in which the transition reward is defined.
+             */
+            Constant(ConstantType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+
+            /*!
+             * Creates an undefined constant with the given type and name.
+             *
+             * @param constantType The type of the constant.
+             * @param constantName The name of the constant.
+             * @param filename The filename in which the transition reward is defined.
+             * @param lineNumber The line number in which the transition reward is defined.
+             */
+            Constant(ConstantType constantType, std::string const& constantName, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            // Create default implementations of constructors/assignment.
+            Constant() = default;
+            Constant(Constant const& other) = default;
+            Constant& operator=(Constant const& other)= default;
+            Constant(Constant&& other) = default;
+            Constant& operator=(Constant&& other) = default;
+            
+            /*!
+             * Retrieves the name of the constant.
+             *
+             * @return The name of the constant.
+             */
+            std::string const& getConstantName() const;
+            
+            /*!
+             * Retrieves the type of the constant.
+             *
+             * @return The type of the constant;
+             */
+            ConstantType getConstantType() const;
+            
+            /*!
+             * Retrieves whether the constant is defined, i.e., whether there is an expression defining its value.
+             *
+             * @return True iff the constant is defined.
+             */
+            bool isDefined() const;
+            
+            /*!
+             * Retrieves the expression that defines the constant. This may only be called if the object is a defined
+             * constant.
+             *
+             * @return The expression that defines the constant.
+             */
+            storm::expressions::Expression const& getExpression() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, Constant const& constant);
+            
+        private:
+            // The type of the constant.
+            ConstantType constantType;
+            
+            // The name of the constant.
+            std::string constantName;
+            
+            // A flag that stores whether or not the constant is defined.
+            bool defined;
+            
+            // The expression that defines the constant (in case it is defined).
+            storm::expressions::Expression expression;
+        };
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_CONSTANT_H_ */

src/storage/prism/Formula.cpp

@@ -0,0 +1,26 @@
+#include "src/storage/prism/Formula.h"
+
+namespace storm {
+    namespace prism {
+        Formula::Formula(std::string const& formulaName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), formulaName(formulaName), expression(expression) {
+            // Intentionally left empty.
+        }
+        
+        std::string const& Formula::getFormulaName() const {
+            return this->formulaName;
+        }
+        
+        storm::expressions::Expression const& Formula::getExpression() const {
+            return this->expression;
+        }
+        
+        storm::expressions::ExpressionReturnType Formula::getReturnType() const {
+            return this->getExpression().getReturnType();
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, Formula const& formula) {
+            stream << "formula " << formula.getFormulaName() << " = " << formula.getExpression() << ";";
+            return stream;
+        }
+    }
+}

src/storage/prism/Formula.h

@@ -0,0 +1,62 @@
+#ifndef STORM_STORAGE_PRISM_FORMULA_H_
+#define STORM_STORAGE_PRISM_FORMULA_H_
+
+#include "src/storage/prism/LocatedInformation.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace prism {
+        class Formula : public LocatedInformation {
+        public:
+            /*!
+             * Creates a formula with the given name and expression.
+             *
+             * @param formulaName The name of the label.
+             * @param expression The predicate that needs to hold before taking a transition with the previously
+             * specified name in order to obtain the reward.
+             * @param filename The filename in which the transition reward is defined.
+             * @param lineNumber The line number in which the transition reward is defined.
+             */
+            Formula(std::string const& formulaName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            // Create default implementations of constructors/assignment.
+            Formula() = default;
+            Formula(Formula const& other) = default;
+            Formula& operator=(Formula const& other)= default;
+            Formula(Formula&& other) = default;
+            Formula& operator=(Formula&& other) = default;
+            
+            /*!
+             * Retrieves the name that is associated with this formula.
+             *
+             * @return The name that is associated with this formula.
+             */
+            std::string const& getFormulaName() const;
+            
+            /*!
+             * Retrieves the expression that is associated with this formula.
+             *
+             * @return The expression that is associated with this formula.
+             */
+            storm::expressions::Expression const& getExpression() const;
+            
+            /*!
+             * Retrieves the return type of the formula, i.e., the return-type of the defining expression.
+             *
+             * @return The return type of the formula.
+             */
+            storm::expressions::ExpressionReturnType getReturnType() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, Formula const& formula);
+            
+        private:
+            // The name of the formula.
+            std::string formulaName;
+            
+            // A predicate that needs to be satisfied by states for the label to be attached.
+            storm::expressions::Expression expression;
+        };
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_FORMULA_H_ */

src/storage/prism/Label.cpp

@@ -0,0 +1,22 @@
+#include "src/storage/prism/Label.h"
+
+namespace storm {
+    namespace prism {
+        Label::Label(std::string const& labelName, storm::expressions::Expression const& statePredicateExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), labelName(labelName), statePredicateExpression(statePredicateExpression) {
+            // Intentionally left empty.
+        }
+
+        std::string const& Label::getLabelName() const {
+            return this->labelName;
+        }
+        
+        storm::expressions::Expression const& Label::getStatePredicateExpression() const {
+            return this->statePredicateExpression;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, Label const& label) {
+            stream << "label \"" << label.getLabelName() << "\" = " << label.getStatePredicateExpression() << ";";
+            return stream;
+        }
+    }
+}

src/storage/prism/Label.h

@@ -0,0 +1,55 @@
+#ifndef STORM_STORAGE_PRISM_LABEL_H_
+#define STORM_STORAGE_PRISM_LABEL_H_
+
+#include "src/storage/prism/LocatedInformation.h"
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace prism {
+        class Label : public LocatedInformation {
+        public:
+            /*!
+             * Creates a label with the given name and state predicate expression.
+             *
+             * @param labelName The name of the label.
+             * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously
+             * specified name in order to obtain the reward.
+             * @param filename The filename in which the transition reward is defined.
+             * @param lineNumber The line number in which the transition reward is defined.
+             */
+            Label(std::string const& labelName, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            // Create default implementations of constructors/assignment.
+            Label() = default;
+            Label(Label const& other) = default;
+            Label& operator=(Label const& other)= default;
+            Label(Label&& other) = default;
+            Label& operator=(Label&& other) = default;
+            
+            /*!
+             * Retrieves the name that is associated with this label.
+             *
+             * @return The name that is associated with this label.
+             */
+            std::string const& getLabelName() const;
+            
+            /*!
+             * Retrieves the state predicate expression that is associated with this label.
+             *
+             * @return The state predicate expression that is associated with this label.
+             */
+            storm::expressions::Expression const& getStatePredicateExpression() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, Label const& label);
+            
+        private:
+            // The name of the label.
+            std::string labelName;
+            
+            // A predicate that needs to be satisfied by states for the label to be attached.
+            storm::expressions::Expression statePredicateExpression;
+        };
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_LABEL_H_ */

src/storage/prism/LocatedInformation.h

@@ -16,6 +16,7 @@ namespace storm {
             LocatedInformation(std::string const& filename, uint_fast64_t lineNumber);
             
             // Create default implementations of constructors/assignment.
+            LocatedInformation() = default;
             LocatedInformation(LocatedInformation const& other) = default;
             LocatedInformation& operator=(LocatedInformation const& other)= default;
             LocatedInformation(LocatedInformation&& other) = default;

src/storage/prism/Module.cpp

@@ -5,26 +5,29 @@
 
 namespace storm {
     namespace prism {
-        Module::Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap() {
+            // FIXME: construct mappings from variable names to their indices.
             // Initialize the internal mappings for fast information retrieval.
             this->collectActions();
         }
         
         Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() {
             // Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown.
-            for (auto const& nameVariablePair : oldModule.getBooleanVariables()) {
-                auto renamingPair = renaming.find(nameVariablePair.first);
-                LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable " << moduleName << "." << nameVariablePair.first << " was not renamed.");
-                this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber));
+            for (auto const& booleanVariable : oldModule.getBooleanVariables()) {
+                auto const& renamingPair = renaming.find(booleanVariable.getName());
+                LOG_THROW(renamingPair != renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable '" << booleanVariable.getName() << " was not renamed.");
+                this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, renaming, filename, lineNumber);
             }
             
             // Now do the same for the integer variables.
-            for (auto const& nameVariablePair : oldModule.getIntegerVariables()) {
-                auto renamingPair = renaming.find(nameVariablePair.first);
-                LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable " << moduleName << "." << nameVariablePair.first << " was not renamed.");
-                this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber));
+            for (auto const& integerVariable : oldModule.getIntegerVariables()) {
+                auto const& renamingPair = renaming.find(integerVariable.getName());
+                LOG_THROW(renamingPair != renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable '" << integerVariable.getName() << " was not renamed.");
+                this->integerVariables.emplace_back(integerVariable, renamingPair->second, renaming, filename, lineNumber);
             }
             
+            // FIXME: construct mappings from variable names to their indices.
+            
             // Now we are ready to clone all commands and rename them if requested.
             this->commands.reserve(oldModule.getNumberOfCommands());
             for (Command const& command : oldModule.getCommands()) {
@@ -44,22 +47,22 @@ namespace storm {
         }
         
         storm::prism::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const {
-            auto const& nameVariablePair = this->getBooleanVariables().find(variableName);
-            LOG_THROW(nameVariablePair == this->getBooleanVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'.");
-            return nameVariablePair->second;
+            auto const& nameIndexPair = this->booleanVariableToIndexMap.find(variableName);
+            LOG_THROW(nameIndexPair != this->booleanVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'.");
+            return this->getBooleanVariables()[nameIndexPair->second];
         }
         
-        std::map<std::string, storm::prism::BooleanVariable> const& Module::getBooleanVariables() const {
+        std::vector<storm::prism::BooleanVariable> const& Module::getBooleanVariables() const {
             return this->booleanVariables;
         }
 
         storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const {
-            auto const& nameVariablePair = this->getIntegerVariables().find(variableName);
-            LOG_THROW(nameVariablePair == this->getIntegerVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'.");
-            return nameVariablePair->second;
+            auto const& nameIndexPair = this->integerVariableToIndexMap.find(variableName);
+            LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'.");
+            return this->getIntegerVariables()[nameIndexPair->second];
         }
         
-        std::map<std::string, storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
+        std::vector<storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
             return this->integerVariables;
         }
         
@@ -67,6 +70,14 @@ namespace storm {
             return this->commands.size();
         }
         
+        std::size_t Module::getNumberOfUpdates() const {
+            std::size_t result = 0;
+            for (auto const& command : this->getCommands()) {
+                result += command.getNumberOfUpdates();
+            }
+            return result;
+        }
+        
         storm::prism::Command const& Module::getCommand(uint_fast64_t index) const {
             return this->commands[index];
         }
@@ -136,11 +147,11 @@ namespace storm {
         
         std::ostream& operator<<(std::ostream& stream, Module const& module) {
             stream << "module " << module.getName() << std::endl;
-            for (auto const& nameVariablePair : module.getBooleanVariables()) {
-                stream << "\t" << nameVariablePair.second << std::endl;
+            for (auto const& booleanVariable : module.getBooleanVariables()) {
+                stream << "\t" << booleanVariable << std::endl;
             }
-            for (auto const& nameVariablePair : module.getIntegerVariables()) {
-                stream << "\t" << nameVariablePair.second << std::endl;
+            for (auto const& integerVariable : module.getIntegerVariables()) {
+                stream << "\t" << integerVariable << std::endl;
             }
             for (auto const& command : module.getCommands()) {
                 stream << "\t" << command << std::endl;

src/storage/prism/Module.h

@@ -26,7 +26,7 @@ namespace storm {
              * @param filename The filename in which the module is defined.
              * @param lineNumber The line number in which the module is defined.
              */
-            Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             /*!
              * Special copy constructor, implementing the module renaming functionality. This will create a new module
@@ -74,7 +74,7 @@ namespace storm {
              *
              * @return The boolean variables of the module.
              */
-            std::map<std::string, storm::prism::BooleanVariable> const& getBooleanVariables() const;
+            std::vector<storm::prism::BooleanVariable> const& getBooleanVariables() const;
             
             /*!
              * Retrieves a reference to the integer variable with the given name.
@@ -89,15 +89,22 @@ namespace storm {
              *
              * @return The integer variables of the module.
              */
-            std::map<std::string, storm::prism::IntegerVariable> const& getIntegerVariables() const;
+            std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const;
 
             /*!
              * Retrieves the number of commands of this module.
              *
-             * @return the number of commands of this module.
+             * @return The number of commands of this module.
              */
             std::size_t getNumberOfCommands() const;
             
+            /*!
+             * Retrieves the total number of updates of this module.
+             *
+             * @return The total number of updates of this module.
+             */
+            std::size_t getNumberOfUpdates() const;
+            
             /*!
              * Retrieves a reference to the command with the given index.
              *
@@ -163,11 +170,17 @@ namespace storm {
             std::string moduleName;
             
             // A list of boolean variables.
-            std::map<std::string, storm::prism::BooleanVariable> booleanVariables;
+            std::vector<storm::prism::BooleanVariable> booleanVariables;
             
-            // A list of integer variables.
-            std::map<std::string, storm::prism::IntegerVariable> integerVariables;
+            // A mapping from boolean variables to the corresponding indices in the vector.
+            std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
             
+            // A list of integer variables.
+            std::vector<storm::prism::IntegerVariable> integerVariables;
+
+            // A mapping from integer variables to the corresponding indices in the vector.
+            std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
+
             // The commands associated with the module.
             std::vector<storm::prism::Command> commands;
             

src/storage/prism/Program.cpp

@@ -5,7 +5,8 @@
 
 namespace storm {
     namespace prism {
-        Program::Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> const& definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> const& definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> const& definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::map<std::string, storm::expressions::Expression>const& formulas, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), definedBooleanConstants(definedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), definedIntegerConstants(definedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), definedDoubleConstants(definedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), formulas(formulas), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
+        Program::Program(ModelType modelType, std::vector<Constant> const& undefinedConstants, std::vector<Constant> const& definedConstants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedConstants(undefinedConstants), definedConstants(definedConstants), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), labelToIndexMap(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
+            // FIXME: build the mappings for constants, formulas, modules, global variables, reward models and labels.
             // Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
             for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
                 Module const& module = this->getModule(moduleIndex);
@@ -21,10 +22,10 @@ namespace storm {
                 
                 // Put in the appropriate entries for the mapping from variable names to module index.
                 for (auto const& booleanVariable : module.getBooleanVariables()) {
-                    this->variableToModuleIndexMap[booleanVariable.first] = moduleIndex;
+                    this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
                 }
                 for (auto const& integerVariable : module.getBooleanVariables()) {
-                    this->variableToModuleIndexMap[integerVariable.first] = moduleIndex;
+                    this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
                 }
             }
         }
@@ -34,63 +35,35 @@ namespace storm {
         }
         
         bool Program::hasUndefinedConstants() const {
-            return this->hasUndefinedBooleanConstants() || this->hasUndefinedIntegerConstants() || this->hasUndefinedDoubleConstants();
+            return this->undefinedConstants.size() > 0;
         }
         
-        bool Program::hasUndefinedBooleanConstants() const {
-            return !this->undefinedBooleanConstants.empty();
+        std::vector<Constant> const& Program::getUndefinedConstants() const {
+            return this->undefinedConstants;
         }
         
-        bool Program::hasUndefinedIntegerConstants() const {
-            return !this->undefinedIntegerConstants.empty();
-        }
-        
-        bool Program::hasUndefinedDoubleConstants() const {
-            return !this->undefinedDoubleConstants.empty();
-        }
-        
-        std::set<std::string> const& Program::getUndefinedBooleanConstants() const {
-            return this->undefinedBooleanConstants;
-        }
-        
-        std::map<std::string, storm::expressions::Expression> const& Program::getDefinedBooleanConstants() const {
-            return this->definedBooleanConstants;
-        }
-
-        std::set<std::string> const& Program::getUndefinedIntegerConstants() const {
-            return this->undefinedIntegerConstants;
-        }
-        
-        std::map<std::string, storm::expressions::Expression> const& Program::getDefinedIntegerConstants() const {
-            return this->definedIntegerConstants;
-        }
-
-        std::set<std::string> const& Program::getUndefinedDoubleConstants() const {
-            return this->undefinedDoubleConstants;
-        }
-
-        std::map<std::string, storm::expressions::Expression> const& Program::getDefinedDoubleConstants() const {
-            return this->definedDoubleConstants;
+        std::vector<Constant> const& Program::getDefinedConstants() const {
+            return this->definedConstants;
         }
 
-        std::map<std::string, storm::prism::BooleanVariable> const& Program::getGlobalBooleanVariables() const {
+        std::vector<BooleanVariable> const& Program::getGlobalBooleanVariables() const {
             return this->globalBooleanVariables;
         }
-
-        storm::prism::BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const {
-            auto const& nameVariablePair = this->getGlobalBooleanVariables().find(variableName);
-            LOG_THROW(nameVariablePair != this->getGlobalBooleanVariables().end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'.");
-            return nameVariablePair->second;
-        }
         
-        std::map<std::string, storm::prism::IntegerVariable> const& Program::getGlobalIntegerVariables() const {
+        std::vector<IntegerVariable> const& Program::getGlobalIntegerVariables() const {
             return this->globalIntegerVariables;
         }
 
-        storm::prism::IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const {
-            auto const& nameVariablePair = this->getGlobalIntegerVariables().find(variableName);
-            LOG_THROW(nameVariablePair != this->getGlobalIntegerVariables().end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'.");
-            return nameVariablePair->second;
+        BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const {
+            auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName);
+            LOG_THROW(nameIndexPair != this->globalBooleanVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'.");
+            return this->getGlobalBooleanVariables()[nameIndexPair->second];
+        }
+
+        IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const {
+            auto const& nameIndexPair = this->globalIntegerVariableToIndexMap.find(variableName);
+            LOG_THROW(nameIndexPair != this->globalIntegerVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'.");
+            return this->getGlobalIntegerVariables()[nameIndexPair->second];
         }
         
         std::size_t Program::getNumberOfGlobalBooleanVariables() const {
@@ -101,7 +74,7 @@ namespace storm {
             return this->getGlobalIntegerVariables().size();
         }
         
-        std::map<std::string, storm::expressions::Expression> const& Program::getFormulas() const {
+        std::vector<Formula> const& Program::getFormulas() const {
             return this->formulas;
         }
         
@@ -113,6 +86,12 @@ namespace storm {
             return this->modules[index];
         }
         
+        Module const& Program::getModule(std::string const& moduleName) const {
+            auto const& nameIndexPair = this->moduleToIndexMap.find(moduleName);
+            LOG_THROW(nameIndexPair != this->moduleToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown module '" << moduleName << "'.");
+            return this->getModules()[nameIndexPair->second];
+        }
+        
         std::vector<storm::prism::Module> const& Program::getModules() const {
             return this->modules;
         }
@@ -131,10 +110,10 @@ namespace storm {
                 
                 for (auto const& module : this->getModules()) {
                     for (auto const& booleanVariable : module.getBooleanVariables()) {
-                        result = result && (storm::expressions::Expression::createBooleanVariable(booleanVariable.second.getName()).iff(booleanVariable.second.getInitialValueExpression()));
+                        result = result && (storm::expressions::Expression::createBooleanVariable(booleanVariable.getName()).iff(booleanVariable.getInitialValueExpression()));
                     }
                     for (auto const& integerVariable : module.getIntegerVariables()) {
-                        result = result && (storm::expressions::Expression::createIntegerVariable(integerVariable.second.getName()) == integerVariable.second.getInitialValueExpression());
+                        result = result && (storm::expressions::Expression::createIntegerVariable(integerVariable.getName()) == integerVariable.getInitialValueExpression());
                     }
                 }
                 return result;
@@ -157,17 +136,17 @@ namespace storm {
             return variableNameToModuleIndexPair->second;
         }
         
-        std::map<std::string, storm::prism::RewardModel> const& Program::getRewardModels() const {
+        std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
             return this->rewardModels;
         }
         
         storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
-            auto const& nameRewardModelPair = this->getRewardModels().find(name);
-            LOG_THROW(nameRewardModelPair != this->getRewardModels().end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist.");
-            return nameRewardModelPair->second;
+            auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
+            LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist.");
+            return this->getRewardModels()[nameIndexPair->second];
         }
         
-        std::map<std::string, storm::expressions::Expression> const& Program::getLabels() const {
+        std::vector<Label> const& Program::getLabels() const {
             return this->labels;
         }
         
@@ -179,7 +158,7 @@ namespace storm {
                 newModules.push_back(module.restrictCommands(indexSet));
             }
             
-            return Program(this->getModelType(), this->getUndefinedBooleanConstants(), this->getDefinedBooleanConstants(), this->getUndefinedIntegerConstants(), this->getDefinedIntegerConstants(), this->getUndefinedDoubleConstants(), this->getDefinedDoubleConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
+            return Program(this->getModelType(), this->getUndefinedConstants(), this->getDefinedConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
         }
         
         std::ostream& operator<<(std::ostream& stream, Program const& program) {
@@ -193,22 +172,16 @@ namespace storm {
             }
             stream << std::endl;
             
-            for (auto const& element : program.getUndefinedBooleanConstants()) {
-                stream << "const bool " << element << ";" << std::endl;
-            }
-            for (auto const& element : program.getUndefinedIntegerConstants()) {
-                stream << "const int " << element << ";" << std::endl;
-            }
-            for (auto const& element : program.getUndefinedDoubleConstants()) {
-                stream << "const double " << element << ";" << std::endl;
+            for (auto const& constant : program.getUndefinedConstants()) {
+                stream << constant << std::endl;
             }
             stream << std::endl;
             
-            for (auto const& element : program.getGlobalBooleanVariables()) {
-                stream << "global " << element.second << std::endl;
+            for (auto const& variable : program.getGlobalBooleanVariables()) {
+                stream << "global " << variable << std::endl;
             }
-            for (auto const& element : program.getGlobalIntegerVariables()) {
-                stream << "global " << element.second << std::endl;
+            for (auto const& variable : program.getGlobalIntegerVariables()) {
+                stream << "global " << variable << std::endl;
             }
             stream << std::endl;
             
@@ -217,11 +190,11 @@ namespace storm {
             }
             
             for (auto const& rewardModel : program.getRewardModels()) {
-                stream << rewardModel.second << std::endl;
+                stream << rewardModel << std::endl;
             }
             
             for (auto const& label : program.getLabels()) {
-                stream << "label \"" << label.first << "\" = " << label.second <<";" << std::endl;
+                stream << label << std::endl;
             }
             
             return stream;

src/storage/prism/Program.h

@@ -7,6 +7,9 @@
 #include <boost/container/flat_set.hpp>
 
 #include "src/storage/expressions/Expression.h"
+#include "src/storage/prism/Constant.h"
+#include "src/storage/prism/Formula.h"
+#include "src/storage/prism/Label.h"
 #include "src/storage/prism/Module.h"
 #include "src/storage/prism/RewardModel.h"
 
@@ -24,12 +27,8 @@ namespace storm {
              * models, labels and initial states.
              *
              * @param modelType The type of the program.
-             * @param undefinedBooleanConstants The undefined boolean constants of the program.
-             * @param definedBooleanConstants The defined boolean constants of the program.
-             * @param undefinedIntegerConstants The undefined integer constants of the program.
-             * @param definedIntegerConstants The defined integer constants of the program.
-             * @param undefinedDoubleConstants The undefined double constants of the program.
-             * @param definedDoubleConstants The defined double constants of the program.
+             * @param undefinedConstants The undefined constants of the program.
+             * @param definedConstants The defined integer constants of the program.
              * @param globalBooleanVariables The global boolean variables of the program.
              * @param globalIntegerVariables The global integer variables of the program.
              * @param formulas The formulas defined in the program.
@@ -44,7 +43,7 @@ namespace storm {
              * @param filename The filename in which the program is defined.
              * @param lineNumber The line number in which the program is defined.
              */
-            Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> const& definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> const& definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> const& definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::map<std::string, storm::expressions::Expression> const& formulas, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Program(ModelType modelType, std::vector<Constant> const& undefinedConstants, std::vector<Constant> const& definedConstants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -68,74 +67,25 @@ namespace storm {
             bool hasUndefinedConstants() const;
             
             /*!
-             * Retrieves whether there are boolean undefined constants in the program.
+             * Retrieves the undefined constants of the program.
              *
-             * @return True iff there are boolean undefined constants in the program.
+             * @return The undefined constants of the program.
              */
-            bool hasUndefinedBooleanConstants() const;
+            std::vector<Constant> const& getUndefinedConstants() const;
 
             /*!
-             * Retrieves whether there are integer undefined constants in the program.
+             * Retrieves the defined constants of the program.
              *
-             * @return True iff there are integer undefined constants in the program.
+             * @return The defined constants of the program.
              */
-            bool hasUndefinedIntegerConstants() const;
-            
-            /*!
-             * Retrieves whether there are double undefined constants in the program.
-             *
-             * @return True iff there are double undefined constants in the program.
-             */
-            bool hasUndefinedDoubleConstants() const;
-            
-            /*!
-             * Retrieves the undefined boolean constants of the program.
-             *
-             * @return The undefined boolean constants of the program.
-             */
-            std::set<std::string> const& getUndefinedBooleanConstants() const;
-            
-            /*!
-             * Retrieves the defined boolean constants of the program.
-             *
-             * @return The defined boolean constants of the program.
-             */
-            std::map<std::string, storm::expressions::Expression> const& getDefinedBooleanConstants() const;
-            
-            /*!
-             * Retrieves the undefined integer constants of the program.
-             *
-             * @return The undefined integer constants of the program.
-             */
-            std::set<std::string> const& getUndefinedIntegerConstants() const;
-
-            /*!
-             * Retrieves the defined integer constants of the program.
-             *
-             * @return The defined integer constants of the program.
-             */
-            std::map<std::string, storm::expressions::Expression> const& getDefinedIntegerConstants() const;
-
-            /*!
-             * Retrieves the undefined double constants of the program.
-             *
-             * @return The undefined double constants of the program.
-             */
-            std::set<std::string> const& getUndefinedDoubleConstants() const;
-            
-            /*!
-             * Retrieves the defined double constants of the program.
-             *
-             * @return The defined double constants of the program.
-             */
-            std::map<std::string, storm::expressions::Expression> const& getDefinedDoubleConstants() const;
+            std::vector<Constant> const& getDefinedConstants() const;
 
             /*!
              * Retrieves the global boolean variables of the program.
              *
              * @return The global boolean variables of the program.
              */
-            std::map<std::string, storm::prism::BooleanVariable> const& getGlobalBooleanVariables() const;
+            std::vector<BooleanVariable> const& getGlobalBooleanVariables() const;
             
             /*!
              * Retrieves a the global boolean variable with the given name.
@@ -143,14 +93,14 @@ namespace storm {
              * @param variableName The name of the global boolean variable to retrieve.
              * @return The global boolean variable with the given name.
              */
-            storm::prism::BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
+            BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
             
             /*!
              * Retrieves the global integer variables of the program.
              *
              * @return The global integer variables of the program.
              */
-            std::map<std::string, storm::prism::IntegerVariable> const& getGlobalIntegerVariables() const;
+            std::vector<IntegerVariable> const& getGlobalIntegerVariables() const;
 
             /*!
              * Retrieves a the global integer variable with the given name.
@@ -158,7 +108,7 @@ namespace storm {
              * @param variableName The name of the global integer variable to retrieve.
              * @return The global integer variable with the given name.
              */
-            storm::prism::IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const;
+            IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const;
 
             /*!
              * Retrieves the number of global boolean variables of the program.
@@ -179,7 +129,7 @@ namespace storm {
              *
              * @return The formulas defined in the program.
              */
-            std::map<std::string, storm::expressions::Expression> const& getFormulas() const;
+            std::vector<Formula> const& getFormulas() const;
             
             /*!
              * Retrieves the number of modules in the program.
@@ -194,14 +144,22 @@ namespace storm {
              * @param index The index of the module to retrieve.
              * @return The module with the given index.
              */
-            storm::prism::Module const& getModule(uint_fast64_t index) const;
+            Module const& getModule(uint_fast64_t index) const;
+
+            /*!
+             * Retrieves the module with the given name.
+             *
+             * @param moduleName The name of the module to retrieve.
+             * @return The module with the given name.
+             */
+            Module const& getModule(std::string const& moduleName) const;
             
             /*!
              * Retrieves all modules of the program.
              *
              * @return All modules of the program.
              */
-            std::vector<storm::prism::Module> const& getModules() const;
+            std::vector<Module> const& getModules() const;
             
             /*!
              * Retrieves whether the program explicitly specifies an expression characterizing the initial states.
@@ -246,7 +204,7 @@ namespace storm {
              *
              * @return The reward models of the program.
              */
-            std::map<std::string, storm::prism::RewardModel> const& getRewardModels() const;
+            std::vector<RewardModel> const& getRewardModels() const;
             
             /*!
              * Retrieves the reward model with the given name.
@@ -254,14 +212,14 @@ namespace storm {
              * @param rewardModelName The name of the reward model to return.
              * @return The reward model with the given name.
              */
-            storm::prism::RewardModel const& getRewardModel(std::string const& rewardModelName) const;
+            RewardModel const& getRewardModel(std::string const& rewardModelName) const;
             
             /*!
              * Retrieves all labels that are defined by the probabilitic program.
              *
              * @return A set of labels that are defined in the program.
              */
-            std::map<std::string, storm::expressions::Expression> const& getLabels() const;
+            std::vector<Label> const& getLabels() const;
             
             /*!
              * Creates a new program that drops all commands whose indices are not in the given set.
@@ -276,38 +234,41 @@ namespace storm {
             // The type of the model.
             ModelType modelType;
             
-            // The undefined boolean constants of the program.
-            std::set<std::string> undefinedBooleanConstants;
+            // The undefined constants of the program.
+            std::vector<Constant> undefinedConstants;
             
-            // A mapping of (defined) boolean constants to their values (given as expressions).
-            std::map<std::string, storm::expressions::Expression> definedBooleanConstants;
-
-            // The undefined integer constants of the program.
-            std::set<std::string> undefinedIntegerConstants;
-
-            // A mapping of (defined) integer constants to their values (given as expressions).
-            std::map<std::string, storm::expressions::Expression> definedIntegerConstants;
-
-            // The undefined double constants of the program.
-            std::set<std::string> undefinedDoubleConstants;
-            
-            // A mapping of (defined) double constants to their values (given as expressions).
-            std::map<std::string, storm::expressions::Expression> definedDoubleConstants;
+            // The defined constants of the program.
+            std::vector<Constant> definedConstants;
 
             // The global boolean variables.
-            std::map<std::string, BooleanVariable> globalBooleanVariables;
+            std::vector<BooleanVariable> globalBooleanVariables;
+            
+            // A mapping from global boolean variable names to their corresponding indices.
+            std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap;
             
             // The global integer variables.
-            std::map<std::string, IntegerVariable> globalIntegerVariables;
+            std::vector<IntegerVariable> globalIntegerVariables;
             
-            // A mapping of formula names to the corresponding expressions.
-            std::map<std::string, storm::expressions::Expression> formulas;
+            // A mapping from global integer variable names to their corresponding indices.
+            std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap;
+            
+            // The formulas defined in the program.
+            std::vector<Formula> formulas;
+            
+            // A mapping of formula names to their corresponding indices.
+            std::map<std::string, uint_fast64_t> formulaToIndexMap;
             
             // The modules associated with the program.
-            std::vector<storm::prism::Module> modules;
+            std::vector<Module> modules;
+            
+            // A mapping of module names to their indices.
+            std::map<std::string, uint_fast64_t> moduleToIndexMap;
             
             // The reward models associated with the program.
-            std::map<std::string, storm::prism::RewardModel> rewardModels;
+            std::vector<RewardModel> rewardModels;
+            
+            // A mapping of reward models to their indices.
+            std::map<std::string, uint_fast64_t> rewardModelToIndexMap;
             
             // A flag that indicates whether the initial states of the program were given explicitly (in the form of an
             // initial construct) or implicitly (attached to the variable declarations).
@@ -317,7 +278,10 @@ namespace storm {
             storm::expressions::Expression initialStatesExpression;
             
             // The labels that are defined for this model.
-            std::map<std::string, storm::expressions::Expression> labels;
+            std::vector<Label> labels;
+            
+            // A mapping from label names to their corresponding indices.
+            std::map<std::string, uint_fast64_t> labelToIndexMap;
             
             // The set of actions present in this program.
             std::set<std::string> actions;

src/storage/prism/Update.cpp

@@ -1,21 +1,23 @@
 #include "Update.h"
+#include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/OutOfRangeException.h"
 
 namespace storm {
     namespace prism {
-        Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), globalIndex(globalIndex) {
-            // Nothing to do here.
+        Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) {
+            // FIXME: construct the mapping from variable names to assignments and check for uniqueness.
         }
         
-        Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), assignments(), globalIndex(newGlobalIndex) {
-            for (auto const& variableAssignmentPair : update.getAssignments()) {
-                auto const& namePair = renaming.find(variableAssignmentPair.first);
+        Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), assignments(), variableToAssignmentIndexMap(), globalIndex(newGlobalIndex) {
+            for (auto const& assignment : update.getAssignments()) {
+                auto const& namePair = renaming.find(assignment.getVariableName());
                 if (namePair != renaming.end()) {
-                    this->assignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
+                    this->assignments.emplace_back(Assignment(assignment, renaming, filename, lineNumber));
                 } else {
-                    this->assignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
+                    this->assignments.emplace_back(Assignment(assignment));
                 }
             }
+            // FIXME: construct the mapping from variable names to assignments and check for uniqueness.
             this->likelihoodExpression = update.getLikelihoodExpression().substitute<std::map>(renaming);
         }
         
@@ -27,17 +29,14 @@ namespace storm {
             return this->assignments.size();
         }
         
-        std::map<std::string, storm::prism::Assignment> const& Update::getAssignments() const {
+        std::vector<storm::prism::Assignment> const& Update::getAssignments() const {
             return this->assignments;
         }
         
         storm::prism::Assignment const& Update::getAssignment(std::string const& variableName) const {
-            auto variableAssignmentPair = this->getAssignments().find(variableName);
-            if (variableAssignmentPair == this->getAssignments().end()) {
-                throw storm::exceptions::OutOfRangeException() << "Cannot find assignment for variable '" << variableName << "' in update " << *this << ".";
-            }
-            
-            return variableAssignmentPair->second;
+            auto const& variableIndexPair = this->variableToAssignmentIndexMap.find(variableName);
+            LOG_THROW(variableIndexPair != this->variableToAssignmentIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' is not assigned in update.");
+            return this->getAssignments()[variableIndexPair->second];
         }
         
         uint_fast64_t Update::getGlobalIndex() const {
@@ -48,7 +47,7 @@ namespace storm {
             stream << update.getLikelihoodExpression() << " : ";
             uint_fast64_t i = 0;
             for (auto const& assignment : update.getAssignments()) {
-                stream << assignment.second;
+                stream << assignment;
                 if (i < update.getAssignments().size() - 1) {
                     stream << " & ";
                 }

src/storage/prism/Update.h

@@ -1,7 +1,7 @@
 #ifndef STORM_STORAGE_PRISM_UPDATE_H_
 #define STORM_STORAGE_PRISM_UPDATE_H_
 
-#include <map>
+#include <vector>
 
 #include "src/storage/prism/LocatedInformation.h"
 #include "src/storage/prism/Assignment.h"
@@ -11,16 +11,15 @@ namespace storm {
         class Update : public LocatedInformation {
         public:
             /*!
-             * Creates an update with the given expression specifying the likelihood and the mapping of variable to
-             * their assignments.
+             * Creates an update with the given expression specifying the likelihood and assignments.
              *
              * @param globalIndex The global index of the update.
              * @param likelihoodExpression An expression specifying the likelihood of this update.
-             * @param assignments A map of variable names to their assignments.
-             * @param filename The filename in which the variable is defined.
-             * @param lineNumber The line number in which the variable is defined.
+             * @param assignments A assignments to variables.
+             * @param filename The filename in which the update is defined.
+             * @param lineNumber The line number in which the update is defined.
              */
-            Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& assignments, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             /*!
              * Creates a copy of the given update and performs the provided renaming.
@@ -28,8 +27,8 @@ namespace storm {
              * @param update The update that is to be copied.
              * @param newGlobalIndex The global index of the resulting update.
              * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
-             * @param filename The filename in which the variable is defined.
-             * @param lineNumber The line number in which the variable is defined.
+             * @param filename The filename in which the update is defined.
+             * @param lineNumber The line number in which the update is defined.
              */
             Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
@@ -59,7 +58,7 @@ namespace storm {
              *
              * @return A reference to the map of variable names to their respective assignments.
              */
-            std::map<std::string, storm::prism::Assignment> const& getAssignments() const;
+            std::vector<storm::prism::Assignment> const& getAssignments() const;
             
             /*!
              * Retrieves a reference to the assignment for the variable with the given name.
@@ -81,8 +80,11 @@ namespace storm {
             // An expression specifying the likelihood of taking this update.
             storm::expressions::Expression likelihoodExpression;
             
-            // A mapping of variable names to their assignments in this update.
-            std::map<std::string, storm::prism::Assignment> assignments;
+            // The assignments of this update.
+            std::vector<storm::prism::Assignment> assignments;
+            
+            // A mapping from variable names to their assignments.
+            std::map<std::string, uint_fast64_t> variableToAssignmentIndexMap;
             
             // The global index of the update.
             uint_fast64_t globalIndex;

src/storm.cpp

@@ -54,6 +54,7 @@
 #include "log4cplus/loggingmacros.h"
 #include "log4cplus/consoleappender.h"
 #include "log4cplus/fileappender.h"
+log4cplus::Logger logger;
 
 #include "src/parser/PrismParser.h"
 #include "src/adapters/ExplicitModelAdapter.h"
@@ -121,8 +122,6 @@ void printUsage() {
 #endif
 }
 
-log4cplus::Logger logger;
-
 /*!
  * Initializes the logging framework and sets up logging to console.
  */