diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp
index d028bca8d..1d291af02 100644
--- a/src/storm/builder/BuilderOptions.cpp
+++ b/src/storm/builder/BuilderOptions.cpp
@@ -35,7 +35,7 @@ namespace storm {
             return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
-        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), explorationChecks(false) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildChoiceOrigins(false), explorationChecks(false) {
             // Intentionally left empty.
         }
         
@@ -139,6 +139,10 @@ namespace storm {
             return buildChoiceLabels;
         }
         
+        bool BuilderOptions::isBuildChoiceOriginsSet() const {
+            return buildChoiceOrigins;
+        }
+        
         bool BuilderOptions::isBuildAllRewardModelsSet() const {
             return buildAllRewardModels;
         }
@@ -197,6 +201,11 @@ namespace storm {
             buildChoiceLabels = newValue;
             return *this;
         }
+ 
+        BuilderOptions& BuilderOptions::setBuildChoiceOrigins(bool newValue) {
+            buildChoiceOrigins = newValue;
+            return *this;
+        }
 
     }
 }
diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h
index 4be1bbc19..1485c1113 100644
--- a/src/storm/builder/BuilderOptions.h
+++ b/src/storm/builder/BuilderOptions.h
@@ -89,6 +89,7 @@ namespace storm {
             bool hasTerminalStates() const;
             void clearTerminalStates();
             bool isBuildChoiceLabelsSet() const;
+            bool isBuildChoiceOriginsSet() const;
             bool isBuildAllRewardModelsSet() const;
             bool isBuildAllLabelsSet() const;
             bool isExplorationChecksSet() const;
@@ -101,6 +102,7 @@ namespace storm {
             BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value);
             BuilderOptions& addTerminalLabel(std::string const& label, bool value);
             BuilderOptions& setBuildChoiceLabels(bool newValue);
+            BuilderOptions& setBuildChoiceOrigins(bool newValue);
             BuilderOptions& setExplorationChecks(bool newValue);
             
         private:
@@ -125,6 +127,10 @@ namespace storm {
             
             /// A flag indicating whether or not to build choice labels.
             bool buildChoiceLabels;
+                         
+            // A flag that indicates whether or not to generate the information from which parts of the model specification
+            // each choice originates.
+            bool buildChoiceOrigins;
             
             /// A flag that stores whether exploration checks are to be performed.
             bool explorationChecks;
diff --git a/src/storm/builder/ChoiceInformationBuilder.cpp b/src/storm/builder/ChoiceInformationBuilder.cpp
new file mode 100644
index 000000000..b51c68b15
--- /dev/null
+++ b/src/storm/builder/ChoiceInformationBuilder.cpp
@@ -0,0 +1,34 @@
+#include "storm/builder/ChoiceInformationBuilder.h"
+
+namespace storm {
+    namespace builder {
+         
+        void ChoiceInformationBuilder::addLabel(std::string const& label, uint_fast64_t choiceIndex) {
+            storm::storage::BitVector& labeledChoices = labels[label];
+            labeledChoices.grow(choiceIndex + 1);
+            labeledChoices.set(choiceIndex, true);
+        }
+        
+        void ChoiceInformationBuilder::addOriginData(boost::any const& originData, uint_fast64_t choiceIndex) {
+            if(dataOfOrigins.size() != choiceIndex) {
+                dataOfOrigins.resize(choiceIndex);
+            }
+            dataOfOrigins.push_back(originData);
+        }
+        
+        storm::models::sparse::ChoiceLabeling ChoiceInformationBuilder::buildChoiceLabeling(uint_fast64_t totalNumberOfChoices) {
+            storm::models::sparse::ChoiceLabeling result(totalNumberOfChoices);
+            for (auto& label : labels) {
+                label.second.resize(totalNumberOfChoices, false);
+                result.addLabel(label.first, std::move(label.second));
+            }
+            return result;
+        }
+            
+        std::vector<boost::any> ChoiceInformationBuilder::buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices) {
+            dataOfOrigins.resize(totalNumberOfChoices);
+            return std::move(dataOfOrigins);
+        }
+        
+    }
+}
\ No newline at end of file
diff --git a/src/storm/builder/ChoiceInformationBuilder.h b/src/storm/builder/ChoiceInformationBuilder.h
new file mode 100644
index 000000000..ca29e3fe1
--- /dev/null
+++ b/src/storm/builder/ChoiceInformationBuilder.h
@@ -0,0 +1,41 @@
+#pragma once
+
+#include <memory>
+#include <string>
+#include <unordered_map>
+#include <vector>
+#include <boost/any.hpp>
+
+#include "storm/models/sparse/ChoiceLabeling.h"
+#include "storm/storage/BitVector.h"
+#include "storm/storage/sparse/PrismChoiceOrigins.h"
+#include "storm/storage/prism/Program.h"
+
+
+namespace storm {
+    namespace builder {
+        
+        /*!
+         * This class collects information regarding the choices
+         */
+        class ChoiceInformationBuilder {
+        public:
+            
+            ChoiceInformationBuilder() = default;
+
+            void addLabel(std::string const& label, uint_fast64_t choiceIndex);
+            
+            void addOriginData(boost::any const& originData, uint_fast64_t choiceIndex);
+            
+            storm::models::sparse::ChoiceLabeling buildChoiceLabeling(uint_fast64_t totalNumberOfChoices);
+            
+            std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
+            
+            
+        private:
+            std::unordered_map<std::string, storm::storage::BitVector> labels;
+            std::vector<boost::any> dataOfOrigins;
+        };
+    }
+}
+    
\ No newline at end of file
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index b207816bb..02d286dd4 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -14,6 +14,7 @@
 #include "storm/settings/modules/IOSettings.h"
 
 #include "storm/builder/RewardModelBuilder.h"
+#include "storm/builder/ChoiceInformationBuilder.h"
 
 #include "storm/generator/PrismNextStateGenerator.h"
 #include "storm/generator/JaniNextStateGenerator.h"
@@ -66,36 +67,30 @@ namespace storm {
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        storm::storage::sparse::StateValuations const& ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getStateValuations() const {
-            STORM_LOG_THROW(static_cast<bool>(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
-            return stateValuations.get();
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitModelBuilder<ValueType, RewardModelType, StateType>::build() {
+        ExplicitModelBuilderResult<ValueType, RewardModelType> ExplicitModelBuilder<ValueType, RewardModelType, StateType>::build() {
             STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder);
             ModelComponents modelComponents = buildModelComponents();
             
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> result;
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> resultModel;
             switch (generator->getModelType()) {
                 case storm::generator::ModelType::DTMC:
-                    result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Dtmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Dtmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
                     break;
                 case storm::generator::ModelType::CTMC:
-                    result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Ctmc<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
                     break;
                 case storm::generator::ModelType::MDP:
-                    result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Mdp<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::Mdp<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
                     break;
                 case storm::generator::ModelType::MA:
-                    result = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), *std::move(modelComponents.markovianStates), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling)));
+                    resultModel = std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(new storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), *std::move(modelComponents.markovianStates), std::move(modelComponents.rewardModels)    )); //, std::move(modelComponents.choiceLabeling)));
                     break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type.");
                     break;
             }
             
