diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index f1ef50396..b06c24b21 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -16,11 +16,8 @@
 #include <boost/functional/hash.hpp>
 #include <boost/container/flat_set.hpp>
 
-#include "src/ir/Program.h"
-#include "src/ir/RewardModel.h"
-#include "src/ir/StateReward.h"
-#include "src/ir/TransitionReward.h"
-#include "src/utility/IRUtility.h"
+#include "src/storage/prism/Program.h"
+#include "src/storage/expressions/SimpleValuation.h"
 #include "src/models/AbstractModel.h"
 #include "src/models/Dtmc.h"
 #include "src/models/Ctmc.h"
@@ -29,20 +26,17 @@
 #include "src/models/AtomicPropositionsLabeling.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/settings/Settings.h"
+#include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/WrongFormatException.h"
 
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-extern log4cplus::Logger logger;
-
-using namespace storm::utility::ir;
-
 namespace storm {
     namespace adapters {
                 
         template<typename ValueType>
         class ExplicitModelAdapter {
         public:
+            typedef storm::expressions::SimpleValuation StateType;
+            
             // A structure holding information about the reachable state space.
             struct StateInformation {
                 StateInformation() : reachableStates(), stateToIndexMap() {
@@ -53,7 +47,7 @@ namespace storm {
                 std::vector<StateType*> reachableStates;
                 
                 // A mapping from states to indices in the list of reachable states.
-                std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
+                std::unordered_map<StateType*, uint_fast64_t, storm::expressions::SimpleValuationPointerHash, storm::expressions::SimpleValuationPointerCompare> stateToIndexMap;
             };
             
             // A structure holding the individual components of a model.
@@ -90,24 +84,24 @@ namespace storm {
              * rewards.
              * @return The explicit model that was given by the probabilistic program.
              */
-            static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
+            static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
                 // Start by defining the undefined constants in the model.
-                defineUndefinedConstants(program, constantDefinitionString);
+                storm::prism::Program definedProgram = program.defineUndefinedConstants(constantDefinitions);
                 
-                ModelComponents modelComponents = buildModelComponents(program, rewardModelName);
+                ModelComponents modelComponents = buildModelComponents(definedProgram, rewardModelName);
                 
                 std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
                 switch (program.getModelType()) {
-                    case storm::ir::Program::DTMC:
+                    case storm::prism::Program::ModelType::DTMC:
                         result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
-                    case storm::ir::Program::CTMC:
+                    case storm::prism::Program::ModelType::CTMC:
                         result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
-                    case storm::ir::Program::MDP:
+                    case storm::prism::Program::ModelType::MDP:
                         result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
-                    case storm::ir::Program::CTMDP:
+                    case storm::prism::Program::ModelType::CTMDP:
                         result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
                         break;
                     default:
@@ -116,26 +110,10 @@ namespace storm {
                         break;
                 }
                 
-                // Undefine the constants so that the program can be used again somewhere else.
-                undefineUndefinedConstants(program);
-                
                 return result;
             }
             
         private:
-            /*!
-             * Transforms a state into a somewhat readable string.
-             *
-             * @param state The state to transform into a string.
-             * @return A string representation of the state.
-             */
-            static std::string toString(StateType const* state) {
-                std::stringstream ss;
-                for (unsigned int i = 0; i < state->first.size(); i++) ss << state->first[i] << "\t";
-                for (unsigned int i = 0; i < state->second.size(); i++) ss << state->second[i] << "\t";
-                return ss.str();
-            }
-            
             /*!
              * Applies an update to the given state and returns the resulting new state object. This methods does not
              * modify the given state but returns a new one.
@@ -145,7 +123,7 @@ namespace storm {
              * @params update The update to apply.
              * @return The resulting state.
              */
-            static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::ir::Update const& update) {
+            static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::prism::Update const& update) {
                 return applyUpdate(variableInformation, state, state, update);
             }
             
@@ -160,7 +138,7 @@ namespace storm {
              * @param update The update to apply.
              * @return The resulting state.
              */
-            static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::ir::Update const& update) {
+            static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::prism::Update const& update) {
                 StateType* newState = new StateType(*state);
                 for (auto variableAssignmentPair : update.getBooleanAssignments()) {
                     setValue(newState, variableInformation.booleanVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState));
@@ -220,12 +198,12 @@ namespace storm {
              * @param action The action label to select.
              * @return A list of lists of active commands or nothing.
              */
-            static boost::optional<std::vector<std::list<storm::ir::Command>>> getActiveCommandsByAction(storm::ir::Program const& program, StateType const* state, std::string const& action) {
-                boost::optional<std::vector<std::list<storm::ir::Command>>> result((std::vector<std::list<storm::ir::Command>>()));
+            static boost::optional<std::vector<std::list<storm::prism::Command>>> getActiveCommandsByAction(storm::prism::Program const& program, StateType const* state, std::string const& action) {
+                boost::optional<std::vector<std::list<storm::prism::Command>>> result((std::vector<std::list<storm::prism::Command>>()));
                 
                 // Iterate over all modules.
                 for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
-                    storm::ir::Module const& module = program.getModule(i);
+                    storm::prism::Module const& module = program.getModule(i);
                     
                     // If the module has no command labeled with the given action, we can skip this module.
                     if (!module.hasAction(action)) {
@@ -237,14 +215,14 @@ namespace storm {
                     // If the module contains the action, but there is no command in the module that is labeled with
                     // this action, we don't have any feasible command combinations.
                     if (commandIndices.empty()) {
-                        return boost::optional<std::vector<std::list<storm::ir::Command>>>();
+                        return boost::optional<std::vector<std::list<storm::prism::Command>>>();
                     }
                     
-                    std::list<storm::ir::Command> commands;
+                    std::list<storm::prism::Command> commands;
                     
                     // Look up commands by their indices and add them if the guard evaluates to true in the given state.
                     for (uint_fast64_t commandIndex : commandIndices) {
-                        storm::ir::Command const& command = module.getCommand(commandIndex);
+                        storm::prism::Command const& command = module.getCommand(commandIndex);
                         if (command.getGuard()->getValueAsBool(state)) {
                             commands.push_back(command);
                         }
@@ -253,7 +231,7 @@ namespace storm {
                     // If there was no enabled command although the module has some command with the required action label,
                     // we must not return anything.
                     if (commands.size() == 0) {
-                        return boost::optional<std::vector<std::list<storm::ir::Command>>>();
+                        return boost::optional<std::vector<std::list<storm::prism::Command>>>();
                     }
                     
                     result.get().push_back(std::move(commands));
@@ -261,18 +239,18 @@ namespace storm {
                 return result;
             }
                         
-            static std::list<Choice<ValueType>> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
+            static std::list<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
                 std::list<Choice<ValueType>> result;
                 
                 StateType const* currentState = stateInformation.reachableStates[stateIndex];
 
                 // Iterate over all modules.
                 for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
-                    storm::ir::Module const& module = program.getModule(i);
+                    storm::prism::Module const& module = program.getModule(i);
                     
                     // Iterate over all commands.
                     for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
-                        storm::ir::Command const& command = module.getCommand(j);
+                        storm::prism::Command const& command = module.getCommand(j);
                         
                         // Only consider unlabeled commands.
                         if (command.getActionName() != "") continue;
@@ -286,7 +264,7 @@ namespace storm {
                         double probabilitySum = 0;
                         // Iterate over all updates of the current command.
                         for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
-                            storm::ir::Update const& update = command.getUpdate(k);
+                            storm::prism::Update const& update = command.getUpdate(k);
                             
                             // Obtain target state index.
                             std::pair<bool, uint_fast64_t> flagTargetStateIndexPair = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update), stateInformation);
@@ -315,17 +293,17 @@ namespace storm {
                 return result;
             }
             
-            static std::list<Choice<ValueType>> getLabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
+            static std::list<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
                 std::list<Choice<ValueType>> result;
                 
                 for (std::string const& action : program.getActions()) {
                     StateType const* currentState = stateInformation.reachableStates[stateIndex];
-                    boost::optional<std::vector<std::list<storm::ir::Command>>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action);
+                    boost::optional<std::vector<std::list<storm::prism::Command>>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action);
                     
                     // Only process this action label, if there is at least one feasible solution.
                     if (optionalActiveCommandLists) {
-                        std::vector<std::list<storm::ir::Command>> const& activeCommandList = optionalActiveCommandLists.get();
-                        std::vector<std::list<storm::ir::Command>::const_iterator> iteratorList(activeCommandList.size());
+                        std::vector<std::list<storm::prism::Command>> const& activeCommandList = optionalActiveCommandLists.get();
+                        std::vector<std::list<storm::prism::Command>::const_iterator> iteratorList(activeCommandList.size());
                         
                         // Initialize the list of iterators.
                         for (size_t i = 0; i < activeCommandList.size(); ++i) {
@@ -342,10 +320,10 @@ namespace storm {
                             // FIXME: This does not check whether a global variable is written multiple times. While the
                             // behaviour for this is undefined anyway, a warning should be issued in that case.
                             for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
-                                storm::ir::Command const& command = *iteratorList[i];
+                                storm::prism::Command const& command = *iteratorList[i];
                                 
                                 for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
-                                    storm::ir::Update const& update = command.getUpdate(j);
+                                    storm::prism::Update const& update = command.getUpdate(j);
                                     
                                     for (auto const& stateProbabilityPair : *currentTargetStates) {
                                         StateType* newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update);
@@ -459,7 +437,7 @@ namespace storm {
              * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
              * and a vector containing the labels associated with each choice.
              */
-            static std::vector<boost::container::flat_set<uint_fast64_t>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector<storm::ir::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder<ValueType>& transitionRewardMatrixBuilder) {
+            static std::vector<boost::container::flat_set<uint_fast64_t>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<storm::prism::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder<ValueType>& transitionRewardMatrixBuilder) {
                 std::vector<boost::container::flat_set<uint_fast64_t>> choiceLabels;
                 
                 // Initialize a queue and insert the initial state.
@@ -616,7 +594,7 @@ namespace storm {
              * is considered.
              * @return A structure containing the components of the resulting model.
              */
-            static ModelComponents buildModelComponents(storm::ir::Program const& program, std::string const& rewardModelName) {
+            static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) {
                 ModelComponents modelComponents;
                 
                 VariableInformation variableInformation = createVariableInformation(program);
@@ -625,11 +603,11 @@ namespace storm {
                 StateInformation stateInformation;
                 
                 // Get the selected reward model or create an empty one if none is selected.
-                storm::ir::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::ir::RewardModel();
+                storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::prism::RewardModel();
                 
                 // Determine whether we have to combine different choices to one or whether this model can have more than
                 // one choice per state.
-                bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC;
+                bool deterministicModel = program.getModelType() == storm::prism::Program::DTMC || program.getModelType() == storm::prism::Program::CTMC;
 
                 // Build the transition and reward matrices.
                 storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
@@ -662,8 +640,8 @@ namespace storm {
              * @param stateInformation Information about the state space of the program.
              * @return The state labeling of the given program.
              */
-            static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::ir::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
-                std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels = program.getLabels();
+            static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
+                std::map<std::string, std::unique_ptr<storm::prism::expressions::BaseExpression>> const& labels = program.getLabels();
                 
                 storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1);
                 
@@ -697,7 +675,7 @@ namespace storm {
              * @param stateInformation Information about the state space.
              * @return A vector containing the state rewards for the state space.
              */
-            static std::vector<ValueType> buildStateRewards(std::vector<storm::ir::StateReward> const& rewards, StateInformation const& stateInformation) {
+            static std::vector<ValueType> buildStateRewards(std::vector<storm::prism::StateReward> const& rewards, StateInformation const& stateInformation) {
                 std::vector<ValueType> result(stateInformation.reachableStates.size());
                 for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
                     result[index] = ValueType(0);
diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index b73ff1590..197db76ab 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -11,7 +11,7 @@
 #include <chrono>
 
 #include "src/models/Mdp.h"
-#include "src/ir/Program.h"
+#include "src/storage/prism/Program.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidStateException.h"
@@ -1000,7 +1000,7 @@ namespace storm {
              * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
              * formula can be either an unbounded until formula or an eventually formula.
              */
-            static void computeCounterexample(storm::ir::Program const& program, storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
+            static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
                 std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
                 // First, we need to check whether the current formula is an Until-Formula.
                 storm::property::prctl::ProbabilisticBoundOperator<double> const* probBoundFormula = dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<double> const*>(formulaPtr);
@@ -1045,9 +1045,8 @@ namespace storm {
                 std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
 
                 std::cout << "Resulting program:" << std::endl;
-                storm::ir::Program restrictedProgram(program);
-                restrictedProgram.restrictCommands(usedLabelSet);
-                std::cout << restrictedProgram.toString() << std::endl;
+                storm::prism::Program restrictedProgram = program.restrictCommands(usedLabelSet);
+                std::cout << restrictedProgram << std::endl;
                 std::cout << std::endl << "-------------------------------------------" << std::endl;
                 
                 // FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set.
diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp
index e2e230b64..7a456cb09 100644
--- a/src/storage/expressions/SimpleValuation.cpp
+++ b/src/storage/expressions/SimpleValuation.cpp
@@ -1,5 +1,7 @@
 #include "src/storage/expressions/SimpleValuation.h"
 
+#include <boost/functional/hash.hpp>
+
 namespace storm {
     namespace expressions {
         SimpleValuation::SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount) : identifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>), booleanValues(booleanVariableCount), integerValues(integerVariableCount), doubleValues(doubleVariableCount) {
@@ -9,6 +11,10 @@ namespace storm {
         SimpleValuation::SimpleValuation(std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap, std::vector<bool> booleanValues, std::vector<int_fast64_t> integerValues, std::vector<double> doubleValues) : identifierToIndexMap(identifierToIndexMap), booleanValues(booleanValues), integerValues(integerValues), doubleValues(doubleValues) {
             // Intentionally left empty.
         }
+        
+        bool SimpleValuation::operator==(SimpleValuation const& other) const {
+            return this->identifierToIndexMap.get() == other.identifierToIndexMap.get() && this->booleanValues == other.booleanValues && this->integerValues == other.integerValues && this->doubleValues == other.doubleValues;
+        }
 
         void SimpleValuation::setIdentifierIndex(std::string const& name, uint_fast64_t index) {
             (*this->identifierToIndexMap)[name] = index;
@@ -58,5 +64,41 @@ namespace storm {
             
             return stream;
         }
+        
+        std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* valuation) const {
+            size_t seed = 0;
+            for (auto const& value : valuation->booleanValues) {
+                boost::hash_combine<bool>(seed, value);
+            }
+            for (auto const& value : valuation->integerValues) {
+                boost::hash_combine<int_fast64_t>(seed, value);
+            }
+            for (auto const& value : valuation->doubleValues) {
+                boost::hash_combine<double>(seed, value);
+            }
+            return seed;
+        }
+        
+        bool SimpleValuationPointerCompare::operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const {
+            return *valuation1 == *valuation2;
+        }
+        
+        bool SimpleValuationPointerLess::operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const {
+            // Compare boolean variables.
+            bool less = valuation1->booleanValues < valuation2->booleanValues;
+            if (less) {
+                return true;
+            }
+            less = valuation1->integerValues < valuation2->integerValues;
+            if (less) {
+                return true;
+            }
+            less = valuation1->doubleValues < valuation2->doubleValues;
+            if (less) {
+                return true;
+            } else {
+                return false;
+            }
+        }
     }
 }
\ No newline at end of file
diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h
index 8f0e9d161..0cb3a00f6 100644
--- a/src/storage/expressions/SimpleValuation.h
+++ b/src/storage/expressions/SimpleValuation.h
@@ -12,6 +12,9 @@ namespace storm {
     namespace expressions {
         class SimpleValuation : public Valuation {
         public:
+            friend class SimpleValuationPointerHash;
+            friend class SimpleValuationPointerLess;
+            
             /*!
              * Creates a simple valuation that can hold the given number of boolean, integer and double variables.
              *
@@ -39,6 +42,11 @@ namespace storm {
             SimpleValuation(SimpleValuation&&) = default;
             SimpleValuation& operator=(SimpleValuation const&) = default;
             SimpleValuation& operator=(SimpleValuation&&) = default;
+
+            /*!
+             * Compares two simple valuations wrt. equality.
+             */
+            bool operator==(SimpleValuation const& other) const;
             
             /*!
              * Sets the index of the identifier with the given name to the given value.
@@ -92,6 +100,35 @@ namespace storm {
             // The value container for all double identifiers.
             std::vector<double> doubleValues;
         };
+        
+        /*!
+         * A helper class that can pe used as the hash functor for data structures that need to hash a simple valuations
+         * given via pointers.
+         */
+        class SimpleValuationPointerHash {
+        public:
+            std::size_t operator()(SimpleValuation* valuation) const;
+        };
+        
+        /*!
+         * A helper class that can be used as the comparison functor wrt. equality for data structures that need to
+         * store pointers to a simple valuations and need to compare the elements wrt. their content (rather than
+         * pointer equality).
+         */
+        class SimpleValuationPointerCompare {
+        public:
+            bool operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const;
+        };
+        
+        /*!
+         * A helper class that can be used as the comparison functor wrt. "<" for data structures that need to
+         * store pointers to a simple valuations and need to compare the elements wrt. their content (rather than
+         * pointer equality).
+         */
+        class SimpleValuationPointerLess {
+        public:
+            bool operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const;
+        };
     }
 }
 
diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp
index d556f6332..f15797e6d 100644
--- a/src/storage/prism/Assignment.cpp
+++ b/src/storage/prism/Assignment.cpp
@@ -14,6 +14,10 @@ namespace storm {
             return this->expression;
         }
         
+        Assignment Assignment::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return Assignment(this->getVariableName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
             stream << "(" << assignment.getVariableName() << "' = " << assignment.getExpression() << ")";
             return stream;
diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h
index 2d4629e31..cf71c8960 100644
--- a/src/storage/prism/Assignment.h
+++ b/src/storage/prism/Assignment.h
@@ -41,6 +41,14 @@ namespace storm {
              */
             storm::expressions::Expression const& getExpression() const;
             
+            /*!
+             * Substitutes all identifiers in the assignment according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting assignment.
+             */
+            Assignment substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
             
         private:
diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp
index c746e698d..478b9322d 100644
--- a/src/storage/prism/BooleanVariable.cpp
+++ b/src/storage/prism/BooleanVariable.cpp
@@ -10,6 +10,10 @@ namespace storm {
             // Nothing to do here.
         }
         
+        BooleanVariable BooleanVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
             stream << variable.getName() << ": bool " << variable.getInitialValueExpression() << ";";
             return stream;
diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h
index d52b8d0aa..6c70fbafb 100644
--- a/src/storage/prism/BooleanVariable.h
+++ b/src/storage/prism/BooleanVariable.h
@@ -35,6 +35,14 @@ namespace storm {
              */
             BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
+            /*!
+             * Substitutes all identifiers in the boolean variable according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting boolean variable.
+             */
+            BooleanVariable substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable);
         };
         
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index 5ca424bb1..f075ff6c6 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -30,6 +30,16 @@ namespace storm {
             return this->globalIndex;
         }
         
+        Command Command::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            std::vector<Update> newUpdates;
+            newUpdates.reserve(this->getNumberOfUpdates());
+            for (auto const& update : this->getUpdates()) {
+                newUpdates.emplace_back(update.substitute(substitution));
+            }
+            
+            return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute<std::map>(substitution), newUpdates, this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Command const& command) {
             stream << "[" << command.getActionName() << "] " << command.getGuardExpression() << " -> ";
             for (uint_fast64_t i = 0; i < command.getUpdates().size(); ++i) {
diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h
index 24510bfda..91831d421 100644
--- a/src/storage/prism/Command.h
+++ b/src/storage/prism/Command.h
@@ -73,6 +73,14 @@ namespace storm {
              */
             uint_fast64_t getGlobalIndex() const;
             
+            /*!
+             * Substitutes all identifiers in the command according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting command.
+             */
+            Command substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Command const& command);
             
         private:
diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index b57bf32d3..83e5f9b2a 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -2,11 +2,11 @@
 
 namespace storm {
     namespace prism {
-        Constant::Constant(ConstantType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(true), expression(expression) {
+        Constant::Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(true), expression(expression) {
             // Intentionally left empty.
         }
         
-        Constant::Constant(ConstantType constantType, std::string const& constantName, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(false), expression() {
+        Constant::Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(false), expression() {
             // Intentionally left empty.
         }
         
@@ -14,7 +14,7 @@ namespace storm {
             return this->constantName;
         }
         
-        Constant::ConstantType Constant::getConstantType() const {
+        storm::expressions::ExpressionReturnType Constant::getConstantType() const {
             return this->constantType;
         }
         
@@ -29,9 +29,10 @@ namespace storm {
         std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
             stream << "const ";
             switch (constant.getConstantType()) {
-                case Constant::ConstantType::Bool: stream << "bool "; break;
-                case Constant::ConstantType::Integer: stream << "int "; break;
-                case Constant::ConstantType::Double: stream << "double "; break;
+                case storm::expressions::ExpressionReturnType::Undefined: stream << "undefined "; break;
+                case storm::expressions::ExpressionReturnType::Bool: stream << "bool "; break;
+                case storm::expressions::ExpressionReturnType::Int: stream << "int "; break;
+                case storm::expressions::ExpressionReturnType::Double: stream << "double "; break;
             }
             stream << constant.getConstantName();
             if (constant.isDefined()) {
diff --git a/src/storage/prism/Constant.h b/src/storage/prism/Constant.h
index ad1736ffd..b67e1639f 100644
--- a/src/storage/prism/Constant.h
+++ b/src/storage/prism/Constant.h
@@ -8,11 +8,6 @@ namespace storm {
     namespace prism {
         class Constant : public LocatedInformation {
         public:
-            /*!
-             * The possible constant types.
-             */
-            enum class ConstantType {Bool, Integer, Double};
-            
             /*!
              * Creates a constant with the given type, name and defining expression.
              *
@@ -22,7 +17,7 @@ namespace storm {
              * @param filename The filename in which the transition reward is defined.
              * @param lineNumber The line number in which the transition reward is defined.
              */
-            Constant(ConstantType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
             /*!
              * Creates an undefined constant with the given type and name.
@@ -32,7 +27,7 @@ namespace storm {
              * @param filename The filename in which the transition reward is defined.
              * @param lineNumber The line number in which the transition reward is defined.
              */
-            Constant(ConstantType constantType, std::string const& constantName, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             // Create default implementations of constructors/assignment.
             Constant() = default;
@@ -53,7 +48,7 @@ namespace storm {
              *
              * @return The type of the constant;
              */
-            ConstantType getConstantType() const;
+            storm::expressions::ExpressionReturnType getConstantType() const;
             
             /*!
              * Retrieves whether the constant is defined, i.e., whether there is an expression defining its value.
@@ -74,7 +69,7 @@ namespace storm {
             
         private:
             // The type of the constant.
-            ConstantType constantType;
+            storm::expressions::ExpressionReturnType constantType;
             
             // The name of the constant.
             std::string constantName;
diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp
index e665f22f7..875438441 100644
--- a/src/storage/prism/Formula.cpp
+++ b/src/storage/prism/Formula.cpp
@@ -18,6 +18,10 @@ namespace storm {
             return this->getExpression().getReturnType();
         }
         
+        Formula Formula::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return Formula(this->getFormulaName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Formula const& formula) {
             stream << "formula " << formula.getFormulaName() << " = " << formula.getExpression() << ";";
             return stream;
diff --git a/src/storage/prism/Formula.h b/src/storage/prism/Formula.h
index 4ae67b9dd..d507aebb1 100644
--- a/src/storage/prism/Formula.h
+++ b/src/storage/prism/Formula.h
@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_PRISM_FORMULA_H_
 #define STORM_STORAGE_PRISM_FORMULA_H_
 
+#include <map>
+
 #include "src/storage/prism/LocatedInformation.h"
 #include "src/storage/expressions/Expression.h"
 
@@ -47,6 +49,14 @@ namespace storm {
              */
             storm::expressions::ExpressionReturnType getReturnType() const;
             
+            /*!
+             * Substitutes all identifiers in the expression of the formula according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting formula.
+             */
+            Formula substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Formula const& formula);
             
         private:
diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp
index 2815d5a6c..2655dd266 100644
--- a/src/storage/prism/IntegerVariable.cpp
+++ b/src/storage/prism/IntegerVariable.cpp
@@ -18,6 +18,10 @@ namespace storm {
             return this->upperBoundExpression;
         }
         
+        IntegerVariable IntegerVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute<std::map>(substitution), this->getUpperBoundExpression().substitute<std::map>(substitution), this->getInitialValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {
             stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << " init " << variable.getInitialValueExpression() << ";";
             return stream;
diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h
index 817752925..f85e58701 100644
--- a/src/storage/prism/IntegerVariable.h
+++ b/src/storage/prism/IntegerVariable.h
@@ -53,6 +53,14 @@ namespace storm {
              */
             storm::expressions::Expression const& getUpperBoundExpression() const;
             
+            /*!
+             * Substitutes all identifiers in the boolean variable according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting boolean variable.
+             */
+            IntegerVariable substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable);
             
         private:
diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp
index 297d8691e..51feae5b4 100644
--- a/src/storage/prism/Label.cpp
+++ b/src/storage/prism/Label.cpp
@@ -14,6 +14,10 @@ namespace storm {
             return this->statePredicateExpression;
         }
         
+        Label Label::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return Label(this->getLabelName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Label const& label) {
             stream << "label \"" << label.getLabelName() << "\" = " << label.getStatePredicateExpression() << ";";
             return stream;
diff --git a/src/storage/prism/Label.h b/src/storage/prism/Label.h
index d1ae6e0fd..18899b41d 100644
--- a/src/storage/prism/Label.h
+++ b/src/storage/prism/Label.h
@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_PRISM_LABEL_H_
 #define STORM_STORAGE_PRISM_LABEL_H_
 
+#include <map>
+
 #include "src/storage/prism/LocatedInformation.h"
 #include "src/storage/expressions/Expression.h"
 
@@ -40,6 +42,14 @@ namespace storm {
              */
             storm::expressions::Expression const& getStatePredicateExpression() const;
             
+            /*!
+             * Substitutes all identifiers in the expression of the label according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting label.
+             */
+            Label substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Label const& label);
             
         private:
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 2c87a2077..f17e1bc12 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -127,6 +127,28 @@ namespace storm {
             return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
         }
         
+        Module Module::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            std::vector<BooleanVariable> newBooleanVariables;
+            newBooleanVariables.reserve(this->getNumberOfBooleanVariables());
+            for (auto const& booleanVariable : this->getBooleanVariables()) {
+                newBooleanVariables.emplace_back(booleanVariable.substitute(substitution));
+            }
+            
+            std::vector<IntegerVariable> newIntegerVariables;
+            newBooleanVariables.reserve(this->getNumberOfIntegerVariables());
+            for (auto const& integerVariable : this->getIntegerVariables()) {
+                newIntegerVariables.emplace_back(integerVariable.substitute(substitution));
+            }
+            
+            std::vector<Command> newCommands;
+            newCommands.reserve(this->getNumberOfCommands());
+            for (auto const& command : this->getCommands()) {
+                newCommands.emplace_back(command.substitute(substitution));
+            }
+            
+            return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Module const& module) {
             stream << "module " << module.getName() << std::endl;
             for (auto const& booleanVariable : module.getBooleanVariables()) {
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index 45ccf4f8a..ba23c23c5 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -146,6 +146,14 @@ namespace storm {
              */
             Module restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const;
             
+            /*!
+             * Substitutes all identifiers in the module according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting module.
+             */
+            Module substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Module const& module);
 
         private:
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 98bb75a1a..564665fc0 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -25,6 +25,10 @@ namespace storm {
         std::vector<Constant> const& Program::getConstants() const {
             return this->constants;
         }
+        
+        std::size_t Program::getNumberOfConstants() const {
+            return this->getConstants().size();
+        }
 
         std::vector<BooleanVariable> const& Program::getGlobalBooleanVariables() const {
             return this->globalBooleanVariables;
@@ -59,7 +63,7 @@ namespace storm {
         }
         
         std::size_t Program::getNumberOfFormulas() const {
-            return this->formulas.size();
+            return this->getFormulas().size();
         }
         
         std::size_t Program::getNumberOfModules() const {
@@ -125,7 +129,7 @@ namespace storm {
         }
         
         std::size_t Program::getNumberOfRewardModels() const {
-            return this->rewardModels.size();
+            return this->getRewardModels().size();
         }
         
         storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
@@ -139,10 +143,10 @@ namespace storm {
         }
         
         std::size_t Program::getNumberOfLabels() const {
-            return this->labels.size();
+            return this->getLabels().size();
         }
         
-        Program Program::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) {
+        Program Program::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const {
             std::vector<storm::prism::Module> newModules;
             newModules.reserve(this->getNumberOfModules());
             
@@ -198,6 +202,89 @@ namespace storm {
 
         }
         
+        Program Program::defineUndefinedConstants(std::map<std::string, storm::expressions::Expression> const& constantDefinitions) const {
+            // For sanity checking, we keep track of all undefined constants that we define in the course of this
+            // procedure.
+            std::set<std::string> definedUndefinedConstants;
+            
+            std::vector<Constant> newConstants;
+            newConstants.reserve(this->getNumberOfConstants());
+            for (auto const& constant : this->getConstants()) {
+                // If the constant is already defined, we need to replace the appearances of undefined constants in its
+                // defining expression
+                if (constant.isDefined()) {
+                    // Make sure we are not trying to define an already defined constant.
+                    LOG_THROW(constantDefinitions.find(constant.getConstantName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getConstantName() << "'.");
+                    
+                    // Now replace the occurrences of undefined constants in its defining expression.
+                    newConstants.emplace_back(constant.getConstantType(), constant.getConstantName(), constant.getExpression().substitute<std::map>(constantDefinitions), constant.getFilename(), constant.getLineNumber());
+                } else {
+                    auto const& variableExpressionPair = constantDefinitions.find(constant.getConstantName());
+                    
+                    // If the constant is not defined by the mapping, we leave it like it is.
+                    if (variableExpressionPair == constantDefinitions.end()) {
+                        newConstants.emplace_back(constant);
+                    } else {
+                        // Otherwise, we add it to the defined constants and assign it the appropriate expression.
+                        definedUndefinedConstants.insert(constant.getConstantName());
+                        
+                        // Make sure the type of the constant is correct.
+                        LOG_THROW(variableExpressionPair->second.getReturnType() == constant.getConstantType(), storm::exceptions::InvalidArgumentException, "Illegal type of expression defining constant '" << constant.getConstantName() << "'.");
+                        
+                        // Now create the defined constant.
+                        newConstants.emplace_back(constant.getConstantType(), constant.getConstantName(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
+                    }
+                }
+            }
+            
+            // As a sanity check, we make sure that the given mapping does not contain any definitions for identifiers
+            // that are not undefined constants.
+            for (auto const& constantExpressionPair : constantDefinitions) {
+                LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
+            }
+            
+            // Now we can substitute the constants in all expressions appearing in the program.
+            std::vector<BooleanVariable> newBooleanVariables;
+            newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
+            for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
+                newBooleanVariables.emplace_back(booleanVariable.substitute(constantDefinitions));
+            }
+            
+            std::vector<IntegerVariable> newIntegerVariables;
+            newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
+            for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
+                newIntegerVariables.emplace_back(integerVariable.substitute(constantDefinitions));
+            }
+        
+            std::vector<Formula> newFormulas;
+            newFormulas.reserve(this->getNumberOfFormulas());
+            for (auto const& formula : this->getFormulas()) {
+                newFormulas.emplace_back(formula.substitute(constantDefinitions));
+            }
+
+            std::vector<Module> newModules;
+            newModules.reserve(this->getNumberOfModules());
+            for (auto const& module : this->getModules()) {
+                newModules.emplace_back(module.substitute(constantDefinitions));
+            }
+            
+            std::vector<RewardModel> newRewardModels;
+            newRewardModels.reserve(this->getNumberOfRewardModels());
+            for (auto const& rewardModel : this->getRewardModels()) {
+                newRewardModels.emplace_back(rewardModel.substitute(constantDefinitions));
+            }
+            
+            storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute<std::map>(constantDefinitions);
+            
+            std::vector<Label> newLabels;
+            newLabels.reserve(this->getNumberOfLabels());
+            for (auto const& label : this->getLabels()) {
+                newLabels.emplace_back(label.substitute(constantDefinitions));
+            }
+            
+            return Program(this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels);
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Program const& program) {
             switch (program.getModelType()) {
                 case Program::ModelType::UNDEFINED: stream << "undefined"; break;
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 93e8ffccd..cd3e62345 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -72,6 +72,13 @@ namespace storm {
              */
             std::vector<Constant> const& getConstants() const;
             
+            /*!
+             * Retrieves the number of all constants defined in the program.
+             *
+             * @return The number of constants defined in the program.
+             */
+            std::size_t getNumberOfConstants() const;
+            
             /*!
              * Retrieves the global boolean variables of the program.
              *
@@ -239,7 +246,17 @@ namespace storm {
              *
              * @param indexSet The set of indices for which to keep the commands.
              */
-            Program restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet);
+            Program restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const;
+            
+            /*!
+             * Defines the undefined constants according to the given map and returns the resulting program.
+             *
+             * @param constantDefinitions A mapping from undefined constant names to the expressions they are supposed
+             * to be replaced with.
+             * @return The program after all undefined constants in the given map have been replaced with their
+             * definitions.
+             */
+            Program defineUndefinedConstants(std::map<std::string, storm::expressions::Expression> const& constantDefinitions) const;
             
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index a25d58fc9..a6c68b34f 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -26,6 +26,21 @@ namespace storm {
             return this->transitionRewards;
         }
         
+        RewardModel RewardModel::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            std::vector<StateReward> newStateRewards;
+            newStateRewards.reserve(this->getStateRewards().size());
+            for (auto const& stateReward : this->getStateRewards()) {
+                newStateRewards.emplace_back(stateReward.substitute(substitution));
+            }
+            
+            std::vector<TransitionReward> newTransitionRewards;
+            newTransitionRewards.reserve(this->getTransitionRewards().size());
+            for (auto const& transitionReward : this->getTransitionRewards()) {
+                newTransitionRewards.emplace_back(transitionReward.substitute(substitution));
+            }
+            return RewardModel(this->getName(), newStateRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
             stream << "rewards \"" << rewardModel.getName() << "\"" << std::endl;
             for (auto const& reward : rewardModel.getStateRewards()) {
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index 9e9498843..be43834e1 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -3,6 +3,7 @@
 
 #include <string>
 #include <vector>
+#include <map>
 
 #include "src/storage/prism/StateReward.h"
 #include "src/storage/prism/TransitionReward.h"
@@ -64,6 +65,14 @@ namespace storm {
              */
             std::vector<storm::prism::TransitionReward> const& getTransitionRewards() const;
             
+            /*!
+             * Substitutes all identifiers in the reward model according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting reward model.
+             */
+            RewardModel substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
 
         private:
diff --git a/src/storage/prism/StateReward.cpp b/src/storage/prism/StateReward.cpp
index 7e36406c5..ab2f0974b 100644
--- a/src/storage/prism/StateReward.cpp
+++ b/src/storage/prism/StateReward.cpp
@@ -14,6 +14,10 @@ namespace storm {
             return this->rewardValueExpression;
         }
         
+        StateReward StateReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return StateReward(this->getStatePredicateExpression().substitute<std::map>(substitution), this->getRewardValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward) {
             stream << "\t" << stateReward.getStatePredicateExpression() << ": " << stateReward.getRewardValueExpression() << ";";
             return stream;
diff --git a/src/storage/prism/StateReward.h b/src/storage/prism/StateReward.h
index 5eb98886f..ea6050855 100644
--- a/src/storage/prism/StateReward.h
+++ b/src/storage/prism/StateReward.h
@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_PRISM_STATEREWARD_H_
 #define STORM_STORAGE_PRISM_STATEREWARD_H_
 
+#include <map>
+
 #include "src/storage/prism/LocatedInformation.h"
 #include "src/storage/expressions/Expression.h"
 
@@ -40,6 +42,14 @@ namespace storm {
              */
             storm::expressions::Expression const& getRewardValueExpression() const;
             
+            /*!
+             * Substitutes all identifiers in the state reward according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting state reward.
+             */
+            StateReward substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward);
 
         private:
diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp
index a5b81e55f..0034231d8 100644
--- a/src/storage/prism/TransitionReward.cpp
+++ b/src/storage/prism/TransitionReward.cpp
@@ -18,6 +18,10 @@ namespace storm {
             return this->rewardValueExpression;
         }
         
+        TransitionReward TransitionReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return TransitionReward(this->getActionName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getRewardValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) {
             stream << "\t[" << transitionReward.getActionName() << "] " << transitionReward.getStatePredicateExpression() << ": " << transitionReward.getRewardValueExpression() << ";";
             return stream;
diff --git a/src/storage/prism/TransitionReward.h b/src/storage/prism/TransitionReward.h
index 1232e5b51..987d7dc89 100644
--- a/src/storage/prism/TransitionReward.h
+++ b/src/storage/prism/TransitionReward.h
@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
 #define STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
 
+#include <map>
+
 #include "src/storage/prism/LocatedInformation.h"
 #include "src/storage/expressions/Expression.h"
 
@@ -49,6 +51,14 @@ namespace storm {
              */
             storm::expressions::Expression const& getRewardValueExpression() const;
             
+            /*!
+             * Substitutes all identifiers in the transition reward according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting transition reward.
+             */
+            TransitionReward substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward);
 
         private:
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
index 21c204b00..2e01187c9 100644
--- a/src/storage/prism/Update.cpp
+++ b/src/storage/prism/Update.cpp
@@ -37,6 +37,16 @@ namespace storm {
             }
         }
         
+        Update Update::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            std::vector<Assignment> newAssignments;
+            newAssignments.reserve(this->getNumberOfAssignments());
+            for (auto const& assignment : this->getAssignments()) {
+                newAssignments.emplace_back(assignment.substitute(substitution));
+            }
+            
+            return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute<std::map>(substitution), newAssignments, this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Update const& update) {
             stream << update.getLikelihoodExpression() << " : ";
             uint_fast64_t i = 0;
diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h
index a6e53ea50..176111acb 100644
--- a/src/storage/prism/Update.h
+++ b/src/storage/prism/Update.h
@@ -63,6 +63,14 @@ namespace storm {
              */
             uint_fast64_t getGlobalIndex() const;
             
+            /*!
+             * Substitutes all identifiers in the update according to the given map.
+             *
+             * @param substitution The substitution to perform.
+             * @return The resulting update.
+             */
+            Update substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);
             
         private: