diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index ed15050cb..727579dff 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -1,20 +1,21 @@
 #include "src/parser/PrismParser.h"
 #include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidTypeException.h"
 #include "src/exceptions/WrongFormatException.h"
 
 namespace storm {
     namespace parser {
-        storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) {
+        storm::prism::Program PrismParser::parse(std::string const& filename) {
             // Open file and initialize result.
             std::ifstream inputFileStream(filename, std::ios::in);
-            LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file " << filename << ".");
+            LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
             
             storm::prism::Program result;
             
             // Now try to parse the contents of the file.
             try {
                 std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
-                result = parseFromString(fileContent, filename, typeCheck);
+                result = parseFromString(fileContent, filename);
             } catch(std::exception& e) {
                 // In case of an exception properly close the file before passing exception.
                 inputFileStream.close();
@@ -26,7 +27,7 @@ namespace storm {
             return result;
         }
         
-        storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool typeCheck) {
+        storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename) {
             PositionIteratorType first(input.begin());
             PositionIteratorType iter = first;
             PositionIteratorType last(input.end());
@@ -37,17 +38,17 @@ namespace storm {
             // Create grammar.
             storm::parser::PrismParser grammar(filename, first);
             try {
-                // Now parse the content using phrase_parse in order to be able to supply a skipping parser.
+                // Start first run.
                 bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
                 LOG_THROW(succeeded,  storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
-                if (typeCheck) {
-                    first = PositionIteratorType(input.begin());
-                    iter = first;
-                    last = PositionIteratorType(input.end());
-                    grammar.moveToSecondRun();
-                    succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
-                    LOG_THROW(succeeded,  storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
-                }
+                
+                // Start second run.
+                first = PositionIteratorType(input.begin());
+                iter = first;
+                last = PositionIteratorType(input.end());
+                grammar.moveToSecondRun();
+                succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
+                LOG_THROW(succeeded,  storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
             } catch (qi::expectation_failure<PositionIteratorType> const& e) {
                 // If the parser expected content different than the one provided, display information about the location of the error.
                 std::size_t lineNumber = boost::spirit::get_line(e.first);
@@ -147,13 +148,7 @@ namespace storm {
             
             globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
             globalVariableDefinition.name("global variable declaration list");
-            
-            programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1]
-            >   *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)])
-            >   *(formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1)])
-            >   *(globalVariableDefinition(qi::_r1));
-            programHeader.name("program header");
-            
+                        
             stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
             stateRewardDefinition.name("state reward definition");
             
@@ -167,7 +162,7 @@ namespace storm {
                                      >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
             rewardModelDefinition.name("reward model definition");
             
-            initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesExpression, phoenix::ref(*this), qi::_1, qi::_r1)];
+            initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             initialStatesConstruct.name("initial construct");
             
             labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
@@ -199,7 +194,19 @@ namespace storm {
             moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)];
             moduleDefinitionList.name("module list");
             
-            start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(initialStatesConstruct(qi::_a) | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
+            start = (qi::eps
+                     > modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1]
+                     > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] 
+                         | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
+                         | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
+                         | globalVariableDefinition(qi::_a)
+                         | (moduleRenaming(qi::_a) | moduleDefinition(qi::_a))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_a), qi::_1)]
+                         | initialStatesConstruct(qi::_a)
+                         | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] 
+                         | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] 
+                         | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
+                     )
+                     > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
             start.name("probabilistic program");
             
             // Enable error reporting.
@@ -257,13 +264,13 @@ namespace storm {
             return true;
         }
         
-        bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
-            LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::InvalidArgumentException, "Program must not define two initial constructs.");
-            if (globalProgramInformation.hasInitialStatesExpression) {
+        bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
+            LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs.");
+            if (globalProgramInformation.hasInitialConstruct) {
                 return false;
             }
-            globalProgramInformation.hasInitialStatesExpression = true;
-            globalProgramInformation.initialStatesExpression = initialStatesExpression;
+            globalProgramInformation.hasInitialConstruct = true;
+            globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3));
             return true;
         }
         
@@ -271,7 +278,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1.ite(e2, e3);
+                try {
+                    return e1.ite(e2, e3);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -279,7 +290,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1.implies(e2);
+                try {
+                    return e1.implies(e2);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -287,7 +302,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 || e2;
+                try {
+                    return e1 || e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -295,7 +314,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 && e2;
+                try{
+                    return e1 && e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -303,7 +326,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 > e2;
+                try {
+                    return e1 > e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -311,7 +338,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 >= e2;
+                try {
+                    return e1 >= e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -319,7 +350,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 < e2;
+                try {
+                    return e1 < e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -327,7 +362,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 <= e2;
+                try {
+                    return e1 <= e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -335,10 +374,14 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
-                    return e1.iff(e2);
-                } else {
-                    return e1 == e2;
+                try {
+                    if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
+                        return e1.iff(e2);
+                    } else {
+                        return e1 == e2;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
                 }
             }
         }
@@ -347,10 +390,14 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
-                    return e1 ^ e2;
-                } else {
-                    return e1 != e2;
+                try {
+                    if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
+                        return e1 ^ e2;
+                    } else {
+                        return e1 != e2;
+                    }
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
                 }
             }
         }
@@ -359,7 +406,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 + e2;
+                try {
+                    return e1 + e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -367,7 +418,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 - e2;
+                try {
+                    return e1 - e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -375,7 +430,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 * e2;
+                try {
+                    return e1 * e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -383,7 +442,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1 / e2;
+                try {
+                    return e1 / e2;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -391,7 +454,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return !e1;
+                try {
+                    return !e1;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -399,7 +466,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return -e1;
+                try {
+                    return -e1;
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -444,7 +515,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return storm::expressions::Expression::minimum(e1, e2);
+                try {
+                    return storm::expressions::Expression::minimum(e1, e2);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -452,7 +527,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return storm::expressions::Expression::maximum(e1, e2);
+                try {
+                    return storm::expressions::Expression::maximum(e1, e2);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -460,7 +539,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1.floor();
+                try {
+                    return e1.floor();
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -468,7 +551,11 @@ namespace storm {
             if (!this->secondRun) {
                 return storm::expressions::Expression::createFalse();
             } else {
-                return e1.ceil();
+                try {
+                    return e1.ceil();
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+                }
             }
         }
         
@@ -477,43 +564,62 @@ namespace storm {
                 return storm::expressions::Expression::createFalse();
             } else {
                 storm::expressions::Expression const* expression = this->identifiers_.find(identifier);
-                LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Undeclared identifier '" << identifier << "'.");
+                LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
                 return *expression;
             }
         }
         
         storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
-            this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
+            }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
-            this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
+            }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
-            this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
+            }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
-            this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
+            }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
-            this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
+            }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
-            this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
+            }
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
         }
         
         storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
-            if (this->secondRun) {
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
                 this->identifiers_.add(formulaName, expression);
             }
             return storm::prism::Formula(formulaName, expression, this->getFilename());
@@ -550,12 +656,18 @@ namespace storm {
         }
         
         storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
-            this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+                this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
+            }
             return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
         }
         
         storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
-            this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
+            if (!this->secondRun) {
+                LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+                this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
+            }
             return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
         }
         
@@ -567,19 +679,19 @@ namespace storm {
         storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
             // Check whether the module to rename actually exists.
             auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
-            LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "No module named '" << oldModuleName << "' to rename.");
+            LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": No module named '" << oldModuleName << "' to rename.");
             storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
             
             if (!this->secondRun) {
                 // Register all (renamed) variables for later use.
                 for (auto const& variable : moduleToRename.getBooleanVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
-                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed.");
+                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
                     this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second));
                 }
                 for (auto const& variable : moduleToRename.getIntegerVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
-                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed.");
+                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
                     this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second));
                 }
                 
