diff --git a/examples/mdp/consensus/coin2.nm b/examples/mdp/consensus/coin2.nm
index 07ec59e17..a08bb8741 100644
--- a/examples/mdp/consensus/coin2.nm
+++ b/examples/mdp/consensus/coin2.nm
@@ -29,18 +29,18 @@ module process1
 	// flip coin
 	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
 	// write tails -1  (reset coin to add regularity)
-	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0);
 	// write heads +1 (reset coin to add regularity)
-	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0);
 	// check
 	// decide tails
-	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0);
 	// decide heads
-	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1);
 	// flip again
-	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0);
 	// loop (all loop together when done)
-	[done] (pc1=3) -> (pc1'=3);
+	[done] (pc1=3) -> 1 : (pc1'=3);
 
 endmodule
 
diff --git a/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt b/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt
index be347664f..319db1c64 100644
--- a/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt
+++ b/resources/3rdparty/log4cplus-1.1.2-rc2/CMakeLists.txt
@@ -33,9 +33,17 @@ endif (WIN32)
 
 if (MSVC)
   set (LOG4CPLUS_WORKING_LOCALE_DEFAULT ON)
-else (MSVC)
+elseif(CMAKE_COMPILER_IS_GNUCC)
   set (CMAKE_CXX_FLAGS "-std=c++11")
   set (LOG4CPLUS_WORKING_LOCALE_DEFAULT OFF)
+else(CLANG)
+	set (CLANG ON)
+    if(UNIX AND NOT APPLE)
+      set(CLANG_STDLIB libstdc++)
+    else()
+      set(CLANG_STDLIB libc++)
+    endif()
+    set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=${CLANG_STDLIB}")
 endif (MSVC)
 
 option(LOG4CPLUS_WORKING_LOCALE "Define for compilers/standard libraries that support more than just the C locale."
diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp
index 55d476e47..0d9eb7cf7 100644
--- a/src/adapters/ExplicitModelAdapter.cpp
+++ b/src/adapters/ExplicitModelAdapter.cpp
@@ -15,6 +15,8 @@
 #include "src/models/Mdp.h"
 #include "src/models/Ctmdp.h"
 
+#include <boost/algorithm/string.hpp>
+
 #include <sstream>
 
 #include "log4cplus/logger.h"
@@ -37,7 +39,60 @@ namespace storm {
             this->clearInternalState();
         }
         
-        std::shared_ptr<storm::models::AbstractModel<double>> ExplicitModelAdapter::getModel(std::string const& rewardModelName) {
+        std::shared_ptr<storm::models::AbstractModel<double>> ExplicitModelAdapter::getModel(std::string const& constantDefinitionString, std::string const& rewardModelName) {
+            // Parse the string that defines the undefined constants of the model and make sure that it contains exactly
+            // one value for each undefined constant of the model.
+            std::vector<std::string> definitions;
+            boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
+            for (auto& definition : definitions) {
+                boost::trim(definition);
+                
+                // Check whether the token could be a legal constant definition.
+                uint_fast64_t positionOfAssignmentOperator = definition.find('=');
+                if (positionOfAssignmentOperator == std::string::npos) {
+                    throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error.";
+                }
+
+                // Now extract the variable name and the value from the string.
+                std::string constantName = definition.substr(0, positionOfAssignmentOperator);
+                boost::trim(constantName);
+                std::string value = definition.substr(positionOfAssignmentOperator + 1);
+                boost::trim(value);
+                
+                // Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
+                if (program.hasUndefinedBooleanConstant(constantName)) {
+                    if (value == "true") {
+                        program.getUndefinedBooleanConstantExpression(constantName)->define(true);
+                    } else if (value == "false") {
+                        program.getUndefinedBooleanConstantExpression(constantName)->define(false);
+                    } else {
+                        throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
+                    }
+                } else if (program.hasUndefinedIntegerConstant(constantName)) {
+                    try {
+                        int_fast64_t integerValue = std::stoi(value);
+                        program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue);
+                    } catch (std::invalid_argument const& e) {
+                        throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << ".";
+                    } catch (std::out_of_range const& e) {
+                        throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big).";
+                    }
+                } else if (program.hasUndefinedDoubleConstant(constantName)) {
+                    try {
+                        double doubleValue = std::stod(value);
+                        program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue);
+                    } catch (std::invalid_argument const& e) {
+                        throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << ".";
+                    } catch (std::out_of_range const& e) {
+                        throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big).";
+                    }
+
+                } else {
+                    throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";
+                }
+                
+            }
+            
             // Initialize reward model.
             this->rewardModel = nullptr;
             if (rewardModelName != "") {
@@ -149,15 +204,27 @@ namespace storm {
             uint_fast64_t numberOfBooleanVariables = 0;
             
             // Count number of variables.
+            numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables();
+            numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables();
             for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
-                numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables();
                 numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables();
+                numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables();
             }
             
             this->booleanVariables.resize(numberOfBooleanVariables);
             this->integerVariables.resize(numberOfIntegerVariables);
             
             // Create variables.
+            for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) {
+                storm::ir::BooleanVariable var = program.getGlobalBooleanVariable(i);
+                this->booleanVariables[var.getGlobalIndex()] = var;
+                this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex();
+            }
+            for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) {
+                storm::ir::IntegerVariable var = program.getGlobalIntegerVariable(i);
+                this->integerVariables[var.getGlobalIndex()] = var;
+                this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex();
+            }
             for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
                 storm::ir::Module const& module = program.getModule(i);
                 
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 78f36f9c0..a691bb05a 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -75,12 +75,14 @@ namespace storm {
              * Convert the program given at construction time to an abstract model. The type of the model is the one
              * specified in the program. The given reward model name selects the rewards that the model will contain.
              *
+             * @param constantDefinitionString A string that contains a comma-separated definition of all undefined
+             * constants in the model.
              * @param rewardModelName The name of reward model to be added to the model. This must be either a reward
              * model of the program or the empty string. In the latter case, the constructed model will contain no 
              * rewards.
              * @return The explicit model that was given by the probabilistic program.
              */
-            std::shared_ptr<storm::models::AbstractModel<double>> getModel(std::string const& rewardModelName = "");
+            std::shared_ptr<storm::models::AbstractModel<double>> getModel(std::string const& constantDefinitionString = "", std::string const& rewardModelName = "");
             
         private:
             // Copying/Moving is disabled for this class
diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h
index a827b5635..5ff42b59b 100644
--- a/src/counterexamples/MinimalLabelSetGenerator.h
+++ b/src/counterexamples/MinimalLabelSetGenerator.h
@@ -12,10 +12,9 @@
 #include <gurobi_c++.h>
 #endif
 
-#include "src/models/Mdp.h" 
+#include "src/models/Mdp.h"
 #include "src/exceptions/NotImplementedException.h"
-#include "src/storage/SparseMatrix.h"
-#include "src/storage/BitVector.h"
+#include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace counterexamples {
@@ -27,10 +26,50 @@ namespace storm {
         template <class T>
         class MinimalLabelSetGenerator {
 
+        public:
+            
             static std::unordered_set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T lowerProbabilityBound, bool checkThresholdFeasible = false) {
 #ifdef HAVE_GUROBI
-                // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
-                // (2) Identify relevant labels and states.
+                // (0) Check whether the MDP is indeed labeled.
+                if (!labeledMdp.hasChoiceLabels()) {
+                    throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model.";
+                }
+                
+                // (1) TODO: check whether its possible to exceed the threshold if checkThresholdFeasible is set.
+                
+                // (2) Identify relevant and problematic states.
+                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::BitVector relevantStates = storm::utility::graph::performProbGreater0A(labeledMdp, backwardTransitions, phiStates, psiStates);
+                relevantStates.complement();
+                storm::storage::BitVector problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates);
+                problematicStates &= relevantStates;
+                
+                // (3) Determine set of relevant labels.
+                std::unordered_set<uint_fast64_t> relevantLabels;
+                storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
+                std::vector<std::list<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
+                // Now traverse all choices of all relevant states and check whether there is a relevant target state.
+                // If so, the associated labels become relevant.
+                for (auto state : relevantStates) {
+                    for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state - 1]; ++row) {
+                        for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) {
+                            // If there is a relevant successor, we need to add the labels of the current choice.
+                            if (relevantStates.get(*successorIt)) {
+                                for (auto const& label : choiceLabeling[row]) {
+                                    relevantLabels.insert(label);
+                                }
+                            }
+                        }
+                    }
+                }
+                std::cout << "relevant labels: " << std::endl;
+                for (auto const& label : relevantLabels) {
+                    std::cout << "label: " << label << std::endl;
+                }
+                
+                return relevantLabels;
+                
                 // (3) Encode resulting system as MILP problem.
                 //  (3.1) Initialize MILP solver.
                 //  (3.2) Create variables.
