Improved explicit model building:

- There is now an option to generate a choice labeling that  corresponds to the specified action names.
- The old choice labeling (where each choice was labeled with an index set representing the corresponding prism commands) is renamed to choiceOrigins and has been improved towards support of other input formats (such as Jani) and other applications such as scheduler synthesis

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;
+        }
 
     }
 }

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;

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);
+        }
+        
+    }
+}

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;
+        };
+    }
+}
+    

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;
         }

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;
             

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
+        
+    }
+}

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;
+        };
+    }
+}

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>

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>

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>());

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>;
 

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.

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>;
 

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;
 

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 {

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));
+            }
+        }
+    }
+}

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;
+            };
+        }
+    }
+}

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));
+            }
+            
+        }
+    }
+}

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:
+                
+            };
+        }
+    }
+}

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));
+            }
+
+            
+        }
+    }
+}

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;
+                
+            };
+        }
+    }
+}

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();
         }
     }