@@ -603,7 +715,7 @@ namespace storm {
                 std::vector<storm::prism::BooleanVariable> booleanVariables;
                 for (auto const& variable : moduleToRename.getBooleanVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
-                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed.");
+                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
                     
                     booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
                 }
@@ -612,7 +724,7 @@ namespace storm {
                 std::vector<storm::prism::IntegerVariable> integerVariables;
                 for (auto const& variable : moduleToRename.getIntegerVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
-                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed.");
+                    LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
                     
                     integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
                 }
@@ -645,12 +757,12 @@ namespace storm {
                     ++globalProgramInformation.currentCommandIndex;
                 }
                 
-                return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, this->getFilename());
+                return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming);
             }
         }
         
         storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
-            return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, globalProgramInformation.hasInitialStatesExpression, globalProgramInformation.initialStatesExpression, globalProgramInformation.labels, this->getFilename());
+            return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
         }
     } // namespace parser
 } // namespace storm
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index 4a0eec392..e1a9136ba 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -27,13 +27,17 @@ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost:
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/Expressions.h"
 #include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/WrongFormatException.h"
 
 namespace storm {
     namespace parser {
+        // A class that stores information about the parsed program.
         class GlobalProgramInformation {
         public:
             // Default construct the header information.
-			GlobalProgramInformation() : hasInitialStatesExpression(false), currentCommandIndex(0), currentUpdateIndex(0) {}
+			GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(),hasInitialConstruct(false), initialConstruct(storm::expressions::Expression::createFalse()), currentCommandIndex(0), currentUpdateIndex(0) {
+                // Intentionally left empty.
+            }
             
             // Members for all essential information that needs to be collected.
             storm::prism::Program::ModelType modelType;
@@ -45,8 +49,8 @@ namespace storm {
             std::vector<storm::prism::Module> modules;
             std::vector<storm::prism::RewardModel> rewardModels;
             std::vector<storm::prism::Label> labels;
-            storm::expressions::Expression initialStatesExpression;
-            bool hasInitialStatesExpression;
+            bool hasInitialConstruct;
+            storm::prism::InitialConstruct initialConstruct;
             
             // Counters to provide unique indexing for commands and updates.
             uint_fast64_t currentCommandIndex;
@@ -59,20 +63,18 @@ namespace storm {
              * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
              *
              * @param filename the name of the file to parse.
-             * @param typeCheck Sets whether the expressions are generated and therefore typechecked.
              * @return The resulting PRISM program.
              */
-            static storm::prism::Program parse(std::string const& filename, bool typeCheck = true);
+            static storm::prism::Program parse(std::string const& filename);
             
             /*!
              * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax.
              *
              * @param input The input string to parse.
              * @param filename The name of the file from which the input was read.
-             * @param typeCheck Sets whether the expressions are generated and therefore typechecked.
              * @return The resulting PRISM program.
              */
-            static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool typeCheck = true);
+            static storm::prism::Program parseFromString(std::string const& input, std::string const& filename);
             
         private:
             struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
@@ -117,13 +119,7 @@ namespace storm {
                 
                 template<typename T1, typename T2, typename T3, typename T4>
                 qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
-                    //                    LOG4CPLUS_ERROR(logger, "Error: expecting " << what << " in line " << get_line(where) << " at column " << get_column(b, where, 4) << ".");
-                    std::cerr << "Error: expecting " << what << " in line " << get_line(where) << "." << std::endl;
-                    T3 end(where);
-                    while (end != e && *end != '\r' && *end != '\n') {
-                        ++end;
-                    }
-                    std::cerr << "Error: expecting " << what << " in line " << get_line(where) << ": \n" << std::string(get_line_start(b, where), end) << " ... \n" << std::setw(std::distance(b, where)) << '^' << "---- here\n";
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << ".");
                     return qi::fail;
                 }
             };
@@ -193,7 +189,6 @@ namespace storm {
             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, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
             qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
             qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedIntegerConstantDefinition;
@@ -268,7 +263,7 @@ namespace storm {
             
             // Helper methods used in the grammar.
             bool isValidIdentifier(std::string const& identifier);
-            bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
+            bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
             
             storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
             storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index bbce93902..72abb87bf 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -184,6 +184,23 @@ namespace storm {
             this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd());
         }
         
+        void Dd<DdType::CUDD>::universalAbstract(std::set<std::string> const& metaVariableNames) {
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            
+            for (auto const& metaVariableName : metaVariableNames) {
+                // First check whether the DD contains the meta variable and erase it, if this is the case.
+                if (!this->containsMetaVariable(metaVariableName)) {
+                    throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
+                }
+                this->getContainedMetaVariableNames().erase(metaVariableName);
+                
+                DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                cubeDd *= metaVariable.getCube();
+            }
+            
+            this->cuddAdd = this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd());
+        }
+        
         void Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
             Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 6c7bffd6a..f345c28a2 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -233,6 +233,13 @@ namespace storm {
              */
             void existsAbstract(std::set<std::string> const& metaVariableNames);
             
+            /*!
+             * Universally abstracts from the given meta variables.
+             *
+             * @param metaVariableNames The names of all meta variables from which to abstract.
+             */
+            void universalAbstract(std::set<std::string> const& metaVariableNames);
+            
             /*!
              * Sum-abstracts from the given meta variables.
              *
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index 6c8c66683..64261d0aa 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -4,12 +4,36 @@
 
 #include "src/storage/dd/CuddDdManager.h"
 #include "src/exceptions/InvalidArgumentException.h"
+#include "src/settings/Settings.h"
+
+bool CuddOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool {
+    // Set up options for precision and maximal memory available to Cudd.
+    instance->addOption(storm::settings::OptionBuilder("Cudd", "cuddprec", "", "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+
+    instance->addOption(storm::settings::OptionBuilder("Cudd", "cuddmaxmem", "", "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mb", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
+    
+    // Set up option for reordering.
+    std::vector<std::string> reorderingTechniques;
+    reorderingTechniques.push_back("none");
+    reorderingTechniques.push_back("sift");
+    reorderingTechniques.push_back("ssift");
+    reorderingTechniques.push_back("gsift");
+    reorderingTechniques.push_back("win2");
+    reorderingTechniques.push_back("win3");
+    reorderingTechniques.push_back("win4");
+    reorderingTechniques.push_back("annealing");
+    reorderingTechniques.push_back("genetic");
+    reorderingTechniques.push_back("exact");
+	instance->addOption(storm::settings::OptionBuilder("Cudd", "reorder", "", "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines. Must be in {\"none\", \"sift\", \"ssift\", \"gsift\", \"win2\", \"win3\", \"win4\", \"annealing\", \"genetic\", \"exact\"}.").setDefaultValueString("gsift").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(reorderingTechniques)).build()).build());
+    
+    return true;
+});
 
 namespace storm {
     namespace dd {
         DdManager<DdType::CUDD>::DdManager() : metaVariableMap(), cuddManager() {
-            
-            this->cuddManager.SetEpsilon(1.0e-15);
+            this->cuddManager.SetMaxMemory(storm::settings::Settings::getInstance()->getOptionByLongName("cuddmaxmem").getArgument(0).getValueAsUnsignedInteger() * 1024);
+            this->cuddManager.SetEpsilon(storm::settings::Settings::getInstance()->getOptionByLongName("cuddprec").getArgument(0).getValueAsDouble());
         }
         
         Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne() {
@@ -124,7 +148,7 @@ namespace storm {
             metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
         }
         
-        void DdManager<DdType::CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
+        void DdManager<DdType::CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup) {
             // Make sure that at least one meta variable is added.
             if (names.size() == 0) {
                 throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables.";
@@ -158,6 +182,13 @@ namespace storm {
                 }
             }
             
+            // If required, we group the bits on the same layer of the interleaved meta variables.
+            if (fixedGroup) {
+                for (uint_fast64_t i = 0; i < names.size(); ++i) {
+                    this->getCuddManager().MakeTreeNode(variables[i].front().getCuddAdd().NodeReadIndex(), names.size(), MTR_FIXED);
+                }
+            }
+            
             // Now add the meta variables.
             for (uint_fast64_t i = 0; i < names.size(); ++i) {
                 metaVariableMap.emplace(names[i], DdMetaVariable<DdType::CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 6df3dc25c..25844598c 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -103,8 +103,10 @@ namespace storm {
              * @param names The names of the variables.
              * @param low The lowest value of the ranges of the variables.
              * @param high The highest value of the ranges of the variables.
+             * @param fixedGroup If set to true, the interleaved bits of the meta variable are always kept together as
+             * a group during a potential reordering.
              */
-            void addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high);
+            void addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high, bool fixedGroup = true);
             
             /*!
              * Retrieves the meta variable with the given name if it exists.
diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp
index b9734a9ad..bb4ea0921 100644
--- a/src/storage/expressions/BaseExpression.cpp
+++ b/src/storage/expressions/BaseExpression.cpp
@@ -53,7 +53,12 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue) {
-            stream << static_cast<std::underlying_type<ExpressionReturnType>::type>(enumValue);
+            switch (enumValue) {
+                case ExpressionReturnType::Undefined: stream << "undefined"; break;
+                case ExpressionReturnType::Bool: stream << "bool"; break;
+                case ExpressionReturnType::Int: stream << "int"; break;
+                case ExpressionReturnType::Double: stream << "double"; break;
+            }
             return stream;
         }
         
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index 90570f244..51d085fe4 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -4,6 +4,7 @@
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/SubstitutionVisitor.h"
 #include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
+#include "src/storage/expressions/TypeCheckVisitor.h"
 #include "src/exceptions/InvalidTypeException.h"
 #include "src/exceptions/ExceptionMacros.h"
 
@@ -28,21 +29,29 @@ namespace storm {
         }
         
 		Expression Expression::substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const {
-            return SubstitutionVisitor< std::map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
+            return SubstitutionVisitor<std::map<std::string, Expression>>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
         }
 
 		Expression Expression::substitute(std::unordered_map<std::string, Expression> const& identifierToExpressionMap) const {
-			return SubstitutionVisitor< std::unordered_map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
+			return SubstitutionVisitor<std::unordered_map<std::string, Expression>>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
 		}
         
 		Expression Expression::substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const {
-			return IdentifierSubstitutionVisitor< std::map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
+			return IdentifierSubstitutionVisitor<std::map<std::string, std::string>>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
         }
 
 		Expression Expression::substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const {
-			return IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
+			return IdentifierSubstitutionVisitor<std::unordered_map<std::string, std::string>>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
 		}
         
+        void Expression::check(std::map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const {
+            return TypeCheckVisitor<std::map<std::string, storm::expressions::ExpressionReturnType>>(identifierToTypeMap).check(this->getBaseExpressionPointer().get());
+        }
+
+        void Expression::check(std::unordered_map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const {
+            return TypeCheckVisitor<std::unordered_map<std::string, storm::expressions::ExpressionReturnType>>(identifierToTypeMap).check(this->getBaseExpressionPointer().get());
+        }
+
         bool Expression::evaluateAsBool(Valuation const* valuation) const {
             return this->getBaseExpression().evaluateAsBool(valuation);
         }
@@ -79,6 +88,13 @@ namespace storm {
             return this->getBaseExpression().getConstants();
         }
         
+        std::set<std::string> Expression::getIdentifiers() const {
+            std::set<std::string> result = this->getConstants();
+            std::set<std::string> variables = this->getVariables();
+            result.insert(variables.begin(), variables.end());
+            return result;
+        }
+        
         BaseExpression const& Expression::getBaseExpression() const {
             return *this->expressionPtr;
         }
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 15936219c..36c367639 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -110,6 +110,22 @@ namespace storm {
 			*/
 			Expression substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const;
             
+            /*!
+             * Checks that all identifiers appearing in the expression have the types given by the map. An exception
+             * is thrown in case a violation is found.
+             *
+             * @param identifierToTypeMap A mapping from identifiers to the types that are supposed to have.
+             */
+            void check(std::map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const;
+            
+            /*!
+             * Checks that all identifiers appearing in the expression have the types given by the map. An exception
+             * is thrown in case a violation is found.
+             *
+             * @param identifierToTypeMap A mapping from identifiers to the types that are supposed to have.
+             */
+            void check(std::unordered_map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const;
+            
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
              * valuation and returns the resulting boolean value. If the return type of the expression is not a boolean
@@ -182,6 +198,13 @@ namespace storm {
              */
             std::set<std::string> getConstants() const;
             
+            /*!
+             * Retrieves the set of all identifiers (constants and variables) that appear in the expression.
+             *
+             * @return The est of all identifiers that appear in the expression.
+             */
+            std::set<std::string> getIdentifiers() const;
+            
             /*!
              * Retrieves the base expression underlying this expression object. Note that prior to calling this, the
              * expression object must be properly initialized.
diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp
index 54b533d49..7990ab4f9 100644
--- a/src/storage/expressions/SubstitutionVisitor.cpp
+++ b/src/storage/expressions/SubstitutionVisitor.cpp
@@ -3,20 +3,7 @@
 #include <string>
 
 #include "src/storage/expressions/SubstitutionVisitor.h"
-
-#include "src/storage/expressions/IfThenElseExpression.h"
-#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
-#include "src/storage/expressions/IntegerConstantExpression.h"
-#include "src/storage/expressions/DoubleConstantExpression.h"
-#include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
-#include "src/storage/expressions/VariableExpression.h"
-#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/Expressions.h"
 
 namespace storm {
     namespace expressions  {
@@ -195,7 +182,7 @@ namespace storm {
         }
         
         // Explicitly instantiate the class with map and unordered_map.
-		template class SubstitutionVisitor< std::map<std::string, Expression> >;
-		template class SubstitutionVisitor< std::unordered_map<std::string, Expression> >;
+		template class SubstitutionVisitor<std::map<std::string, Expression>>;
+		template class SubstitutionVisitor<std::unordered_map<std::string, Expression>>;
     }
 }
diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp
new file mode 100644
index 000000000..d5cef0381
--- /dev/null
+++ b/src/storage/expressions/TypeCheckVisitor.cpp
@@ -0,0 +1,101 @@
+#include "src/storage/expressions/TypeCheckVisitor.h"
+#include "src/storage/expressions/Expressions.h"
+
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidTypeException.h"
+
+namespace storm {
+    namespace expressions {
+        template<typename MapType>
+        TypeCheckVisitor<MapType>::TypeCheckVisitor(MapType const& identifierToTypeMap) : identifierToTypeMap(identifierToTypeMap) {
+            // Intentionally left empty.
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::check(BaseExpression const* expression) {
+            expression->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(IfThenElseExpression const* expression) {
+            expression->getCondition()->accept(this);
+            expression->getThenExpression()->accept(this);
+            expression->getElseExpression()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            expression->getSecondOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            expression->getSecondOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            expression->getSecondOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'bool', but found '" << expression->getReturnType() << "'.");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Double, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'double', but found '" << expression->getReturnType() << "'.");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Int, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'int', but found '" << expression->getReturnType() << "'.");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(VariableExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'.");
+            LOG_THROW(identifierTypePair->second == expression->getReturnType(), storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected '" << identifierTypePair->first << "', but found '" << expression->getReturnType() << "'.");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
+            expression->getOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
+            expression->getOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
+            // Intentionally left empty.
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
+            // Intentionally left empty.
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
+            // Intentionally left empty.
+        }
+        
+        // Explicitly instantiate the class with map and unordered_map.
+		template class TypeCheckVisitor<std::map<std::string, ExpressionReturnType>>;
+		template class TypeCheckVisitor<std::unordered_map<std::string, ExpressionReturnType>>;
+    }
+}
\ No newline at end of file
diff --git a/src/storage/expressions/TypeCheckVisitor.h b/src/storage/expressions/TypeCheckVisitor.h
new file mode 100644
index 000000000..e39a536a6
--- /dev/null
+++ b/src/storage/expressions/TypeCheckVisitor.h
@@ -0,0 +1,50 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_
+
+#include <stack>
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        template<typename MapType>
+        class TypeCheckVisitor : public ExpressionVisitor {
+        public:
+            /*!
+             * Creates a new type check visitor that uses the given map to check the types of variables and constants.
+             *
+             * @param identifierToTypeMap A mapping from identifiers to expressions.
+             */
+            TypeCheckVisitor(MapType const& identifierToTypeMap);
+            
+            /*!
+             * Checks that the types of the identifiers in the given expression match the ones in the previously given
+             * map.
+             *
+             * @param expression The expression in which to check the types.
+             */
+            void check(BaseExpression const* expression);
+            
+            virtual void visit(IfThenElseExpression const* expression) override;
+            virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BinaryRelationExpression const* expression) override;
+            virtual void visit(BooleanConstantExpression const* expression) override;
+            virtual void visit(DoubleConstantExpression const* expression) override;
+            virtual void visit(IntegerConstantExpression const* expression) override;
+            virtual void visit(VariableExpression const* expression) override;
+            virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(UnaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BooleanLiteralExpression const* expression) override;
+            virtual void visit(IntegerLiteralExpression const* expression) override;
+            virtual void visit(DoubleLiteralExpression const* expression) override;
+            
+        private:            
+            // A mapping of identifier names to expressions with which they shall be replaced.
+            MapType const& identifierToTypeMap;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_ */
\ No newline at end of file
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index 4b36942df..4c1619732 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -51,5 +51,5 @@ namespace storm {
             stream << ";";
             return stream;
         }
-    } // namespace ir
+    } // namespace prism
 } // namespace storm
diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index 641336c76..c02deea99 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -48,5 +48,5 @@ namespace storm {
             stream << ";";
             return stream;
         }
-    }
-}
\ No newline at end of file
+    } // namespace prism
+} // namespace storm
\ No newline at end of file
diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp
index fbda0c69d..a120078b8 100644
--- a/src/storage/prism/Formula.cpp
+++ b/src/storage/prism/Formula.cpp
@@ -26,5 +26,5 @@ namespace storm {
             stream << "formula " << formula.getName() << " = " << formula.getExpression() << ";";
             return stream;
         }
-    }
-}
\ No newline at end of file
+    } // namespace prism
+} // namespace storm
\ No newline at end of file
diff --git a/src/storage/prism/InitialConstruct.cpp b/src/storage/prism/InitialConstruct.cpp
new file mode 100644
index 000000000..61c662843
--- /dev/null
+++ b/src/storage/prism/InitialConstruct.cpp
@@ -0,0 +1,24 @@
+#include "src/storage/prism/InitialConstruct.h"
+
+namespace storm {
+    namespace prism {
+        InitialConstruct::InitialConstruct(storm::expressions::Expression initialStatesExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), initialStatesExpression(initialStatesExpression) {
+            // Intentionally left empty.
+        }
+        
+        storm::expressions::Expression InitialConstruct::getInitialStatesExpression() const {
+            return this->initialStatesExpression;
+        }
+        
+        InitialConstruct InitialConstruct::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return InitialConstruct(this->getInitialStatesExpression().substitute(substitution));
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct) {
+            stream << "initial " << std::endl;
+            stream << "\t" << initialConstruct.getInitialStatesExpression() << std::endl;
+            stream << "endinitial" << std::endl;
+            return stream;
+        }
+    } // namespace prism
+} // namespace storm
\ No newline at end of file
diff --git a/src/storage/prism/InitialConstruct.h b/src/storage/prism/InitialConstruct.h
new file mode 100644
index 000000000..6f7f6adb9
--- /dev/null
+++ b/src/storage/prism/InitialConstruct.h
@@ -0,0 +1,56 @@
+#ifndef STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_
+#define STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_
+
+#include <string>
+
+#include "src/storage/prism/LocatedInformation.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace prism {
+        class InitialConstruct : public LocatedInformation {
+            public:
+            /*!
+             * Creates an initial construct with the given expression.
+             *
+             * @param initialStatesExpression An expression characterizing the initial states.
+             * @param filename The filename in which the command is defined.
+             * @param lineNumber The line number in which the command is defined.
+             */
+            InitialConstruct(storm::expressions::Expression initialStatesExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            // Create default implementations of constructors/assignment.
+            InitialConstruct() = default;
+            InitialConstruct(InitialConstruct const& other) = default;
+            InitialConstruct& operator=(InitialConstruct const& other)= default;
+#ifndef WINDOWS
+            InitialConstruct(InitialConstruct&& other) = default;
+            InitialConstruct& operator=(InitialConstruct&& other) = default;
+#endif
+            
+            /*!
+             * Retrieves the expression characterizing the initial states.
+             *
+             * @return The expression characterizing the initial states.
+             */
+            storm::expressions::Expression getInitialStatesExpression() const;
+            
+            /*!
+             * Substitutes all identifiers in the constant according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting initial construct.
+             */
+            InitialConstruct substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct);
+            
+        private:
+            // An expression characterizing the initial states.
+            storm::expressions::Expression initialStatesExpression;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ */
\ No newline at end of file
diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp
index cb8a13f25..d11091cf0 100644
--- a/src/storage/prism/Label.cpp
+++ b/src/storage/prism/Label.cpp
@@ -22,5 +22,5 @@ namespace storm {
             stream << "label \"" << label.getName() << "\" = " << label.getStatePredicateExpression() << ";";
             return stream;
         }
-    }
-}
\ No newline at end of file
+    } // namespace prism
+} // namespace storm
\ No newline at end of file
diff --git a/src/storage/prism/LocatedInformation.cpp b/src/storage/prism/LocatedInformation.cpp
index a5a493319..a3862d57a 100644
--- a/src/storage/prism/LocatedInformation.cpp
+++ b/src/storage/prism/LocatedInformation.cpp
@@ -21,5 +21,5 @@ namespace storm {
         void LocatedInformation::setLineNumber(uint_fast64_t lineNumber) {
             this->lineNumber = lineNumber;
         }
-    }
-}
\ No newline at end of file
+    } // namespace prism
+} // namespace storm
\ No newline at end of file
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index f17e1bc12..6f4becb0a 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -2,10 +2,15 @@
 #include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/OutOfRangeException.h"
 #include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidAccessException.h"
 
 namespace storm {
     namespace prism {
-        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() {
+        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) : Module(moduleName, booleanVariables, integerVariables, commands, "", std::map<std::string, std::string>(), filename, lineNumber) {
+            // Intentionally left empty.
+        }
+        
+        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& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
             // Initialize the internal mappings for fast information retrieval.
             this->createMappings();
         }
@@ -71,6 +76,20 @@ namespace storm {
             return actionEntry != this->actions.end();
         }
         
+        bool Module::isRenamedFromModule() const {
+            return this->renamedFromModule != "";
+        }
+        
+        std::string const& Module::getBaseModule() const {
+            LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve base module of module that was not created by renaming.");
+            return this->renamedFromModule;
+        }
+        
+        std::map<std::string, std::string> const& Module::getRenaming() const {
+            LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve renaming of module that was not created by renaming.");
+            return this->renaming;
+        }
+        
         std::set<uint_fast64_t> const& Module::getCommandIndicesByAction(std::string const& action) const {
             auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
             if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
@@ -163,7 +182,6 @@ namespace storm {
             stream << "endmodule" << std::endl;
             return stream;
         }
-
         
-    } // namespace ir
+    } // namespace prism
 } // namespace storm
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index f4fd21f29..1031cbf27 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -2,6 +2,7 @@
 #define STORM_STORAGE_PRISM_MODULE_H_
 
 #include <set>