-            return result;
+            return ExplicitModelBuilderResult<ValueType, RewardModelType>(resultModel, modelComponents.stateValuations, modelComponents.choiceOrigins);
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
@@ -122,11 +117,7 @@ namespace storm {
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>& choiceLabels, boost::optional<storm::storage::BitVector>& markovianStates) {
-            // Create choice labels, if requested,
-            if (generator->getOptions().isBuildChoiceLabelsSet()) {
-                choiceLabels = std::vector<boost::container::flat_set<uint_fast64_t>>();
-            }
+        void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates) {
             
             // Create markovian states bit vector, if required.
             if (generator->getModelType() == storm::generator::ModelType::MA) {
@@ -177,11 +168,6 @@ namespace storm {
                             this->stateStorage.deadlockStateIndices.push_back(currentIndex);
                         }
                         
-                        if (generator->getOptions().isBuildChoiceLabelsSet()) {
-                            // Insert empty choice labeling for added self-loop transitions.
-                            choiceLabels.get().push_back(boost::container::flat_set<uint_fast64_t>());
-                        }
-                        
                         if (markovianStates) {
                             markovianStates.get().grow(currentRowGroup + 1, false);
                             markovianStates.get().set(currentRowGroup);
@@ -225,9 +211,15 @@ namespace storm {
                     
                     // Now add all choices.
                     for (auto const& choice : behavior) {
-                        // Add command labels if requested.
-                        if (generator->getOptions().isBuildChoiceLabelsSet()) {
-                            choiceLabels.get().push_back(choice.getLabels());
+                        
+                        // add the generated choice information
+                        if (choice.hasLabels()) {
+                            for (auto const& label : choice.getLabels()) {
+                                choiceInformationBuilder.addLabel(label, currentRow);
+                            }
+                        }
+                        if (choice.hasOriginData()) {
+                            choiceInformationBuilder.addOriginData(choice.getOriginData(), currentRow);
                         }
                         
                         // If we keep track of the Markovian choices, store whether the current one is Markovian.
@@ -300,8 +292,8 @@ namespace storm {
                 rewardModelBuilders.emplace_back(generator->getRewardModelInformation(i));
             }
             
-            boost::optional<storm::storage::BitVector> markovianChoices;
-            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, modelComponents.choiceLabeling, modelComponents.markovianStates);
+            ChoiceInformationBuilder choiceInformationBuilder;
+            buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, modelComponents.markovianStates);
             modelComponents.transitionMatrix = transitionMatrixBuilder.build();
 
             // Now finalize all reward models.
@@ -312,13 +304,18 @@ namespace storm {
             // Build the state labeling.
             modelComponents.stateLabeling = buildStateLabeling();
             
-            // Finally -- if requested -- build the state information that can be retrieved from the outside.
+            // Build the choice labeling
+            modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
+            
+            // if requested, build the state valuations and choice origins
             if (options.buildStateValuations) {
-                stateValuations = storm::storage::sparse::StateValuations(stateStorage.getNumberOfStates());
+                modelComponents.stateValuations = std::make_shared<storm::storage::sparse::StateValuations>(stateStorage.getNumberOfStates());
                 for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
-                    stateValuations.get().valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first);
+                    modelComponents.stateValuations->valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first);
                 }
             }
+            auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());
+            modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData);
             
             return modelComponents;
         }
diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h
index 25acb684c..d1cea0e7e 100644
--- a/src/storm/builder/ExplicitModelBuilder.h
+++ b/src/storm/builder/ExplicitModelBuilder.h
@@ -19,14 +19,16 @@
 #include "storm/models/sparse/StateAnnotation.h"
 #include "storm/models/sparse/Model.h"
 #include "storm/models/sparse/StateLabeling.h"
+#include "storm/models/sparse/ChoiceLabeling.h"
 #include "storm/storage/SparseMatrix.h"
-#include "storm/storage/sparse/StateValuations.h"
+#include "storm/storage/sparse/ChoiceOrigins.h"
 #include "storm/storage/sparse/StateStorage.h"
 #include "storm/settings/SettingsManager.h"
 
 #include "storm/utility/prism.h"
 
 #include "storm/builder/ExplorationOrder.h"
+#include "storm/builder/ExplicitModelBuilderResult.h"
 
 #include "storm/generator/NextStateGenerator.h"
 #include "storm/generator/CompressedState.h"