diff --git a/src/ir/Module.h b/src/ir/Module.h
index f79fa14a0..03e4d0be8 100644
--- a/src/ir/Module.h
+++ b/src/ir/Module.h
@@ -51,8 +51,8 @@ namespace storm {
              * @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 booleanVariableToLocalIndexMap A mapping of boolean variables to global (i.e. module-local) indices.
-             * @param integerVariableToLocalIndexMap A mapping of integer variables to global (i.e. module-local) indices.
+             * @param booleanVariableToLocalIndexMap A mapping of boolean variables to local (i.e. module-local) indices.
+             * @param integerVariableToLocalIndexMap A mapping of integer variables to local (i.e. module-local) indices.
              * @param commands The commands of the module.
              */
             Module(std::string const& moduleName, std::vector<storm::ir::BooleanVariable> const& booleanVariables,
diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp
index 276b59134..eb21aa9f2 100644
--- a/src/ir/Program.cpp
+++ b/src/ir/Program.cpp
@@ -23,8 +23,18 @@ namespace storm {
             // Nothing to do here.
         }
         
-        Program::Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels)
-        : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() {
+        Program::Program(ModelType modelType,
+                         std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
+                         std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
+                         std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
+                         std::vector<BooleanVariable> const& globalBooleanVariables,
+                         std::vector<IntegerVariable> const& globalIntegerVariables,
+                         std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
+                         std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
+                         std::vector<storm::ir::Module> const& modules,
+                         std::map<std::string, storm::ir::RewardModel> const& rewards,
+                         std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels)
+        : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() {
             // Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
             for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) {
                 Module const& module = this->modules[moduleIndex];
@@ -88,6 +98,14 @@ namespace storm {
             return result.str();
         }
         
+        storm::ir::BooleanVariable const& Program::getGlobalBooleanVariable(uint_fast64_t index) const {
+            return this->globalBooleanVariables[index];
+        }
+        
+        storm::ir::IntegerVariable const& Program::getGlobalIntegerVariable(uint_fast64_t index) const {
+            return this->globalIntegerVariables[index];
+        }
+        
         uint_fast64_t Program::getNumberOfModules() const {
             return this->modules.size();
         }
@@ -117,6 +135,14 @@ namespace storm {
             throw storm::exceptions::OutOfRangeException() << "Variable '" << variableName << "' does not exist.";
         }
         
+        uint_fast64_t Program::getNumberOfGlobalBooleanVariables() const {
+            return this->globalBooleanVariables.size();
+        }
+        
+        uint_fast64_t Program::getNumberOfGlobalIntegerVariables() const {
+            return this->globalIntegerVariables.size();
+        }
+        
         storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const {
             auto nameRewardModelPair = this->rewards.find(name);
             if (nameRewardModelPair == this->rewards.end()) {
@@ -130,5 +156,44 @@ namespace storm {
             return this->labels;
         }
         
+        bool Program::hasUndefinedBooleanConstant(std::string const& constantName) const {
+            return this->booleanUndefinedConstantExpressions.find(constantName) != this->booleanUndefinedConstantExpressions.end();
+        }
+        
+        std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const {
+            auto constantExpressionPair = this->booleanUndefinedConstantExpressions.find(constantName);
+            if (constantExpressionPair != this->booleanUndefinedConstantExpressions.end()) {
+                return constantExpressionPair->second;
+            } else {
+                throw storm::exceptions::InvalidArgumentException() << "Unknown undefined boolean constant " << constantName << ".";
+            }
+        }
+        
+        bool Program::hasUndefinedIntegerConstant(std::string const& constantName) const {
+            return this->integerUndefinedConstantExpressions.find(constantName) != this->integerUndefinedConstantExpressions.end();
+        }
+        
+        std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const {
+            auto constantExpressionPair = this->integerUndefinedConstantExpressions.find(constantName);
+            if (constantExpressionPair != this->integerUndefinedConstantExpressions.end()) {
+                return constantExpressionPair->second;
+            } else {
+                throw storm::exceptions::InvalidArgumentException() << "Unknown undefined integer constant " << constantName << ".";
+            }
+        }
+        
+        bool Program::hasUndefinedDoubleConstant(std::string const& constantName) const {
+            return this->doubleUndefinedConstantExpressions.find(constantName) != this->doubleUndefinedConstantExpressions.end();
+        }
+        
+        std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const {
+            auto constantExpressionPair = this->doubleUndefinedConstantExpressions.find(constantName);
+            if (constantExpressionPair != this->doubleUndefinedConstantExpressions.end()) {
+                return constantExpressionPair->second;
+            } else {
+                throw storm::exceptions::InvalidArgumentException() << "Unknown undefined double constant " << constantName << ".";
+            }
+        }
+        
     } // namespace ir
 } // namepsace storm
diff --git a/src/ir/Program.h b/src/ir/Program.h
index 23d154110..ae92db0de 100644
--- a/src/ir/Program.h
+++ b/src/ir/Program.h
@@ -49,17 +49,27 @@ namespace storm {
              * expression nodes.
              * @param doubleUndefinedConstantExpressions A map of undefined double constants to their
              * expression nodes.
+             * @param globalBooleanVariables A list of global boolean variables.
+             * @param globalIntegerVariables A list of global integer variables.
+             * @param globalBooleanVariableToIndexMap A mapping from global boolean variable names to the index in the
+             * list of global boolean variables.
+             * @param globalIntegerVariableToIndexMap A mapping from global integer variable names to the index in the
+             * list of global integer variables.
              * @param modules The modules of the program.
              * @param rewards The reward models of the program.
              * @param labels The labels defined for this model.
              */
             Program(ModelType modelType,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions,
-                    std::vector<storm::ir::Module> modules,
-                    std::map<std::string, storm::ir::RewardModel> rewards,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels);
+                    std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
+                    std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
+                    std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
+                    std::vector<BooleanVariable> const& globalBooleanVariables,
+                    std::vector<IntegerVariable> const& globalIntegerVariables,
+                    std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
+                    std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
+                    std::vector<storm::ir::Module> const& modules,
+                    std::map<std::string, storm::ir::RewardModel> const& rewards,
+                    std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels);
             
             /*!
              * Retrieves the number of modules in the program.
@@ -90,6 +100,20 @@ namespace storm {
              */
             std::string toString() const;
             
+            /*!
+             * Retrieves a reference to the global boolean variable with the given index.
+             *
+             * @return A reference to the global boolean variable with the given index.
+             */
+            storm::ir::BooleanVariable const& getGlobalBooleanVariable(uint_fast64_t index) const;
+            
+            /*!
+             * Retrieves a reference to the global integer variable with the given index.
+             *
+             * @return A reference to the global integer variable with the given index.
+             */
+            storm::ir::IntegerVariable const& getGlobalIntegerVariable(uint_fast64_t index) const;
+            
             /*!
              * Retrieves the set of actions present in this module.
              *
@@ -114,6 +138,20 @@ namespace storm {
              */
             uint_fast64_t getModuleIndexForVariable(std::string const& variableName) const;
             
+            /*!
+             * Retrieves the number of global boolean variables of the program.
+             *
+             * @return The number of global boolean variables of the program.
+             */
+            uint_fast64_t getNumberOfGlobalBooleanVariables() const;
+            
+            /*!
+             * Retrieves the number of global integer variables of the program.
+             *
+             * @return The number of global integer variables of the program.
+             */
+            uint_fast64_t getNumberOfGlobalIntegerVariables() const;
+            
             /*!
              * Retrieves the reward model with the given name.
              *
@@ -129,6 +167,51 @@ namespace storm {
              */
             std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() const;
             
+            /*!
+             * Retrieves whether the given constant name is an undefined boolean constant of the program.
+             *
+             * @return True if the given constant name is an undefined boolean constant of the program.
+             */
+            bool hasUndefinedBooleanConstant(std::string const& constantName) const;
+            
+            /*!
+             * Retrieves the expression associated with the given undefined boolean constant.
+             *
+             * @param constantName The name of the undefined boolean constant for which to retrieve the expression.
+             * @return The expression associated with the given undefined boolean constant.
+             */
+            std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> getUndefinedBooleanConstantExpression(std::string const& constantName) const;
+            
+            /*!
+             * Retrieves whether the given constant name is an undefined integer constant of the program.
+             *
+             * @return True if the given constant name is an undefined integer constant of the program.
+             */
+            bool hasUndefinedIntegerConstant(std::string const& constantName) const;
+            
+            /*!
+             * Retrieves the expression associated with the given undefined integer constant.
+             *
+             * @param constantName The name of the undefined integer constant for which to retrieve the expression.
+             * @return The expression associated with the given undefined integer constant.
+             */
+            std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> getUndefinedIntegerConstantExpression(std::string const& constantName) const;
+
+            /*!
+             * Retrieves whether the given constant name is an undefined double constant of the program.
+             *
+             * @return True if the given constant name is an undefined double constant of the program.
+             */
+            bool hasUndefinedDoubleConstant(std::string const& constantName) const;
+            
+            /*!
+             * Retrieves the expression associated with the given undefined double constant.
+             *
+             * @param constantName The name of the undefined double constant for which to retrieve the expression.
+             * @return The expression associated with the given undefined double constant.
+             */
+            std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> getUndefinedDoubleConstantExpression(std::string const& constantName) const;
+            
         private:
             // The type of the model.
             ModelType modelType;
@@ -142,6 +225,18 @@ namespace storm {
             // A map of undefined double constants to their expressions nodes.
             std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
             
+            // A list of global boolean variables.
+            std::vector<BooleanVariable> globalBooleanVariables;
+            
+            // A list of global integer variables.
+            std::vector<IntegerVariable> globalIntegerVariables;
+            
+            // A mapping from global boolean variable names to their indices.
+            std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap;
+            
+            // A mapping from global integer variable names to their indices.
+            std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap;
+            
             // The modules associated with the program.
             std::vector<storm::ir::Module> modules;
             
diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp
index 4daa4c244..40676ab7b 100644
--- a/src/ir/expressions/IntegerConstantExpression.cpp
+++ b/src/ir/expressions/IntegerConstantExpression.cpp
@@ -6,7 +6,7 @@
  */
 
 #include <sstream>
-
+#include <iostream>
 #include "IntegerConstantExpression.h"
 
 namespace storm {
@@ -14,11 +14,13 @@ namespace storm {
         namespace expressions {
             
             IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(int_, constantName), value(0), defined(false) {
+                std::cout << "Creating constant integer expression with constant name " << constantName << "[" << this << "]" << std::endl;
                 // Nothing to do here.
             }
             
             IntegerConstantExpression::IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression)
             : ConstantExpression(integerConstantExpression), value(integerConstantExpression.value), defined(integerConstantExpression.defined) {
+                std::cout << "Creating constant integer expression as copy of " << integerConstantExpression.toString() << "[" << this << "]" << std::endl;
                 // Nothing to do here.
             }
             
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 27aef7480..7790bd7b9 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -18,7 +18,7 @@ namespace models {
  *  @brief  Enumeration of all supported types of models.
  */
 enum ModelType {
-    Unknown, DTMC, CTMC, MDP, UPDATE_LABELED_MDP, CTMDP
+    Unknown, DTMC, CTMC, MDP, CTMDP
 };
 
 /*!
@@ -345,6 +345,14 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		std::vector<T> const& getStateRewardVector() const {
 			return stateRewardVector.get();
 		}
+    
+        /*!
+         * Returns the labels for the choices of the model, if there are any.
+         * @return The labels for the choices of the model.
+         */
+        std::vector<std::list<uint_fast64_t>> const& getChoiceLabeling() const {
+            return choiceLabeling.get();
+        }
 
 		/*!
 		 * Returns the set of labels with which the given state is labeled.
@@ -379,6 +387,14 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		bool hasTransitionRewards() const {
 			return transitionRewardMatrix;
 		}
+    
+        /*!
+         * Retrieves whether this model has a labeling for the choices.
+         * @return True if this model has a labeling.
+         */
+        bool hasChoiceLabels() const {
+            return choiceLabeling;
+        }
 
 		/*!
 		 * Retrieves the size of the internal representation of the model in memory.
diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp
index 8d3ed0fc8..99dbf0efd 100644
--- a/src/parser/prismparser/PrismGrammar.cpp
+++ b/src/parser/prismparser/PrismGrammar.cpp
@@ -50,16 +50,16 @@ void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpress
 }
     
 void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
-	this->state->assignedLocalIntegerVariables_.add(variable, variable);
+	this->state->assignedIntegerVariables_.add(variable, variable);
 	variableToAssignmentMap[variable] = Assignment(variable, value);
 }
     
 void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
-	this->state->assignedLocalBooleanVariables_.add(variable, variable);
+	this->state->assignedBooleanVariables_.add(variable, variable);
 	variableToAssigmentMap[variable] = Assignment(variable, value);
 }
     
-Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string>& renaming) {
+Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string> const& renaming) {
 	this->state->moduleNames_.add(newName, newName);
 	Module* old = this->moduleMap_.find(oldName);
 	if (old == nullptr) {
@@ -78,34 +78,40 @@ Module PrismGrammar::createModule(std::string const& name, std::vector<BooleanVa
 	return res;
 }
 
-void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
+void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
 	uint_fast64_t id = this->state->addIntegerVariable(name);
     uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
 	vars.emplace_back(newLocalIndex, id, name, lower, upper, init);
 	varids[name] = newLocalIndex;
     ++this->state->nextLocalIntegerVariableIndex;
 	this->state->localIntegerVariables_.add(name, name);
+    if (isGlobalVariable) {
+        this->state->globalIntegerVariables_.add(name, name);
+    }
 }
     
-void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
+void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
 	uint_fast64_t id = this->state->addBooleanVariable(name);
     uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
 	vars.emplace_back(newLocalIndex, id, name, init);
 	varids[name] = newLocalIndex;
     ++this->state->nextLocalBooleanVariableIndex;
 	this->state->localBooleanVariables_.add(name, name);
+    if (isGlobalVariable) {
+        this->state->globalBooleanVariables_.add(name, name);
+    }
 }
 
 StateReward createStateReward(std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
 	return StateReward(guard, reward);
 }
-TransitionReward createTransitionReward(std::string label, std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
+TransitionReward createTransitionReward(std::string const& label, std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
 	return TransitionReward(label, guard, reward);
 }
-void createRewardModel(std::string name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
+void createRewardModel(std::string const& name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
 	mapping[name] = RewardModel(name, stateRewards, transitionRewards);
 }
-Update createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment>& bools, std::map<std::string, Assignment> ints) {
+Update createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
 	return Update(likelihood, bools, ints);
 }
 Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> guard, std::vector<Update> const& updates) {
@@ -114,13 +120,17 @@ Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<Ba
 }
 Program createProgram(
 		Program::ModelType modelType,
-		std::map<std::string, std::shared_ptr<BooleanConstantExpression>> undefBoolConst,
-		std::map<std::string, std::shared_ptr<IntegerConstantExpression>> undefIntConst,
-		std::map<std::string, std::shared_ptr<DoubleConstantExpression>> undefDoubleConst,
-		std::vector<Module> modules,
-		std::map<std::string, RewardModel> rewards,
-		std::map<std::string, std::shared_ptr<BaseExpression>> labels) {
-	return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels);
+		std::map<std::string, std::shared_ptr<BooleanConstantExpression>> const& undefBoolConst,
+		std::map<std::string, std::shared_ptr<IntegerConstantExpression>> const& undefIntConst,
+		std::map<std::string, std::shared_ptr<DoubleConstantExpression>> const& undefDoubleConst,
+        GlobalVariableInformation const& globalVariableInformation,
+		std::vector<Module> const& modules,
+		std::map<std::string, RewardModel> const& rewards,
+		std::map<std::string, std::shared_ptr<BaseExpression>> const& labels) {
+	return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst,
+                   globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables,
+                   globalVariableInformation.booleanVariableToIndexMap,
+                   globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels);
 }
 
 PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) {
@@ -144,10 +154,10 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl
 
 	commandName %= this->state->commandNames_;
 	commandName.name("command name");
-	unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_;
-	unassignedLocalBooleanVariableName.name("unassigned local boolean variable");
-	unassignedLocalIntegerVariableName %= this->state->localIntegerVariables_ - this->state->assignedLocalIntegerVariables_;
-	unassignedLocalIntegerVariableName.name("unassigned local integer variable");
+	unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_;
+	unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable");
+	unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_;
+	unassignedLocalIntegerVariableName.name("unassigned local/global integer variable");
 
 	// This block defines all entities that are needed for parsing a single command.
 	assignmentDefinition =
@@ -157,7 +167,7 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl
 	assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
 	assignmentDefinitionList.name("assignment list");
 	updateDefinition = (
-			ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)];
+			ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)];
 	updateDefinition.name("update");
 	updateListDefinition = +updateDefinition % "+";
 	updateListDefinition.name("update list");
@@ -170,17 +180,13 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl
 
 	// This block defines all entities that are needed for parsing variable definitions.
 	booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
-		[
-			phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2)
-		];
+		[phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
 	booleanVariableDefinition.name("boolean variable declaration");
 
 	integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
-		[
-			phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2)
-		];
+        [phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
 	integerVariableDefinition.name("integer variable declaration");
-	variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4));
+	variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false));
 	variableDefinition.name("variable declaration");
 
 	// This block defines all entities that are needed for parsing a module.
@@ -198,6 +204,10 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl
 	moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
 	moduleDefinitionList.name("module list");
 
+    // This block defines all entities that are needed for parsing global variable definitions.
+    globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
+    globalVariableDefinitionList.name("global variable declaration list");
+    
 	// This block defines all entities that are needed for parsing constant definitions.
 	definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
 	definedBooleanConstantDefinition.name("defined boolean constant declaration");
@@ -227,10 +237,10 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl
 	start = (
 			modelTypeDefinition >
 			constantDefinitionList(qi::_a, qi::_b, qi::_c) >
+            globalVariableDefinitionList(qi::_d) >
 			moduleDefinitionList >
-			rewardDefinitionList(qi::_d) >
-			labelDefinitionList(qi::_e)
-		)[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)];
+			rewardDefinitionList(qi::_e) >
+			labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
 	start.name("probabilistic program declaration");
 }
 
diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h
index bb0b9e8f7..d953d67fa 100644
--- a/src/parser/prismparser/PrismGrammar.h
+++ b/src/parser/prismparser/PrismGrammar.h
@@ -31,6 +31,13 @@ namespace prism {
 using namespace storm::ir;
 using namespace storm::ir::expressions;
 
+struct GlobalVariableInformation {
+    std::vector<BooleanVariable> booleanVariables;
+    std::vector<IntegerVariable> integerVariables;
+    std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
+    std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
+};
+    
 /*!
  * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of
  * the input that complies with the PRISM syntax.
@@ -42,6 +49,7 @@ class PrismGrammar : public qi::grammar<
 		std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
 		std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
 		std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
+        GlobalVariableInformation,
 		std::map<std::string, RewardModel>,
 		std::map<std::string, std::shared_ptr<BaseExpression>>
 	>,
@@ -68,7 +76,7 @@ private:
 
 	std::shared_ptr<storm::parser::prism::VariableState> state;
 	struct qi::symbols<char, Module> moduleMap_;
-
+        
 	// The starting point of the grammar.
 	qi::rule<
 			Iterator,
@@ -77,6 +85,7 @@ private:
 				std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
 				std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
 				std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
+                GlobalVariableInformation,
 				std::map<std::string, RewardModel>,
 				std::map<std::string, std::shared_ptr<BaseExpression>>
 			>,
@@ -84,6 +93,9 @@ private:
 	qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
 	qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
 	qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
+        
+    // Rules for global variable definitions
+    qi::rule<Iterator, qi::unused_type(GlobalVariableInformation&), Skipper> globalVariableDefinitionList;
 
 	// Rules for module definition.
 	qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
@@ -91,8 +103,8 @@ private:
 
 	// Rules for variable definitions.
 	qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
-	qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
-	qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
+	qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&, bool), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
+	qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, bool), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
 
 	// Rules for command definitions.
 	qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
@@ -180,7 +192,7 @@ private:
      * @param oldName The name of the module that is to be copied (modulo renaming).
      * @param renaming A mapping from identifiers to their new names.
      */
-	Module renameModule(std::string const& name, std::string const& oldName, std::map<std::string, std::string>& renaming);
+	Module renameModule(std::string const& name, std::string const& oldName, std::map<std::string, std::string> const& renaming);
         
     /*!
      * Creates a new module with the given name, boolean and integer variables and commands.
@@ -203,8 +215,9 @@ private:
      * @param upper The expression that defines the upper bound of the domain.
      * @param init The expression that defines the initial value of the variable.
      * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices.
+     * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not.
      */
-	void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap);
+	void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap, bool isGlobalVariable);
         
     /*!
     * Creates an boolean variable with the given name and initial value and adds it to the
@@ -213,8 +226,9 @@ private:
     * @param name The name of the boolean variable.
     * @param init The expression that defines the initial value of the variable.
     * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices.
+    * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not.
     */
-	void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap);
+	void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap, bool isGlobalVariable);
     
     /*!
      * Creates a command with the given label, guard and updates.
diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h
index 1895eefe0..fe10d86cf 100644
--- a/src/parser/prismparser/VariableState.h
+++ b/src/parser/prismparser/VariableState.h
@@ -119,7 +119,8 @@ public:
 	// A structure representing the identity function over identifier names.
 	struct variableNamesStruct : qi::symbols<char, std::string> { }
             integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
-			localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
+			localBooleanVariables_, localIntegerVariables_, assignedBooleanVariables_, assignedIntegerVariables_,
+            globalBooleanVariables_, globalIntegerVariables_;
 	
 	/*!
 	 * Adds a new boolean variable with the given name.
diff --git a/src/storm.cpp b/src/storm.cpp
index 537c52d5e..eb39452cb 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -332,8 +332,16 @@ int main(const int argc, const char* argv[]) {
 		} else if (s->isSet("symbolic")) {
 			std::string const arg = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
 			storm::adapters::ExplicitModelAdapter adapter(storm::parser::PrismParserFromFile(arg));
-			std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel();
+			std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel("K=2");
 			model->printModelInformationToStream(std::cout);
+            
+            if (model->getType() == storm::models::MDP) {
+                std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
+                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
+                storm::storage::BitVector const& allCoinsEqualStates = labeledMdp->getLabeledStates("agree");
+                storm::storage::BitVector targetStates = finishedStates & allCoinsEqualStates;
+                storm::counterexamples::MinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
+            }
 		}
 
         // Perform clean-up and terminate.