+#include <map>
 #include <string>
 #include <vector>
 #include <memory>
@@ -28,7 +29,22 @@ namespace storm {
              * @param lineNumber The line number in which the module is defined.
              */
             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);
-            
+
+            /*!
+             * Creates a module with the given name, variables and commands that is marked as being renamed from the
+             * given module with the given renaming.
+             *
+             * @param moduleName The name of the module.
+             * @param booleanVariables The boolean variables defined by the module.
+             * @param integerVariables The integer variables defined by the module.
+             * @param commands The commands of the module.
+             * @param renamedFromModule The name of the module from which this module was renamed.
+             * @param renaming The renaming of identifiers used to create this module.
+             * @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::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+
             // Create default implementations of constructors/assignment.
             Module() = default;
             Module(Module const& other) = default;
@@ -133,6 +149,29 @@ namespace storm {
              */
             bool hasAction(std::string const& action) const;
             
+            /*!
+             * Retrieves whether this module was created from another module via renaming.
+             *
+             * @return True iff the module was created via renaming.
+             */
+            bool isRenamedFromModule() const;
+            
+            /*!
+             * If the module was created via renaming, this method retrieves the name of the module that was used as the
+             * in the base in the renaming process.
+             *
+             * @return The name of the module from which this module was created via renaming.
+             */
+            std::string const& getBaseModule() const;
+            
+            /*!
+             * If the module was created via renaming, this method returns the applied renaming of identifiers used for
+             * the renaming process.
+             *
+             * @return A mapping of identifiers to new identifiers that was used in the renaming process.
+             */
+            std::map<std::string, std::string> const& getRenaming() const;
+            
             /*!
              * Retrieves the indices of all commands within this module that are labelled by the given action.
              *
@@ -188,6 +227,12 @@ namespace storm {
             
             // A map of actions to the set of commands labeled with this action.
             std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
+            
+            // This string indicates whether and from what module this module was created via renaming.
+            std::string renamedFromModule;
+            
+            // If the module was created by renaming, this mapping contains the provided renaming of identifiers.
+            std::map<std::string, std::string> renaming;
         };
         
     } // namespace prism
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 1c4118b8b..c29001b16 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -1,14 +1,46 @@
 #include "src/storage/prism/Program.h"
+
+#include <algorithm>
+
 #include "src/exceptions/ExceptionMacros.h"
 #include "exceptions/InvalidArgumentException.h"
 #include "src/exceptions/OutOfRangeException.h"
+#include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidTypeException.h"
 
 namespace storm {
     namespace prism {
-        Program::Program(ModelType modelType, std::vector<Constant> const& constants, 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), constants(constants), constantToIndexMap(), 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() {
+        Program::Program(ModelType modelType, std::vector<Constant> const& constants, 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 fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), labelToIndexMap(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
             this->createMappings();
+            
+            // Create a new initial construct if none was given explicitly.
+            if (fixInitialConstruct) {
+                if (this->getInitialConstruct().getInitialStatesExpression().isFalse()) {
+                    storm::expressions::Expression newInitialExpression = storm::expressions::Expression::createTrue();
+                    
+                    for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
+                        newInitialExpression = newInitialExpression && (storm::expressions::Expression::createBooleanVariable(booleanVariable.getName()).iff(booleanVariable.getInitialValueExpression()));
+                    }
+                    for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
+                        newInitialExpression = newInitialExpression && (storm::expressions::Expression::createIntegerVariable(integerVariable.getName()) == integerVariable.getInitialValueExpression());
+                    }
+                    for (auto const& module : this->getModules()) {
+                        for (auto const& booleanVariable : module.getBooleanVariables()) {
+                            newInitialExpression = newInitialExpression && (storm::expressions::Expression::createBooleanVariable(booleanVariable.getName()).iff(booleanVariable.getInitialValueExpression()));
+                        }
+                        for (auto const& integerVariable : module.getIntegerVariables()) {
+                            newInitialExpression = newInitialExpression && (storm::expressions::Expression::createIntegerVariable(integerVariable.getName()) == integerVariable.getInitialValueExpression());
+                        }
+                    }
+                    this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber());
+                }
+            }
+            
+            if (checkValidity) {
+                this->checkValidity();
+            }
         }
-        
+    
         Program::ModelType Program::getModelType() const {
             return modelType;
         }
@@ -93,28 +125,8 @@ namespace storm {
             return this->modules;
         }
         
-        bool Program::definesInitialStatesExpression() const {
-            return this->hasInitialStatesExpression;
-        }
-        
-        storm::expressions::Expression Program::getInitialStatesExpression() const {
-            // If the program specifies the initial states explicitly, we simply return the expression.
-            if (this->definesInitialStatesExpression()) {
-                return this->initialStatesExpression;
-            } else {
-                // Otherwise, we need to assert that all variables are equal to their initial value.
-                storm::expressions::Expression result = storm::expressions::Expression::createTrue();
-                
-                for (auto const& module : this->getModules()) {
-                    for (auto const& booleanVariable : module.getBooleanVariables()) {
-                        result = result && (storm::expressions::Expression::createBooleanVariable(booleanVariable.getName()).iff(booleanVariable.getInitialValueExpression()));
-                    }
-                    for (auto const& integerVariable : module.getIntegerVariables()) {
-                        result = result && (storm::expressions::Expression::createIntegerVariable(integerVariable.getName()) == integerVariable.getInitialValueExpression());
-                    }
-                }
-                return result;
-            }
+        storm::prism::InitialConstruct const& Program::getInitialConstruct() const {
+            return this->initialConstruct;
         }
         
         std::set<std::string> const& Program::getActions() const {
@@ -163,7 +175,7 @@ namespace storm {
                 newModules.push_back(module.restrictCommands(indexSet));
             }
             
-            return Program(this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
+            return Program(this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
         }
         
         void Program::createMappings() {
@@ -255,7 +267,7 @@ namespace storm {
                 LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
             }
             
-            return Program(this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
+            return Program(this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getRewardModels(), false, this->getInitialConstruct(), this->getLabels());
         }
         
         Program Program::substituteConstants() const {
@@ -306,7 +318,7 @@ namespace storm {
                 newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution));
             }
             
-            storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution);
+            storm::prism::InitialConstruct newInitialConstruct = this->getInitialConstruct().substitute(constantSubstitution);
             
             std::vector<Label> newLabels;
             newLabels.reserve(this->getNumberOfLabels());
@@ -314,7 +326,343 @@ namespace storm {
                 newLabels.emplace_back(label.substitute(constantSubstitution));
             }
             
-            return Program(this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels);
+            return Program(this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, false, newInitialConstruct, newLabels);
+        }
+        
+        void Program::checkValidity() const {
+            // We need to construct a mapping from identifiers to their types, so we can type-check the expressions later.
+            std::map<std::string, storm::expressions::ExpressionReturnType> identifierToTypeMap;
+            
+            // Start by checking the constant declarations.
+            std::set<std::string> allIdentifiers;
+            std::set<std::string> globalIdentifiers;
+            std::set<std::string> constantNames;
+            for (auto const& constant : this->getConstants()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(constant.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": duplicate identifier '" << constant.getName() << "'.");
+                
+                // Check defining expressions of defined constants.
+                if (constant.isDefined()) {
+                    LOG_THROW(constant.getExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": definition of constant " << constant.getName() << " must not refer to variables.");
+                    
+                    std::set<std::string> containedConstantNames = constant.getExpression().getConstants();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstantNames.begin(), containedConstantNames.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown constants.");
+                    
+                    // Now check that the constants appear with the right types.
+                    try {
+                        constant.getExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": " << e.what());
+                    }
+                }
+                
+                // Finally, register the type of the constant for later type checks.
+                identifierToTypeMap.emplace(constant.getName(), constant.getType());
+                
+                // Record the new identifier for future checks.
+                constantNames.insert(constant.getName());
+                allIdentifiers.insert(constant.getName());
+                globalIdentifiers.insert(constant.getName());
+            }
+            
+            // Now we check the variable declarations. We start with the global variables.
+            std::set<std::string> variableNames;
+            for (auto const& variable : this->getGlobalBooleanVariables()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                
+                // Check the initial value of the variable.
+                LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                std::set<std::string> containedConstants = variable.getInitialValueExpression().getConstants();
+                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                try {
+                variable.getInitialValueExpression().check(identifierToTypeMap);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                }
+
+                // Register the type of the constant for later type checks.
+                identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
+                
+                // Record the new identifier for future checks.
+                variableNames.insert(variable.getName());
+                allIdentifiers.insert(variable.getName());
+                globalIdentifiers.insert(variable.getName());
+            }
+            for (auto const& variable : this->getGlobalIntegerVariables()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                
+                // Check that bound expressions of the range.
+                LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables.");
+                std::set<std::string> containedConstants = variable.getLowerBoundExpression().getConstants();
+                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
+                try {
+                    variable.getLowerBoundExpression().check(identifierToTypeMap);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                }
+
+                LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables.");
+                containedConstants = variable.getLowerBoundExpression().getConstants();
+                isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
+                try {
+                    variable.getUpperBoundExpression().check(identifierToTypeMap);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                }
+                
+                // Check the initial value of the variable.
+                LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                containedConstants = variable.getInitialValueExpression().getConstants();
+                isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                try {
+                    variable.getInitialValueExpression().check(identifierToTypeMap);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                }
+                
+                // Register the type of the constant for later type checks.
+                identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
+
+                // Record the new identifier for future checks.
+                variableNames.insert(variable.getName());
+                allIdentifiers.insert(variable.getName());
+                globalIdentifiers.insert(variable.getName());
+            }
+
+            // Now go through the variables of the modules.
+            for (auto const& module : this->getModules()) {
+                for (auto const& variable : module.getBooleanVariables()) {
+                    // Check for duplicate identifiers.
+                    LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                    
+                    // Check the initial value of the variable.
+                    LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                    std::set<std::string> containedConstants = variable.getInitialValueExpression().getConstants();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                    try {
+                        variable.getInitialValueExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                    }
+                    
+                    // Register the type of the constant for later type checks.
+                    identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
+                    
+                    // Record the new identifier for future checks.
+                    variableNames.insert(variable.getName());
+                    allIdentifiers.insert(variable.getName());
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    // Check for duplicate identifiers.
+                    LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                    
+                    // Register the type of the constant for later type checks.
+                    identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
+                    
+                    // Check that bound expressions of the range.
+                    LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables.");
+                    std::set<std::string> containedConstants = variable.getLowerBoundExpression().getConstants();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
+                    try {
+                        variable.getLowerBoundExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                    }
+
+                    LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables.");
+                    containedConstants = variable.getLowerBoundExpression().getConstants();
+                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
+                    try {
+                        variable.getUpperBoundExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                    }
+                    
+                    // Check the initial value of the variable.
+                    LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                    containedConstants = variable.getInitialValueExpression().getConstants();
+                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                    try {
+                        variable.getInitialValueExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": " << e.what());
+                    }
+                    
+                    // Record the new identifier for future checks.
+                    variableNames.insert(variable.getName());
+                    allIdentifiers.insert(variable.getName());
+                }
+            }
+            
+            // Create the set of valid identifiers for future checks.
+            std::set<std::string> variablesAndConstants;
+            std::set_union(variableNames.begin(), variableNames.end(), constantNames.begin(), constantNames.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
+            
+            // Check the commands of the modules.
+            for (auto const& module : this->getModules()) {
+                std::set<std::string> legalIdentifiers = globalIdentifiers;
+                for (auto const& variable : module.getBooleanVariables()) {
+                    legalIdentifiers.insert(variable.getName());
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    legalIdentifiers.insert(variable.getName());
+                }
+                
+                for (auto const& command : module.getCommands()) {
+                    // Check the guard.
+                    std::set<std::string> containedIdentifiers = command.getGuardExpression().getIdentifiers();
+                    bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard refers to unknown identifiers.");
+                    try {
+                        command.getGuardExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
+                    }
+                    LOG_THROW(command.getGuardExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
+                    
+                    // Check all updates.
+                    for (auto const& update : command.getUpdates()) {
+                        containedIdentifiers = update.getLikelihoodExpression().getIdentifiers();
+                        isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                        LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
+                        try {
+                            update.getLikelihoodExpression().check(identifierToTypeMap);
+                        } catch (storm::exceptions::InvalidTypeException const& e) {
+                            LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
+                        }
+                        
+                        // Check all assignments.
+                        std::set<std::string> alreadyAssignedIdentifiers;
+                        for (auto const& assignment : update.getAssignments()) {
+                            if (legalIdentifiers.find(assignment.getVariableName()) == legalIdentifiers.end()) {
+                                if (allIdentifiers.find(assignment.getVariableName()) != allIdentifiers.end()) {
+                                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
+                                } else {
+                                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment refers to unknown variable '" << assignment.getVariableName() << "'.");
+                                }
+                            }
+                            LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
+                            auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName());
+                            LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'.");
+                            
+                            containedIdentifiers = assignment.getExpression().getIdentifiers();
+                            isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                            LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers.");
+                            try {
+                                assignment.getExpression().check(identifierToTypeMap);
+                            } catch (storm::exceptions::InvalidTypeException const& e) {
+                                LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": " << e.what());
+                            }
+                            
+                            // Add the current variable to the set of assigned variables (of this update).
+                            alreadyAssignedIdentifiers.insert(assignment.getVariableName());
+                        }
+                    }
+                }
+            }
+            
+            // Now check the reward models.
+            for (auto const& rewardModel : this->getRewardModels()) {
+                for (auto const& stateReward : rewardModel.getStateRewards()) {
+                    std::set<std::string> containedIdentifiers = stateReward.getStatePredicateExpression().getIdentifiers();
+                    bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
+                    try {
+                        stateReward.getStatePredicateExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": " << e.what());
+                    }
+                    LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
+                    
+                    containedIdentifiers = stateReward.getRewardValueExpression().getIdentifiers();
+                    isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
+                    try {
+                        stateReward.getRewardValueExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": " << e.what());
+                    }
+                    LOG_THROW(stateReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
+                }
+                
+                for (auto const& transitionReward : rewardModel.getTransitionRewards()) {
+                    std::set<std::string> containedIdentifiers = transitionReward.getStatePredicateExpression().getIdentifiers();
+                    bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
+                    try {
+                        transitionReward.getStatePredicateExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": " << e.what());
+                    }
+                    LOG_THROW(transitionReward.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
+                    
+                    containedIdentifiers = transitionReward.getRewardValueExpression().getIdentifiers();
+                    isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
+                    try {
+                        transitionReward.getRewardValueExpression().check(identifierToTypeMap);
+                    } catch (storm::exceptions::InvalidTypeException const& e) {
+                        LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": " << e.what());
+                    }
+                    LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalReturnType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
+                }
+            }
+            
+            // Check the initial states expression.
+            std::set<std::string> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getIdentifiers();
+            bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+            LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial expression refers to unknown identifiers.");
+            try {
+                this->getInitialConstruct().getInitialStatesExpression().check(identifierToTypeMap);
+            } catch (storm::exceptions::InvalidTypeException const& e) {
+                LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": " << e.what());
+            }
+            
+            // Check the labels.
+            for (auto const& label : this->getLabels()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'.");
+                
+                std::set<std::string> containedIdentifiers = label.getStatePredicateExpression().getIdentifiers();
+                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
+                try {
+                    label.getStatePredicateExpression().check(identifierToTypeMap);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": " << e.what());
+                }
+                
+                LOG_THROW(label.getStatePredicateExpression().hasBooleanReturnType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
+            }
+            
+            // Check the formulas.
+            for (auto const& formula : this->getFormulas()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'.");
+                
+                std::set<std::string> containedIdentifiers = formula.getExpression().getIdentifiers();
+                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
+                try {
+                    formula.getExpression().check(identifierToTypeMap);
+                } catch (storm::exceptions::InvalidTypeException const& e) {
+                    LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": " << e.what());
+                }
+                
+                // Record the new identifier for future checks.
+                allIdentifiers.insert(formula.getName());
+            }
         }
         
         std::ostream& operator<<(std::ostream& stream, Program const& program) {
@@ -361,5 +709,5 @@ namespace storm {
             return stream;
         }
         
-    } // namespace ir
+    } // namespace prism
 } // namepsace storm
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 40f8047e1..2a618ff7a 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -12,6 +12,7 @@
 #include "src/storage/prism/Label.h"
 #include "src/storage/prism/Module.h"
 #include "src/storage/prism/RewardModel.h"
+#include "src/storage/prism/InitialConstruct.h"
 #include "src/utility/OsDetection.h"
 
 namespace storm {
@@ -33,17 +34,18 @@ namespace storm {
              * @param globalIntegerVariables The global integer variables of the program.
              * @param formulas The formulas defined in the program.
              * @param modules The modules of the program.
-             * @param hasInitialStatesExpression A flag indicating whether the program specifies its initial states via
-             * an explicit initial construct.
-             * @param initialStatesExpression If the model specifies an explicit initial construct, this
-             * expression defines its initial states. Otherwise it is irrelevant and may be set to an arbitrary (but
-             * valid) expression, e.g. false.
+             * @param fixInitialConstruct A flag that indicates whether the given initial construct is to be ignored and
+             * replaced by a new one created from the initial values of the variables.
+             * @param initialConstruct The initial construct of the program. If the initial construct specifies "false"
+             * as the initial condition, the default values of the variables are used to construct a legal initial
+             * condition.
              * @param rewardModels The reward models of the program.
              * @param labels The labels defined for this program.
              * @param filename The filename in which the program is defined.
              * @param lineNumber The line number in which the program is defined.
+             * @param checkValidity If set to true, the program is checked for validity.
              */