@@ -44,6 +46,7 @@ namespace storm {
         
         // Forward-declare classes.
         template <typename ValueType> struct RewardModelBuilder;
+        class ChoiceInformationBuilder;
         
         template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
         class ExplicitModelBuilder {
@@ -62,10 +65,17 @@ namespace storm {
                 std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<typename RewardModelType::ValueType>> rewardModels;
                 
                 // A vector that stores a labeling for each choice.
-                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
+                storm::models::sparse::ChoiceLabeling choiceLabeling;
                 
                 // A vector that stores which states are markovian.
                 boost::optional<storm::storage::BitVector> markovianStates;
+                
+                // Stores for each state to which variable valuation it belongs (is nullptr if not generated)
+                std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations;
+                
+                // Stores for each choice from which parts of the input model description it originates (is nullptr if not generated)
+                std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins;
+
             };
             
             struct Options {
@@ -78,8 +88,7 @@ namespace storm {
                 ExplorationOrder explorationOrder;
                 
                 // A flag that indicates whether or not to store the state information after successfully building the
-                // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful
-                // call to <code>translateProgram</code>.
+                // model. If it is to be preserved, it is contained in the result obtained from <code> build </code>
                 bool buildStateValuations;
             };
             
@@ -108,21 +117,10 @@ 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 program The program to translate.
-             * @param constantDefinitionString A string that contains a comma-separated definition of all undefined
-             * constants in the model.
-             * @param rewardModel The reward model that is to be built.
-             * @return The explicit model that was given by the probabilistic program.
-             */
-            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
-            
-            /*!
-             * If requested in the options, information about the variable valuations in the reachable states can be
-             * retrieved via this function.
-             *
-             * @return A structure that stores information about all reachable states.
+             * @return The explicit model that was given by the probabilistic program as well as additional
+             *         information (if requested).
              */
-            storm::storage::sparse::StateValuations const& getStateValuations() const;
+            ExplicitModelBuilderResult<ValueType, RewardModelType> build();
             
         private:
             /*!
@@ -141,10 +139,10 @@ namespace storm {
              *
              * @param transitionMatrixBuilder The builder of the transition matrix.
              * @param rewardModelBuilders The builders for the selected reward models.
-             * @param choiceLabels is set to a vector containing the labels associated with each choice (is only set if choice labels are requested).
+             * @param choiceInformationBuilder The builder for the requested information of the choices
              * @param markovianChoices is set to a bit vector storing whether a choice is markovian (is only set if the model type requires this information).
              */
-            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>& choiceLabels , boost::optional<storm::storage::BitVector>& markovianChoices);
+            void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices);
             
             /*!
              * Explores the state space of the given program and returns the components of the model as a result.
@@ -169,10 +167,6 @@ namespace storm {
             /// Internal information about the states that were explored.
             storm::storage::sparse::StateStorage<StateType> stateStorage;
             
-            /// This member holds information about reachable states that can be retrieved from the outside after a
-            /// successful build.
-            boost::optional<storm::storage::sparse::StateValuations> stateValuations;
-            
             /// A set of states that still need to be explored.
             std::deque<CompressedState> statesToExplore;
             
diff --git a/src/storm/builder/ExplicitModelBuilderResult.cpp b/src/storm/builder/ExplicitModelBuilderResult.cpp
new file mode 100644
index 000000000..b2d52522e
--- /dev/null
+++ b/src/storm/builder/ExplicitModelBuilderResult.cpp
@@ -0,0 +1,73 @@
+#include "storm/builder/ExplicitModelBuilderResult.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidOperationException.h"
+
+#include "storm/adapters/CarlAdapter.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+
+namespace storm {
+    namespace builder {
+        
+        template <typename ValueType, typename RewardModelType>
+        ExplicitModelBuilderResult<ValueType, RewardModelType>::ExplicitModelBuilderResult(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model, std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations,std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins) : model(model), stateValuations(stateValuations), choiceOrigins(choiceOrigins) {
+            // Intentionally left empty
+        }
+            
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>& ExplicitModelBuilderResult<ValueType, RewardModelType>::getModel() {
+            STORM_LOG_THROW(model, storm::exceptions::InvalidOperationException, "Retrieving the model failed since it is not set.");
+            return model;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> const& ExplicitModelBuilderResult<ValueType, RewardModelType>::getModel() const {
+            STORM_LOG_THROW(model, storm::exceptions::InvalidOperationException, "Retrieving the model failed since it is not set.");
+            return model;
+        }
+            
+        template <typename ValueType, typename RewardModelType>
+        bool ExplicitModelBuilderResult<ValueType, RewardModelType>::hasStateValuations() {
+            return static_cast<bool>(stateValuations);
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::storage::sparse::StateValuations>& ExplicitModelBuilderResult<ValueType, RewardModelType>::getStateValuations() {
+            STORM_LOG_THROW(stateValuations, storm::exceptions::InvalidOperationException, "Retrieving the state valuations failed since they are not set.");
+            return stateValuations;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::storage::sparse::StateValuations> const& ExplicitModelBuilderResult<ValueType, RewardModelType>::getStateValuations() const {
+            STORM_LOG_THROW(stateValuations, storm::exceptions::InvalidOperationException, "Retrieving the state valuations failed since they are not set.");
+            return stateValuations;
+        }
+            
+        template <typename ValueType, typename RewardModelType>
+        bool ExplicitModelBuilderResult<ValueType, RewardModelType>::hasChoiceOrigins() {
+            return static_cast<bool>(choiceOrigins);
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::storage::sparse::ChoiceOrigins>& ExplicitModelBuilderResult<ValueType, RewardModelType>::getChoiceOrigins() {
+            STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidOperationException, "Retrieving the choice origins failed since they are not set.");
+            return choiceOrigins;
+        }
+        
+        template <typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::storage::sparse::ChoiceOrigins> const& ExplicitModelBuilderResult<ValueType, RewardModelType>::getChoiceOrigins() const {
+            STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidOperationException, "Retrieving the choice origins failed since they are not set.");
+            return choiceOrigins;
+        }
+            
+        // Explicitly instantiate the class.
+        template class ExplicitModelBuilderResult<double, storm::models::sparse::StandardRewardModel<double>>;
+
+#ifdef STORM_HAVE_CARL
+        template class ExplicitModelBuilderResult<RationalNumber, storm::models::sparse::StandardRewardModel<RationalNumber>>;
+        template class ExplicitModelBuilderResult<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>>;
+        template class ExplicitModelBuilderResult<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+#endif
+        
+    }
+}
\ No newline at end of file
diff --git a/src/storm/builder/ExplicitModelBuilderResult.h b/src/storm/builder/ExplicitModelBuilderResult.h
new file mode 100644
index 000000000..76a8e1161
--- /dev/null
+++ b/src/storm/builder/ExplicitModelBuilderResult.h
@@ -0,0 +1,33 @@
+#pragma once
+
+#include <memory>
+#include "storm/models/sparse/Model.h"
+#include "storm/storage/sparse/StateValuations.h"
+#include "storm/storage/sparse/ChoiceOrigins.h"
+
+namespace storm {
+    namespace builder {
+        
+        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+        class ExplicitModelBuilderResult {
+        public:
+            ExplicitModelBuilderResult(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model, std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations,std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins);
+            
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>& getModel();
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> const& getModel() const;
+            
+            bool hasStateValuations();
+            std::shared_ptr<storm::storage::sparse::StateValuations>& getStateValuations();
+            std::shared_ptr<storm::storage::sparse::StateValuations> const& getStateValuations() const;
+            
+            bool hasChoiceOrigins();
+            std::shared_ptr<storm::storage::sparse::ChoiceOrigins>& getChoiceOrigins();
+            std::shared_ptr<storm::storage::sparse::ChoiceOrigins> const& getChoiceOrigins() const;
+            
+        private:
+            std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model;
+            std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations;
+            std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins;
+        };
+    }
+}
\ No newline at end of file
diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp
index cddf12f0f..020198fc6 100644
--- a/src/storm/generator/Choice.cpp
+++ b/src/storm/generator/Choice.cpp
@@ -1,11 +1,15 @@
 #include "storm/generator/Choice.h"
 
+#include <boost/container/flat_set.hpp>
+
 #include "storm/adapters/CarlAdapter.h"
 
 #include "storm/utility/constants.h"
+#include "storm/builder/ChoiceInformationBuilder.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace generator {
@@ -33,17 +37,12 @@ namespace storm {
                 rewardValue += *otherRewIt;
             }
             
-            // Join label sets.
-            if (this->labels) {
-                if (other.labels) {
-                    LabelSet newLabelSet;
-                    std::set_union(this->labels.get().begin(), this->labels.get().end(), other.labels.get().begin(), other.labels.get().end(), std::inserter(newLabelSet, newLabelSet.begin()));
-                    this->labels = std::move(newLabelSet);
-                }
-            } else {
-                if (other.labels) {
-                    this->labels = std::move(other.labels);
-                }
+            // Join label sets and origin data if given.
+            if (other.labels) {
+                this->addLabels(other.labels.get());
+            }
+            if (other.originData) {
+                this->addOriginData(other.originData.get());
             }
         }
         
@@ -68,24 +67,60 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        void Choice<ValueType, StateType>::addLabel(uint_fast64_t label) {
+        void Choice<ValueType, StateType>::addLabel(std::string const& newLabel) {
             if (!labels) {
-                labels = LabelSet();
+                labels = std::set<std::string>();
             }
-            labels->insert(label);
+            labels->insert(newLabel);
         }
         
         template<typename ValueType, typename StateType>
-        void Choice<ValueType, StateType>::addLabels(LabelSet const& labelSet) {
-            if (!labels) {
-                labels = LabelSet();
+        void Choice<ValueType, StateType>::addLabels(std::set<std::string> const& newLabels) {
+            if (labels) {
+                labels->insert(newLabels.begin(), newLabels.end());
+            } else {
+                labels = newLabels;
             }
-            labels->insert(labelSet.begin(), labelSet.end());
         }
-        
+            
+        template<typename ValueType, typename StateType>
+        bool Choice<ValueType, StateType>::hasLabels() const {
+            return labels.is_initialized();
+        }
+            
+        template<typename ValueType, typename StateType>
+        std::set<std::string> const& Choice<ValueType, StateType>::getLabels() const {
+            return labels.get();
+        }
+            
+        template<typename ValueType, typename StateType>
+        void Choice<ValueType, StateType>::addOriginData(boost::any const& data) {
+            if (!this->originData || this->originData->empty()) {
+                this->originData = data;
+            } else {
+                if (!data.empty()) {
+                    // Reaching this point means that the both the existing and the given data are non-empty
+                
+                    auto existingDataAsIndexSet = boost::any_cast<boost::container::flat_set<uint_fast64_t>>(&this->originData.get());
+                    if (existingDataAsIndexSet != nullptr) {
+                        auto givenDataAsIndexSet = boost::any_cast<boost::container::flat_set<uint_fast64_t>>(&data);
+                        STORM_LOG_THROW(givenDataAsIndexSet != nullptr, storm::exceptions::InvalidOperationException, "Types of existing and given choice origin data do not match.");
+                        existingDataAsIndexSet->insert(givenDataAsIndexSet->begin(), givenDataAsIndexSet->end());
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Type of choice origin data (aka " << data.type().name() << ") is not implemented.");
+                    }
+                }
+            }
+        }
+            
+        template<typename ValueType, typename StateType>
+        bool Choice<ValueType, StateType>::hasOriginData() const {
+            return originData.is_initialized();
+        }
+            
         template<typename ValueType, typename StateType>
-        boost::container::flat_set<uint_fast64_t> const& Choice<ValueType, StateType>::getLabels() const {
-            return *labels;
+        boost::any const& Choice<ValueType, StateType>::getOriginData() const {
+            return originData.get();
         }
         
         template<typename ValueType, typename StateType>
diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h
index d6abe51ed..04e0fd311 100644
--- a/src/storm/generator/Choice.h
+++ b/src/storm/generator/Choice.h
@@ -3,9 +3,10 @@
 
 #include <cstdint>
 #include <functional>
+#include <set>
 
 #include <boost/optional.hpp>
-#include <boost/container/flat_set.hpp>
+#include <boost/any.hpp>
 
 #include "storm/storage/Distribution.h"
 
@@ -16,8 +17,6 @@ namespace storm {
         template<typename ValueType, typename StateType=uint32_t>
         struct Choice {
         public:
-            typedef boost::container::flat_set<uint_fast64_t> LabelSet;
-            
             Choice(uint_fast64_t actionIndex = 0, bool markovian = false);
             
             Choice(Choice const& other) = default;
@@ -71,21 +70,41 @@ namespace storm {
              *
              * @param label The label to associate with this choice.
              */
-            void addLabel(uint_fast64_t label);
+            void addLabel(std::string const& label);
             
             /*!
              * Adds the given label set to the labels associated with this choice.
              *
              * @param labelSet The label set to associate with this choice.
              */
-            void addLabels(LabelSet const& labelSet);
+            void addLabels(std::set<std::string> const& labels);
+            
+            /*!
+             * Returns whether there are labels defined for this choice
+             */
+            bool hasLabels() const;
             
             /*!
              * Retrieves the set of labels associated with this choice.
              *
              * @return The set of labels associated with this choice.
              */
-            LabelSet const& getLabels() const;
+            std::set<std::string> const& getLabels() const;
+            
+            /*!
+             * Adds the given data that specifies the origin of this choice w.r.t. the model specification
+             */
+            void addOriginData(boost::any const& data);
+            
+            /*!
+             * Returns whether there is origin data defined for this choice
+             */
+            bool hasOriginData() const;
+            
+            /*!
+             * Returns the origin data associated with this choice.
+             */
+            boost::any const& getOriginData() const;
             
             /*!
              * Retrieves the index of the action of this choice.
@@ -147,8 +166,11 @@ namespace storm {
             // The reward values associated with this choice.
             std::vector<ValueType> rewards;
             
-            // The labels that are associated with this choice.
-            boost::optional<LabelSet> labels;
+            // The data that stores what part of the model specification induced this choice
+            boost::optional<boost::any> originData;
+            
+            // The labels of this choice
+            boost::optional<std::set<std::string>> labels;
         };
 
         template<typename ValueType, typename StateType>
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 9ff5974c3..b7e8cd315 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -342,10 +342,6 @@ namespace storm {
                     if (hasStateActionRewards && !this->isDiscreteTimeModel()) {
                         totalExitRate += choice.getTotalMass();
                     }
-                    
-                    if (this->options.isBuildChoiceLabelsSet()) {
-                        globalChoice.addLabels(choice.getLabels());
-                    }
                 }
                 
                 std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
index 7f931051f..2b4b64a88 100644
--- a/src/storm/generator/NextStateGenerator.cpp
+++ b/src/storm/generator/NextStateGenerator.cpp
@@ -147,6 +147,12 @@ namespace storm {
         storm::expressions::SimpleValuation NextStateGenerator<ValueType, StateType>::toValuation(CompressedState const& state) const {
             return unpackStateIntoValuation(state, variableInformation, *expressionManager);
         }
+        
+        template<typename ValueType, typename StateType>
+        std::shared_ptr<storm::storage::sparse::ChoiceOrigins> NextStateGenerator<ValueType, StateType>::generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const {
+            STORM_LOG_ERROR_COND(!options.isBuildChoiceOriginsSet(), "Generating choice origins is not supported for the considered model format.");
+            return nullptr;
+        }
 
         template class NextStateGenerator<double>;
 
diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h
index ea442d278..f894d84a3 100644
--- a/src/storm/generator/NextStateGenerator.h
+++ b/src/storm/generator/NextStateGenerator.h
@@ -9,6 +9,7 @@
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/BitVectorHashMap.h"
 #include "storm/storage/expressions/ExpressionEvaluator.h"
+#include "storm/storage/sparse/ChoiceOrigins.h"
 
 #include "storm/builder/BuilderOptions.h"
 #include "storm/builder/RewardModelInformation.h"
@@ -62,6 +63,8 @@ namespace storm {
             
             NextStateGeneratorOptions const& getOptions() const;
             
+            virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const;
+            
         protected:
             /*!
              * Creates the state labeling for the given states using the provided labels and expressions.
diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
index 62eeae361..015d64509 100644
--- a/src/storm/generator/PrismNextStateGenerator.cpp
+++ b/src/storm/generator/PrismNextStateGenerator.cpp
@@ -1,10 +1,12 @@
 #include "storm/generator/PrismNextStateGenerator.h"
 
 #include <boost/container/flat_map.hpp>
+#include <boost/any.hpp>
 
 #include "storm/models/sparse/StateLabeling.h"
 
 #include "storm/storage/expressions/SimpleValuation.h"
+#include "storm/storage/sparse/PrismChoiceOrigins.h"
 
 #include "storm/solver/SmtSolver.h"
 
@@ -244,9 +246,13 @@ namespace storm {
                         totalExitRate += choice.getTotalMass();
                     }
                     
-                    if (this->options.isBuildChoiceLabelsSet()) {
+                    if (this->options.isBuildChoiceLabelsSet() && choice.hasLabels()) {
                         globalChoice.addLabels(choice.getLabels());
                     }
+                    
+                    if (this->options.isBuildChoiceOriginsSet() && choice.hasOriginData()) {
+                        globalChoice.addOriginData(choice.getOriginData());
+                    }
                 }
                 
                 // Now construct the state-action reward for all selected reward models.
@@ -391,9 +397,10 @@ namespace storm {
                     result.push_back(Choice<ValueType>(command.getActionIndex(), command.isMarkovian()));
                     Choice<ValueType>& choice = result.back();
                     
-                    // Remember the command labels only if we were asked to.
-                    if (this->options.isBuildChoiceLabelsSet()) {
-                        choice.addLabel(command.getGlobalIndex());
+                    // Remember the choice origin only if we were asked to.
+                    if (this->options.isBuildChoiceOriginsSet()) {
+                        CommandSet commandIndex { command.getGlobalIndex() };
+                        choice.addOriginData(boost::any(std::move(commandIndex)));
                     }
                     
                     // Iterate over all updates of the current command.
@@ -503,12 +510,16 @@ namespace storm {
                         // Now create the actual distribution.
                         Choice<ValueType>& choice = result.back();
                         
-                        // Remember the command labels only if we were asked to.
+                        // Remember the choice label and origins only if we were asked to.
                         if (this->options.isBuildChoiceLabelsSet()) {
-                            // Add the labels of all commands to this choice.
+                            choice.addLabel(program.getActionName(actionIndex));
+                        }
+                        if (this->options.isBuildChoiceOriginsSet()) {
+                            CommandSet commandIndices;
                             for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
-                                choice.addLabel(iteratorList[i]->get().getGlobalIndex());
+                                commandIndices.insert(iteratorList[i]->get().getGlobalIndex());
                             }
+                            choice.addOriginData(boost::any(std::move(commandIndices)));
                         }
                         
                         // Add the probabilities/rates to the newly created choice.
@@ -594,6 +605,41 @@ namespace storm {
             storm::prism::RewardModel const& rewardModel = rewardModels[index].get();
             return storm::builder::RewardModelInformation(rewardModel.getName(), rewardModel.hasStateRewards(), rewardModel.hasStateActionRewards(), rewardModel.hasTransitionRewards());
         }
+        
+        template<typename ValueType, typename StateType>
+        std::shared_ptr<storm::storage::sparse::ChoiceOrigins> PrismNextStateGenerator<ValueType, StateType>::generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const {
+            
+            if (!this->getOptions().isBuildChoiceOriginsSet()) {
+                return nullptr;
+            }
+            
+            std::vector<uint_fast64_t> identifiers;
+            identifiers.reserve(dataForChoiceOrigins.size());
+            
+            std::map<CommandSet, uint_fast64_t> commandSetToIdentifierMap;
+            uint_fast64_t currentIdentifier = 0;
+            for (boost::any& originData : dataForChoiceOrigins) {
+                STORM_LOG_ASSERT(originData.empty() || boost::any_cast<CommandSet>(&originData) != nullptr, "Origin data has unexpected type: " << originData.type().name() << ".");
+                
+                CommandSet currentCommandSet = originData.empty() ? CommandSet() : boost::any_cast<CommandSet>(std::move(originData));
+                auto insertionRes = commandSetToIdentifierMap.insert(std::make_pair(std::move(currentCommandSet), currentIdentifier));
+                identifiers.push_back(insertionRes.first->second);
+                if (insertionRes.second) {
+                    ++currentIdentifier;
+                }
+            }
+            
+            std::vector<CommandSet> identifierToCommandSetMapping(currentIdentifier);
+            std::vector<std::string> identifierToInfoMapping(currentIdentifier);
+            for (auto const& setIdPair : commandSetToIdentifierMap) {
+                identifierToCommandSetMapping[setIdPair.second] = setIdPair.first;
+                // Todo: Make these identifiers unique
+                identifierToInfoMapping[setIdPair.second] = "Choice made from " + std::to_string(setIdPair.first.size()) + " commands";
+            }
+            
+            return std::make_shared<storm::storage::sparse::PrismChoiceOrigins>(std::make_shared<storm::prism::Program>(program), std::move(identifiers), std::move(identifierToInfoMapping), std::move(identifierToCommandSetMapping));
+        }
+
                 
         template class PrismNextStateGenerator<double>;
 
diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h
index ee12130e1..0097e7055 100644
--- a/src/storm/generator/PrismNextStateGenerator.h
+++ b/src/storm/generator/PrismNextStateGenerator.h
@@ -1,6 +1,8 @@
 #ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
 #define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_
 
+#include <boost/container/flat_set.hpp>
+
 #include "storm/generator/NextStateGenerator.h"
 
 #include "storm/storage/prism/Program.h"
@@ -12,9 +14,10 @@ namespace storm {
         class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
         public:
             typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
+            typedef boost::container::flat_set<uint_fast64_t> CommandSet;
             
             PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
-            
+
             virtual ModelType getModelType() const override;
             virtual bool isDeterministicModel() const override;
             virtual bool isDiscreteTimeModel() const override;
@@ -27,6 +30,8 @@ namespace storm {
             
             virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
 
+            virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
+
         private:
             void checkValid() const;
 
diff --git a/src/storm/models/sparse/ChoiceLabeling.cpp b/src/storm/models/sparse/ChoiceLabeling.cpp
index 96c6aeec0..fe1117027 100644
--- a/src/storm/models/sparse/ChoiceLabeling.cpp
+++ b/src/storm/models/sparse/ChoiceLabeling.cpp
@@ -54,7 +54,7 @@ namespace storm {
 
 
             void ChoiceLabeling::addLabelToChoice(std::string const& label,uint64_t choice) {
-                this->addLabelToChoice(label, choice);
+                return ItemLabeling::addLabelToItem(label, choice);
             }
 
             bool ChoiceLabeling::getChoiceHasLabel(std::string const& label, uint64_t choice) const {
diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp
new file mode 100644
index 000000000..d9a045482
--- /dev/null
+++ b/src/storm/storage/sparse/ChoiceOrigins.cpp
@@ -0,0 +1,69 @@
+#include "storm/storage/sparse/ChoiceOrigins.h"
+
+#include "storm/storage/sparse/PrismChoiceOrigins.h"
+#include "storm/storage/sparse/JaniChoiceOrigins.h"
+#include "storm/utility/vector.h"
+
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            ChoiceOrigins::ChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping) : indexToIdentifier(indexToIdentifierMapping), identifierToInfo(identifierToInfoMapping) {
+                // Intentionally left empty
+            }
+            
+            ChoiceOrigins::ChoiceOrigins(std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping) : indexToIdentifier(std::move(indexToIdentifierMapping)), identifierToInfo(std::move(identifierToInfoMapping)) {
+                // Intentionally left empty
+            }
+            
+            bool ChoiceOrigins::isPrismChoiceOrigins() const {
+                return false;
+            }
+            
+            bool ChoiceOrigins::isJaniChoiceOrigins() const {
+                return false;
+            }
+                
+            PrismChoiceOrigins& ChoiceOrigins::asPrismChoiceOrigins() {
+                return dynamic_cast<PrismChoiceOrigins&>(*this);
+            }
+            
+            PrismChoiceOrigins const& ChoiceOrigins::asPrismChoiceOrigins() const {
+                return dynamic_cast<PrismChoiceOrigins const&>(*this);
+            }
+                
+            JaniChoiceOrigins& ChoiceOrigins::asJaniChoiceOrigins() {
+                return dynamic_cast<JaniChoiceOrigins&>(*this);
+            }
+            
+            JaniChoiceOrigins const& ChoiceOrigins::asJaniChoiceOrigins() const {
+                return dynamic_cast<JaniChoiceOrigins const&>(*this);
+            }
+            			    
+            uint_fast64_t ChoiceOrigins::getIdentifier(uint_fast64_t choiceIndex) const {
+            	return  indexToIdentifier[choiceIndex];
+            }
+            
+			std::string const& ChoiceOrigins::getIdentifierInfo(uint_fast64_t identifier) const {
+				return identifierToInfo[identifier];
+			}
+                
+			std::string const& ChoiceOrigins::getChoiceInfo(uint_fast64_t choiceIndex) const {
+				return getIdentifierInfo(getIdentifier(choiceIndex));
+			}
+            
+            std::shared_ptr<ChoiceOrigins> ChoiceOrigins::selectChoices(storm::storage::BitVector const& selectedChoices) const {
+                std::vector<uint_fast64_t> indexToIdentifierMapping(selectedChoices.getNumberOfSetBits());
+                storm::utility::vector::selectVectorValues(indexToIdentifierMapping, selectedChoices, indexToIdentifier);
+                return cloneWithNewIndexToIdentifierMapping(std::move(indexToIdentifierMapping));
+            }
+            
+            std::shared_ptr<ChoiceOrigins> ChoiceOrigins::selectChoices(std::vector<uint_fast64_t> const& selectedChoices) const {
+                std::vector<uint_fast64_t> indexToIdentifierMapping(selectedChoices.size());
+                storm::utility::vector::selectVectorValues(indexToIdentifierMapping, selectedChoices, indexToIdentifier);
+                return cloneWithNewIndexToIdentifierMapping(std::move(indexToIdentifierMapping));
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h
new file mode 100644
index 000000000..e869658ea
--- /dev/null
+++ b/src/storm/storage/sparse/ChoiceOrigins.h
@@ -0,0 +1,65 @@
+#pragma once
+
+#include <vector>
+#include <string>
+#include "storm/storage/BitVector.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            class PrismChoiceOrigins;
+            class JaniChoiceOrigins;
+            
+            /*!
+             * This class represents the origin of the choices of a model in terms of the input model specification
+             * (e.g., the Prism commands that induced the choice).
+             */
+            class ChoiceOrigins {
+            public:
+                
+                virtual ~ChoiceOrigins() = default;
+                
+                virtual bool isPrismChoiceOrigins() const;
+                virtual bool isJaniChoiceOrigins() const;
+                
+                PrismChoiceOrigins& asPrismChoiceOrigins();
+                PrismChoiceOrigins const& asPrismChoiceOrigins() const;
+                
+                JaniChoiceOrigins& asJaniChoiceOrigins();
+                JaniChoiceOrigins const& asJaniChoiceOrigins() const;
+                
+                /*
+                 * Returns a unique identifier of the origin of the given choice which can be used to e.g. check whether two choices have the same origin
+                 */
+                uint_fast64_t getIdentifier(uint_fast64_t choiceIndex) const;
+                
+                /*
+                 * Returns the information for the given choice origin identifier as a (human readable) string
+                 */
+                std::string const& getIdentifierInfo(uint_fast64_t identifier) const;
+                
+                /*
+                 * Returns the choice origin information as a (human readable) string.
+                 */
+                std::string const& getChoiceInfo(uint_fast64_t choiceIndex) const;
+                
+                
+                std::shared_ptr<ChoiceOrigins> selectChoices(storm::storage::BitVector const& selectedChoices) const;
+                std::shared_ptr<ChoiceOrigins> selectChoices(std::vector<uint_fast64_t> const& selectedChoiceIndices) const;
+
+            protected:
+                ChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping);
+                ChoiceOrigins(std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping);
+                
+                /*
+                 * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
+                 */
+                virtual std::shared_ptr<ChoiceOrigins> cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const = 0;
+                
+                std::vector<uint_fast64_t> indexToIdentifier;
+                std::vector<std::string> identifierToInfo;
+            };
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.cpp b/src/storm/storage/sparse/JaniChoiceOrigins.cpp
new file mode 100644
index 000000000..3548469f8
--- /dev/null
+++ b/src/storm/storage/sparse/JaniChoiceOrigins.cpp
@@ -0,0 +1,23 @@
+#include "storm/storage/sparse/JaniChoiceOrigins.h"
+
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            JaniChoiceOrigins::JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping) {
+				// Intentionally left empty
+			}
+
+            bool JaniChoiceOrigins::isJaniChoiceOrigins() const  {
+            	return true;
+            }
+             
+            std::shared_ptr<ChoiceOrigins> JaniChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const {
+                std::vector<std::string> identifierToInfoMapping = this->identifierToInfo;
+                return std::make_shared<JaniChoiceOrigins>(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping));
+            }
+            
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h
new file mode 100644
index 000000000..58518c561
--- /dev/null
+++ b/src/storm/storage/sparse/JaniChoiceOrigins.h
@@ -0,0 +1,40 @@
+#pragma once
+
+#include <memory>
+#include <string>
+
+#include "storm/storage/sparse/ChoiceOrigins.h"
+
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            
+            /*!
+             * This class represents for each choice the origin in the jani specification
+             */
+            class JaniChoiceOrigins : public ChoiceOrigins {
+            public:
+                
+                /*!
+                 * Creates a new representation of the choice indices to their origin in the Jani specification
+                 * // TODO complete this
+                 */
+                JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping);
+                
+                virtual ~JaniChoiceOrigins() = default;
+                
+                virtual bool isJaniChoiceOrigins() const override ;
+                
+                /*
+                 * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
+                 */
+                virtual std::shared_ptr<ChoiceOrigins> cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const override;
+                
+            private:
+                
+            };
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp
new file mode 100644
index 000000000..ec417bdff
--- /dev/null
+++ b/src/storm/storage/sparse/PrismChoiceOrigins.cpp
@@ -0,0 +1,37 @@
+#include "storm/storage/sparse/PrismChoiceOrigins.h"
+
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping, std::vector<CommandSet> const& identifierToCommandSetMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping), program(prismProgram), identifierToCommandSet(identifierToCommandSetMapping) {
+				// Intentionally left empty
+			}
+
+            PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping, std::vector<CommandSet>&& identifierToCommandSetMapping) : ChoiceOrigins(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping)), program(prismProgram), identifierToCommandSet(std::move(identifierToCommandSetMapping)) {
+				// Intentionally left empty
+            }
+                
+            bool PrismChoiceOrigins::isPrismChoiceOrigins() const  {
+            	return true;
+            }
+             
+            storm::prism::Program const& PrismChoiceOrigins::getProgram() const {
+            	return *program;
+            }
+                
+            PrismChoiceOrigins::CommandSet const& PrismChoiceOrigins::getCommandSet(uint_fast64_t choiceIndex) const {
+                return identifierToCommandSet[this->getIdentifier(choiceIndex)];
+			}
+            
+            std::shared_ptr<ChoiceOrigins> PrismChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const {
+                std::vector<CommandSet> identifierToCommandSetMapping = this->identifierToCommandSet;
+                std::vector<std::string> identifierToInfoMapping = this->identifierToInfo;
+                return std::make_shared<PrismChoiceOrigins>(this->program, std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping), std::move(identifierToCommandSetMapping));
+            }
+
+            
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h
new file mode 100644
index 000000000..0d65728a2
--- /dev/null
+++ b/src/storm/storage/sparse/PrismChoiceOrigins.h
@@ -0,0 +1,62 @@
+#pragma once
+
+#include <memory>
+#include <string>
+#include <boost/container/flat_set.hpp>
+
+#include "storm/storage/sparse/ChoiceOrigins.h"
+#include "storm/storage/prism/Program.h"
+
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            
+            /*!
+             * This class represents for each choice the set of prism commands that induced the choice
+             */
+            class PrismChoiceOrigins : public ChoiceOrigins {
+            public:
+                
+                typedef boost::container::flat_set<uint_fast64_t> CommandSet;
+                
+                /*!
+                 * Creates a new representation of the choice indices to their origin in the prism program
+                 * @param prismProgram The associated prism program
+                 * @param indexToIdentifierMapping maps a choice index to the internally used identifier of the choice origin
+                 * @param identifierToInfoMapping maps an origin identifier to a string representation of the origin
+                 * @param identifierToCommandSetMapping maps an origin identifier to the set of global indices of the corresponding prism commands
+                 */
+                PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<std::string> const& identifierToInfoMapping, std::vector<CommandSet> const& identifierToCommandSetMapping);
+                PrismChoiceOrigins(std::shared_ptr<storm::prism::Program const> const& prismProgram, std::vector<uint_fast64_t>&& indexToIdentifierMapping, std::vector<std::string>&& identifierToInfoMapping, std::vector<CommandSet>&& identifierToCommandSetMapping);
+                
+                virtual ~PrismChoiceOrigins() = default;
+                
+                virtual bool isPrismChoiceOrigins() const override ;
+                
+                /*
+                 * Returns the prism program associated with this
+                 */
+                storm::prism::Program const& getProgram() const;
+                
+                /*
+                 * Returns the set of prism commands that induced the choice with the given index.
+                 * The command set is represented by a set of global command indices
+                 */
+                CommandSet const& getCommandSet(uint_fast64_t choiceIndex) const;
+                
+                /*
+                 * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
+                 */
+                virtual std::shared_ptr<ChoiceOrigins> cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const override;
+                
+            private:
+                
+                std::shared_ptr<storm::prism::Program const> program;
+                std::vector<CommandSet> identifierToCommandSet;
+                
+            };
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 368a09618..c45c013b4 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -168,7 +168,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
             }
             storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
-            return builder.build();
+            return builder.build().getModel();
         }
     }