-            Program(ModelType modelType, std::vector<Constant> const& constants, 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);
+            Program(ModelType modelType, std::vector<Constant> const& constants, 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 fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool checkValidity = true);
             
             // Provide default implementations for constructors and assignments.
             Program() = default;
@@ -187,18 +189,11 @@ namespace storm {
             std::vector<Module> const& getModules() const;
             
             /*!
-             * Retrieves whether the program explicitly specifies an expression characterizing the initial states.
+             * Retrieves the initial construct of the program.
              *
-             * @return True iff the program specifies an expression defining the initial states.
+             * @return The initial construct of the program.
              */
-            bool definesInitialStatesExpression() const;
-            
-            /*!
-             * Retrieves an expression characterizing the initial states of the program.
-             *
-             * @return An expression characterizing the initial states.
-             */
-            storm::expressions::Expression getInitialStatesExpression() const;
+            storm::prism::InitialConstruct const& getInitialConstruct() const;
             
             /*!
              * Retrieves the set of actions present in the program.
@@ -285,6 +280,12 @@ namespace storm {
              */
             Program substituteConstants() const;
             
+            /*!
+             * Checks the validity of the program. If the program is not valid, an exception is thrown with a message
+             * that indicates the source of the problem.
+             */
+            void checkValidity() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
         private:
@@ -330,12 +331,8 @@ namespace storm {
             // 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).
-            bool hasInitialStatesExpression;
-            
-            // The expression contained in the initial construct (if any).
-            storm::expressions::Expression initialStatesExpression;
+            // The initial construct of the program.
+            storm::prism::InitialConstruct initialConstruct;
             
             // The labels that are defined for this model.
             std::vector<Label> labels;
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
index 5d65e6dd5..9082bc6f1 100644
--- a/src/storage/prism/Update.cpp
+++ b/src/storage/prism/Update.cpp
@@ -60,5 +60,5 @@ namespace storm {
             return stream;
         }
         
-    } // namespace ir
+    } // namespace prism
 } // namespace storm
diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp
index 81731114b..5bf7bfd49 100644
--- a/test/functional/parser/PrismParserTest.cpp
+++ b/test/functional/parser/PrismParserTest.cpp
@@ -2,47 +2,20 @@
 #include "storm-config.h"
 #include "src/parser/PrismParser.h"
 
-TEST(PrismParser, SimpleParsingOnlyTest) {
-    std::string testInput =
-    R"(dtmc
-    module mod1
-        b : bool;
-        [a] true -> 1: (b'=true);
-    endmodule)";
-    
+TEST(PrismParser, StandardModelTest) {
     storm::prism::Program result;
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false));
-    EXPECT_EQ(1, result.getNumberOfModules());
-    EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
-}
-
-TEST(PrismParser, StandardModelParsingTest) {
-    storm::prism::Program result;
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3_5.pm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm", false));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm", false));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3_5.pm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm"));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm"));
 }
 
-TEST(PrismParser, StandardModelFullTest) {
-    storm::prism::Program result;
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3_5.pm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm", true));
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm", true));
-}
-
-TEST(PrismParser, SimpleFullTest) {
+TEST(PrismParser, SimpleTest) {
     std::string testInput =
     R"(dtmc
     module mod1
@@ -51,12 +24,27 @@ TEST(PrismParser, SimpleFullTest) {
     endmodule)";
     
     storm::prism::Program result;
-    EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true));
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
     EXPECT_EQ(1, result.getNumberOfModules());
     EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
+    
+    testInput =
+    R"(mdp
+    
+    module main
+        x : [1..5] init 1;
+        [] x=1 -> 1:(x'=2);
+        [] x=2 -> 1:(x'=3);
+        [] x=3 -> 1:(x'=1);
+        [] x=3 -> 1:(x'=4);
+        [] x=4 -> 1:(x'=5);
+    endmodule)";
+    EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
+    EXPECT_EQ(1, result.getNumberOfModules());
+    EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType());
 }
 
-TEST(PrismParser, ComplexFullTest) {
+TEST(PrismParser, ComplexTest) {
     std::string testInput =
     R"(ma
     
@@ -79,11 +67,11 @@ TEST(PrismParser, ComplexFullTest) {
         j : bool init c;
         k : [125..a] init a;
 
-        [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(a) <= max(k, b) - 1 + k);
+        [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(a) + max(k, b) - 1 + k);
     endmodule
                                               
     module mod2
-        [b] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (j'=(1-a) * 2 + floor(f));
+        [b] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (g'=(1-a) * 2 + floor(f) > 2);
     endmodule
     
     module mod3 = mod1 [ i = i1, j = j1, k = k1 ] endmodule
@@ -105,66 +93,131 @@ TEST(PrismParser, ComplexFullTest) {
     endrewards)";
     
     storm::prism::Program result;
-    result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true);
+    result = storm::parser::PrismParser::parseFromString(testInput, "testfile");
     EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType());
     EXPECT_EQ(3, result.getNumberOfModules());
     EXPECT_EQ(2, result.getNumberOfRewardModels());
     EXPECT_EQ(1, result.getNumberOfLabels());
-    EXPECT_TRUE(result.definesInitialStatesExpression());
 }
 
-TEST(PrismParser, ComplexParsingTest) {
+TEST(PrismParser, IllegalInputTest) {
     std::string testInput =
-    R"(ma
+    R"(ctmc
+
+    const int a;
+    const bool a = true;
+    
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c < 3 -> 2: (c' = c+1); 
+    endmodule
+    )";
+    
+    storm::prism::Program result;
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
     
     const int a;
-    const int b = 10;
-    const bool c;
-    const bool d = true | false;
-    const double e;
-    const double f = 9;
     
-    formula test = (a >= 10 & (max(a, b) > floor(e)));
+    module mod1
+        a : [0 .. 8] init 1;
+        [] a < 3 -> 1: (a' = a+1); 
+    endmodule)";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
+    
+    const int a = 2;
+    formula a = 41;
+    
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c < 3 -> 1: (c' = c+1); 
+    endmodule)";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
+    
+    const int a = 2;
+    
+    init
+        c > 3
+    endinit
+    
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c < 3 -> 1: (c' = c+1); 
+    endmodule
+        
+    init
+        c > 3
+    endinit
 
-    global g : bool init false;
-    global h : [0 .. b];
+    )";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
     
     module mod1
-        i : bool;
-        j : bool init c;
-        k : [125..a] init a;
-        [a] true -> (i'=true)&(h'=1+1) + 1 : (j'=floor(a) <= max(k, b) - 1 + k);
+        c : [0 .. 8] init 1;
+        [] c < 3 -> 1: (c' = c+1);
     endmodule
-                                    
+                    
     module mod2
-        [b] (x > 3) & false & (min(a, b0) < max(as8, b)) -> y: (x'=(1-g) * 2 + a);
-        [] s=1 -> (a'=a);
-        [read] c<N-1 -> 1 : (c'=floor(c) + 1);
+        [] c < 3 -> 1: (c' = c+1);
+    endmodule)";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+                        
+    testInput =
+    R"(dtmc
+                        
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c < 3 -> 1: (c' = c+1)&(c'=c-1);
+    endmodule)";
+                                        
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
+    
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c < 3 -> 1: (c' = true || false);
+    endmodule)";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
+    
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c + 3 -> 1: (c' = 1);
+    endmodule)";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
+    
+    testInput =
+    R"(dtmc
+    
+    module mod1
+        c : [0 .. 8] init 1;
+        [] c + 3 -> 1: (c' = 1);
     endmodule
-                             
-    module mod3 = mod2 [ x = y ] endmodule
-             
-    label "mal" = max(x, i) > 0;
-                             
-    init
-        true
-    endinit
-                             
-    rewards "testrewards"
-        [stateRew] true : a + 7;
-        max(z, f) <= 8 : 2*b;
-    endrewards
-                             
-    rewards "testrewards2"
-        [stateRew] true : a + 7;
-        max(z, f) <= 8 : 2*b;
-    endrewards)";
     
-    storm::prism::Program result;
-    result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false);
-    EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType());
-    EXPECT_EQ(3, result.getNumberOfModules());
-    EXPECT_EQ(2, result.getNumberOfRewardModels());
-    EXPECT_EQ(1, result.getNumberOfLabels());
-    EXPECT_TRUE(result.definesInitialStatesExpression());
+    label "test" = c + 1;
+    
+    )";
+    
+    EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException);
 }
\ No newline at end of file