Merge branch 'master' into almostsurepomdp

CHANGELOG.md

@@ -8,6 +8,7 @@ The releases of major and minor versions contain an overview of changes since th
 Version 1.5.x
 -------------
 ## Version 1.5.x (Under development)
+- Scheduler export: Properly handle models with end components. Added export in .json format.
 - CMake: Search for Gurobi prefers new versions
 - Tests: Enabled tests for permissive schedulers
 

src/storm-cli-utilities/model-handling.h

@@ -448,6 +448,11 @@ namespace storm {
                 options.setBuildAllLabels(true);
                 options.setBuildAllRewardModels(true);
             }
+
+            if (buildSettings.isAddOverlappingGuardsLabelSet()) {
+                options.setAddOverlappingGuardsLabel(true);
+            }
+
             return storm::api::buildSparseModel<ValueType>(input.model.get(), options, useJit, storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
         }
         

src/storm/api/export.h

@@ -48,7 +48,12 @@ namespace storm {
         void exportScheduler(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::storage::Scheduler<ValueType> const& scheduler, std::string const& filename) {
             std::ofstream stream;
             storm::utility::openFile(filename, stream);
+            std::string jsonFileExtension = ".json";
+            if (filename.size() > 4 && std::equal(jsonFileExtension.rbegin(), jsonFileExtension.rend(), filename.rbegin())) {
+                scheduler.printJsonToStream(stream, model);
+            } else {
                 scheduler.printToStream(stream, model);
+            }
             storm::utility::closeFile(stream);
         }
         

src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp

@@ -2,6 +2,8 @@
 
 #include "storm/storage/BitVector.h"
 #include "storm/storage/MaximalEndComponentDecomposition.h"
+#include "storm/storage/Scheduler.h"
+#include "storm/utility/graph.h"
 
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
@@ -11,7 +13,7 @@ namespace storm {
         namespace helper {
         
             template<typename ValueType>
-            SparseMdpEndComponentInformation<ValueType>::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits<uint64_t>::max()), eliminatedEndComponents(false), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) {
+            SparseMdpEndComponentInformation<ValueType>::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits<uint64_t>::max()), eliminatedEndComponents(!endComponentDecomposition.empty()), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) {
                 
                 // (1) Compute how many maybe states there are before each other maybe state.
                 maybeStatesBefore = maybeStates.getNumberOfSetBitsBeforeIndices();
@@ -90,7 +92,7 @@ namespace storm {
             }
 
             template<typename ValueType>
-            SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector) {
+            SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector, bool gatherExitChoices) {
                 
                 SparseMdpEndComponentInformation<ValueType> result(endComponentDecomposition, maybeStates);
                 
@@ -163,7 +165,7 @@ namespace storm {
                 // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs.
                 for (auto const& mec : endComponentDecomposition) {
                     builder.newRowGroup(currentRow);
-                    
+                    std::vector<uint64_t> exitChoices;
                     for (auto const& stateActions : mec) {
                         uint64_t const& state = stateActions.first;
                         for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) {
@@ -207,9 +209,16 @@ namespace storm {
                                 }
                             }
                             
+                            if (gatherExitChoices) {
+                                exitChoices.push_back(row);
+                            }
+                            
                             ++currentRow;
                         }
                     }
+                    if (gatherExitChoices) {
+                        result.ecToExitChoicesBefore.push_back(std::move(exitChoices));
+                    }
                 }
                 
                 submatrix = builder.build(currentRow);
@@ -217,7 +226,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector) {
+            SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector, bool gatherExitChoices) {
                 
                 SparseMdpEndComponentInformation<ValueType> result(endComponentDecomposition, maybeStates);
                 
@@ -271,7 +280,7 @@ namespace storm {
                 // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs.
                 for (auto const& mec : endComponentDecomposition) {
                     builder.newRowGroup(currentRow);
-                    
+                    std::vector<uint64_t> exitChoices;
                     for (auto const& stateActions : mec) {
                         uint64_t const& state = stateActions.first;
                         for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) {
@@ -304,9 +313,16 @@ namespace storm {
                                 }
                             }
                             
+                            if (gatherExitChoices) {
+                                exitChoices.push_back(row);
+                            }
+                            
                             ++currentRow;
                         }
                     }
+                    if (gatherExitChoices) {
+                        result.ecToExitChoicesBefore.push_back(std::move(exitChoices));
+                    }
                 }
                 
                 submatrix = builder.build();
@@ -315,23 +331,65 @@ namespace storm {
             
             template<typename ValueType>
             void SparseMdpEndComponentInformation<ValueType>::setValues(std::vector<ValueType>& result, storm::storage::BitVector const& maybeStates, std::vector<ValueType> const& fromResult) {
-                auto notInEcResultIt = result.begin();
+                // The following assumes that row groups associated to EC states are at the very end.
+                auto notInEcResultIt = fromResult.begin();
                 for (auto state : maybeStates) {
                     if (this->isStateInEc(state)) {
-                        result[state] = result[this->getRowGroupAfterElimination(state)];
+                        STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix.");
+                        result[state] = fromResult[this->getRowGroupAfterElimination(state)];
                     } else {
                         result[state] = *notInEcResultIt;
                         ++notInEcResultIt;
                     }
                 }
-                STORM_LOG_ASSERT(notInEcResultIt == result.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators.");
+                STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators.");
+            }
+            
+            template<typename ValueType>
+            void SparseMdpEndComponentInformation<ValueType>::setScheduler(storm::storage::Scheduler<ValueType>& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<uint64_t> const& fromResult) {
+                // The following assumes that row groups associated to EC states are at the very end.
+                storm::storage::BitVector maybeStatesWithoutChoice(maybeStates.size(), false);
+                storm::storage::BitVector ecStayChoices(transitionMatrix.getRowCount(), false);
+                auto notInEcResultIt = fromResult.begin();
+                for (auto const& state : maybeStates) {
+                    if (this->isStateInEc(state)) {
+                        STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix.");
+                        STORM_LOG_ASSERT(!ecToExitChoicesBefore.empty(), "No EC exit choices available. End Components have probably been build without.");
+                        uint64_t ec = getEc(state);
+                        auto const& exitChoices = ecToExitChoicesBefore[ec];
+                        uint64_t afterEliminationChoice = fromResult[this->getRowGroupAfterElimination(state)];
+                        uint64_t beforeEliminationGlobalChoiceIndex = exitChoices[afterEliminationChoice];
+                        bool noChoice = true;
+                        for (uint64_t globalChoice = transitionMatrix.getRowGroupIndices()[state]; globalChoice < transitionMatrix.getRowGroupIndices()[state+1]; ++globalChoice) {
+                            // Is this the selected exit choice?
+                            if (globalChoice == beforeEliminationGlobalChoiceIndex) {
+                                scheduler.setChoice(beforeEliminationGlobalChoiceIndex - transitionMatrix.getRowGroupIndices()[state], state);
+                                noChoice = false;
+                            } else {
+                                // Check if this is an exit choice
+                                if (std::find(exitChoices.begin(), exitChoices.end(), globalChoice) == exitChoices.end()) {
+                                    ecStayChoices.set(globalChoice, true);
+                                }
+                            }
+                        }
+                        maybeStatesWithoutChoice.set(state, noChoice);
+                    } else {
+                        scheduler.setChoice(*notInEcResultIt, state);
+                        ++notInEcResultIt;
+                    }
+                }
+                
+                STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators.");
+                // The maybeStates without a choice shall reach maybeStates with a choice with probability 1
+                storm::utility::graph::computeSchedulerProb1E(maybeStates, transitionMatrix, backwardTransitions, maybeStatesWithoutChoice, ~maybeStatesWithoutChoice, scheduler, ecStayChoices);
+
             }
             
             template class SparseMdpEndComponentInformation<double>;
             
 #ifdef STORM_HAVE_CARL
             template class SparseMdpEndComponentInformation<storm::RationalNumber>;
-            template class SparseMdpEndComponentInformation<storm::RationalFunction>;
+            //template class SparseMdpEndComponentInformation<storm::RationalFunction>;
 #endif
             
         }

src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h

@@ -12,6 +12,9 @@ namespace storm {
         
         template <typename ValueType>
         class MaximalEndComponentDecomposition;
+        
+        template <typename ValueType>
+        class Scheduler;
     }
     
     namespace modelchecker {
@@ -50,11 +53,12 @@ namespace storm {
 
                 uint64_t getNotInEcMarker() const;
 
-                static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector);
+                static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector, bool gatherExitChoices = false);
                 
-                static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector);
+                static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector, bool gatherExitChoices = false);
                 
                 void setValues(std::vector<ValueType>& result, storm::storage::BitVector const& maybeStates, std::vector<ValueType> const& fromResult);
+                void setScheduler(storm::storage::Scheduler<ValueType>& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<uint64_t> const& fromResult);
                 
             private:
                 // A constant that marks that a state is not contained in any EC.
@@ -70,6 +74,7 @@ namespace storm {
                 uint64_t numberOfMaybeStatesNotInEc;
                 uint64_t numberOfEc;
                 std::vector<uint64_t> maybeStateToEc;
+                std::vector<std::vector<uint64_t>> ecToExitChoicesBefore; // Only available, if gatherExitChoices was enabled. Empty otherwise.
             };
                         
         }

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -583,7 +583,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b) {
+            boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, bool produceScheduler) {
                 
                 // Get the set of states that (under some scheduler) can stay in the set of maybestates forever
                 storm::storage::BitVector candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates);
@@ -599,7 +599,7 @@ namespace storm {
                 // Only do more work if there are actually end-components.
                 if (doDecomposition && !endComponentDecomposition.empty()) {
                     STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s).");
-                    SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr);
+                    SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr, produceScheduler);
                     
                     // If the solve goal has relevant values, we need to adjust them.
                     if (goal.hasRelevantValues()) {
@@ -663,10 +663,7 @@ namespace storm {
                         // If the hint information tells us that we have to eliminate MECs, we do so now.
                         boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
                         if (hintInformation.getEliminateEndComponents()) {
-                            ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b);
+                            ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b, produceScheduler);
-
-                            // Make sure we are not supposed to produce a scheduler if we actually eliminate end components.
-                            STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver.");
                         } else {
                             // Otherwise, we compute the standard equations.
                             computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b);
@@ -678,16 +675,18 @@ namespace storm {
                         // If we eliminated end components, we need to extract the result differently.
                         if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
                             ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
+                            if (produceScheduler) {
+                                ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler());
+                            }
                         } else {
                             // Set values of resulting vector according to result.
                             storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
-                        }
-
                             if (produceScheduler) {
                                 extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates);
                             }
                         }
                     }
+                }
 
                 // Extend scheduler with choices for the states in the qualitative state sets.
                 if (produceScheduler) {
@@ -1028,7 +1027,7 @@ namespace storm {
             }
             
             template<typename ValueType>
-            boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional<storm::storage::BitVector> const& selectedChoices, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, boost::optional<std::vector<ValueType>>& oneStepTargetProbabilities) {
+            boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional<storm::storage::BitVector> const& selectedChoices, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, boost::optional<std::vector<ValueType>>& oneStepTargetProbabilities, bool produceScheduler) {
                 
                 // Start by computing the choices with reward 0, as we only want ECs within this fragment.
                 storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount());
@@ -1075,7 +1074,7 @@ namespace storm {
                 // Only do more work if there are actually end-components.
                 if (doDecomposition && !endComponentDecomposition.empty()) {
                     STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs.");
-                    SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b);
+                    SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler);
                     
                     // If the solve goal has relevant values, we need to adjust them.
                     if (goal.hasRelevantValues()) {
@@ -1163,10 +1162,7 @@ namespace storm {
                         // If the hint information tells us that we have to eliminate MECs, we do so now.
                         boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
                         if (hintInformation.getEliminateEndComponents()) {
-                            ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities);
+                            ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities, produceScheduler);
-                            
-                            // Make sure we are not supposed to produce a scheduler if we actually eliminate end components.
-                            STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver.");
                         } else {
                             // Otherwise, we compute the standard equations.
                             computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
@@ -1184,16 +1180,18 @@ namespace storm {
                         // If we eliminated end components, we need to extract the result differently.
                         if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
                             ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
+                            if (produceScheduler) {
+                                ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler());
+                            }
                         } else {
                             // Set values of resulting vector according to result.
                             storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
-                        }
-                        
                             if (produceScheduler) {
                                 extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices);
                             }
                         }
                     }
+                }
                 
                 // Extend scheduler with choices for the states in the qualitative state sets.
                 if (produceScheduler) {

src/storm/models/sparse/Model.cpp

@@ -420,6 +420,15 @@ namespace storm {
                 this->transitionMatrix = std::move(transitionMatrix);
             }
 
+            template<typename ValueType, typename RewardModelType>
+            bool Model<ValueType, RewardModelType>::isSinkState(uint64_t state) const {
+                for (auto const& entry : this->getTransitionMatrix().getRowGroup(state)) {
+                    if (entry.getColumn() != state) { return false; }
+                    if (storm::utility::isOne(entry.getValue())) { return false; }
+                }
+                return true;
+            }
+
             template<typename ValueType, typename RewardModelType>
             bool Model<ValueType, RewardModelType>::isSparseModel() const {
                 return true;

src/storm/models/sparse/Model.h

@@ -319,6 +319,8 @@ namespace storm {
                  */
                 virtual void printModelInformationToStream(std::ostream& out) const override;
 
+                bool isSinkState(uint64_t sink) const;
+                
                 /*!
                  * Exports the model to the dot-format and prints the result to the given stream.
                  *

src/storm/settings/modules/BuildSettings.cpp

@@ -33,6 +33,7 @@ namespace storm {
             const std::string buildChoiceOriginsOptionName = "buildchoiceorig";
             const std::string buildStateValuationsOptionName = "buildstateval";
             const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate";
+            const std::string buildOverlappingGuardsLabelOptionName = "overlappingguardslabel";
             const std::string bitsForUnboundedVariablesOptionName = "int-bits";
 
             BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
@@ -51,6 +52,7 @@ namespace storm {
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").setIsAdvanced().build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, buildOverlappingGuardsLabelOptionName, false, "For states where multiple guards are enabled, we add a label (for debugging DTMCs)").setIsAdvanced().build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build());
             }
@@ -99,6 +101,10 @@ namespace storm {
                 return this->getOption(buildOutOfBoundsStateOptionName).getHasOptionBeenSet();
             }
 
+            bool BuildSettings::isAddOverlappingGuardsLabelSet() const {
+                return this->getOption(buildOverlappingGuardsLabelOptionName).getHasOptionBeenSet();
+            }
+
             storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const {
                 std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
                 if (explorationOrderAsString == "dfs") {

src/storm/settings/modules/BuildSettings.h

@@ -100,6 +100,11 @@ namespace storm {
                  */
                 bool isBuildOutOfBoundsStateSet() const;
 
+                /*!
+                 * Retrieves whether to build the overlapping label
+                 */
+                 bool isAddOverlappingGuardsLabelSet() const;
+
                 /*!
                  * Retrieves the number of bits that should be used to represent unbounded integer variables
                  * @return

src/storm/settings/modules/IOSettings.cpp

@@ -59,7 +59,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, false, "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportMonotonicityName, false, "Exports the result of monotonicity checking to the given file.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());

src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp

@@ -0,0 +1,50 @@
+#include "storm/simulator/DiscreteTimeSparseModelSimulator.h"
+#include "storm/models/sparse/Model.h"
+
+namespace storm {
+    namespace simulator {
+        template<typename ValueType, typename RewardModelType>
+        DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), currentState(*model.getInitialStates().begin()) {
+            STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits()==1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index.");
+
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        void DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::setSeed(uint64_t seed) {
+            generator = storm::utility::RandomProbabilityGenerator<double>(seed);
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        bool DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::step(uint64_t action) {
+            // TODO lots of optimization potential.
+            //  E.g., do not sample random numbers if there is only a single transition
+            ValueType probability = generator.random();
+            STORM_LOG_ASSERT(action < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions");
+            uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + action;
+            ValueType sum = storm::utility::zero<ValueType>();
+            for (auto const& entry : model.getTransitionMatrix().getRow(row)) {
+                sum += entry.getValue();
+                if (sum >= probability) {
+                    currentState = entry.getColumn();
+                    return true;
+                }
+            }
+            return false;
+            STORM_LOG_ASSERT(false, "This position should never be reached");
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        uint64_t DiscreteTimeSparseModelSimulator<ValueType, RewardModelType>::getCurrentState() const {
+            return currentState;
+        }
+
+        template<typename ValueType, typename RewardModelType>
+        bool DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::resetToInitial() {
+            currentState = *model.getInitialStates().begin();
+            return true;
+        }
+
+
+        template class DiscreteTimeSparseModelSimulator<double>;
+    }
+}

src/storm/simulator/DiscreteTimeSparseModelSimulator.h

@@ -0,0 +1,30 @@
+#include <cstdint>
+#include "storm/models/sparse/Model.h"
+#include "storm/utility/random.h"
+
+namespace storm {
+    namespace simulator {
+
+        /**
+         * This class is a low-level interface to quickly sample from Discrete-Time Models
+         * stored explicitly as a SparseModel.
+         * Additional information about state, actions, should be obtained via the model itself.
+         *
+         * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself.
+         * @tparam ModelType
+         */
+        template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+        class DiscreteTimeSparseModelSimulator {
+        public:
+            DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model);
+            void setSeed(uint64_t);
+            bool step(uint64_t action);
+            uint64_t getCurrentState() const;
+            bool resetToInitial();
+        protected:
+            uint64_t currentState;
+            storm::models::sparse::Model<ValueType, RewardModelType> const& model;
+            storm::utility::RandomProbabilityGenerator<ValueType> generator;
+        };
+    }
+}

src/storm/storage/Scheduler.cpp

@@ -1,7 +1,8 @@
-#include <storm/utility/vector.h>
+#include "storm/utility/vector.h"
 #include "storm/storage/Scheduler.h"
 
 #include "storm/utility/macros.h"
+#include "storm/adapters/JsonAdapter.h"
 #include "storm/exceptions/NotImplementedException.h"
 #include <boost/algorithm/string/join.hpp>
 
@@ -222,6 +223,54 @@ namespace storm {
             out << "___________________________________________________________________" << std::endl;
         }
 
+        template <>
+        void Scheduler<float>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<float>> model, bool skipUniqueChoices) const {
+            STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers not implemented for this value type.");
+        }
+
+        template <typename ValueType>
+        void Scheduler<ValueType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
+            STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler.");
+            STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
+            STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented.");
+            storm::json<storm::RationalNumber> output;
+            for (uint64_t state = 0; state < schedulerChoices.front().size(); ++state) {
+                // Check whether the state is skipped
+                if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) {
+                    continue;
+                }
+                storm::json<storm::RationalNumber> stateChoicesJson;
+                if (model && model->hasStateValuations()) {
+                    stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson();
+                } else {
+                    stateChoicesJson["s"] = state;
+                }
+                auto const& choice = schedulerChoices.front()[state];
+                storm::json<storm::RationalNumber> choicesJson;
+                if (choice.isDefined()) {
+                    for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
+                        uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
+                        storm::json<storm::RationalNumber> choiceJson;
+                        if (model && model->hasChoiceOrigins() && model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) {
+                            choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex);
+                        }
+                        if (model && model->hasChoiceLabeling()) {
+                            auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex);
+                            choiceJson["labels"] = std::vector<std::string>(choiceLabels.begin(), choiceLabels.end());
+                        }
+                        choiceJson["index"] = globalChoiceIndex;
+                        choiceJson["prob"] = storm::utility::convertNumber<storm::RationalNumber>(choiceProbPair.second);
+                        choicesJson.push_back(std::move(choiceJson));
+                    }
+                } else {
+                    choicesJson = "undefined";
+                }
+                stateChoicesJson["c"] = std::move(choicesJson);
+                output.push_back(std::move(stateChoicesJson));
+            }
+            out << output.dump(4);
+        }
+
         template class Scheduler<double>;
         template class Scheduler<float>;
         template class Scheduler<storm::RationalNumber>;

src/storm/storage/Scheduler.h

@@ -112,6 +112,11 @@ namespace storm {
             void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
 
             
+            /*!
+             * Prints the scheduler in json format to the given output stream.
+             */
+             void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false) const;
+            
         private:
             
             boost::optional<storm::storage::MemoryStructure> memoryStructure;

src/storm/storage/expressions/SimpleValuation.cpp

@@ -144,6 +144,23 @@ namespace storm {
             }
         }
         
+        typename SimpleValuation::Json SimpleValuation::toJson() const {
+            Json result;
+            for (auto const& variable : getManager()) {
+                if (variable.second.isBooleanType()) {
+                    result[variable.first.getName()] = this->getBooleanValue(variable.first);
+                } else if (variable.second.isIntegerType()) {
+                    result[variable.first.getName()] = this->getIntegerValue(variable.first);
+                } else if (variable.second.isRationalType()) {
+                    result[variable.first.getName()] = this->getRationalValue(variable.first);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
+                }
+            }
+            return result;
+        }
+        
+        
         std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) {
             out << valuation.toString(false) << std::endl;
             return out;

src/storm/storage/expressions/SimpleValuation.h

@@ -6,6 +6,7 @@
 #include <set>
 
 #include "storm/storage/expressions/Valuation.h"
+#include "storm/adapters/JsonAdapter.h"
 
 namespace storm {
     namespace expressions {
@@ -17,6 +18,8 @@ namespace storm {
         public:
             friend class SimpleValuationPointerHash;
             friend class SimpleValuationPointerLess;
+            typedef storm::json<storm::RationalNumber> Json;
+
 
             /*!
              * Creates an empty simple valuation that is associated to no manager and has no variables.
@@ -63,6 +66,7 @@ namespace storm {
             virtual std::string toPrettyString(std::set<storm::expressions::Variable> const& selectedVariables) const;
 
             virtual std::string toString(bool pretty = true) const;
+            Json toJson() const;
 
             friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation);
             

src/storm/storage/jani/JSONExporter.cpp

@@ -995,19 +995,14 @@ namespace storm {
             return destDeclarations;
         }
         
-        ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+        ExportJsonType buildEdge(Edge const& edge , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
-            ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
-            for(auto const& edge : edges) {
-                if (edge.getGuard().isFalse()) {
-                    continue;
-                }
             STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed.");
             ExportJsonType edgeEntry;
             edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex());
-                if(!edge.hasSilentAction()) {
+            if (!edge.hasSilentAction()) {
                 edgeEntry["action"] = actionNames.at(edge.getActionIndex());
             }
-                if(edge.hasRate()) {
+            if (edge.hasRate()) {
                 edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables);
                 if (commentExpressions) {
                     edgeEntry["rate"]["comment"] = edge.getRate().toString();
@@ -1023,8 +1018,16 @@ namespace storm {
             if (!edge.getAssignments().empty()) {
                 edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions);
             }
+            return edgeEntry;
+        }
         
-                edgeDeclarations.push_back(std::move(edgeEntry));
+        ExportJsonType buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
+            ExportJsonType edgeDeclarations = std::vector<ExportJsonType>();
+            for(auto const& edge : edges) {
+                if (edge.getGuard().isFalse()) {
+                    continue;
+                }
+                edgeDeclarations.push_back(buildEdge(edge, actionNames, locationNames, constants, globalVariables, localVariables, commentExpressions));
             }
             return edgeDeclarations;
         }
@@ -1065,6 +1068,11 @@ namespace storm {
             jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
         }
         
+        ExportJsonType JsonExporter::getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions) {
+            auto const& automaton = janiModel.getAutomaton(automatonIndex);
+            return buildEdge(automaton.getEdge(edgeIndex), janiModel.getActionIndexToNameMap(), automaton.buildIdToLocationNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), automaton.getVariables(), commentExpressions);
+        }
+        
         std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) {
             switch(ft) {
                 case storm::modelchecker::FilterType::MIN:

src/storm/storage/jani/JSONExporter.h

@@ -89,7 +89,7 @@ namespace storm {
             static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false);
             static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false);
             
-            
+            static ExportJsonType getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions = true);
         private:
             void convertModel(storm::jani::Model const& model, bool commentExpressions = true);
             void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);

src/storm/storage/sparse/ChoiceOrigins.cpp

@@ -67,6 +67,18 @@ namespace storm {
 				return getIdentifierInfo(getIdentifier(choiceIndex));
 			}
    
+			typename ChoiceOrigins::Json const& ChoiceOrigins::getIdentifierAsJson(uint_fast64_t identifier) const {
+                STORM_LOG_ASSERT(identifier < this->getNumberOfIdentifiers(), "Invalid choice origin identifier: " << identifier);
+                if (identifierToJson.empty()) {
+                    computeIdentifierJson();
+                }
+				return identifierToJson[identifier];
+            }
+            
+            typename ChoiceOrigins::Json const& ChoiceOrigins::getChoiceAsJson(uint_fast64_t choiceIndex) const {
+                return getIdentifierAsJson(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);

src/storm/storage/sparse/ChoiceOrigins.h

@@ -5,6 +5,7 @@
 #include "storm/storage/BitVector.h"
 #include "storm/models/sparse/ChoiceLabeling.h"
 
+#include "storm/adapters/JsonAdapter.h"
 
 namespace storm {
     namespace storage {
@@ -19,6 +20,7 @@ namespace storm {
              */
             class ChoiceOrigins {
             public:
+                typedef storm::json<storm::RationalNumber> Json;
                 
                 virtual ~ChoiceOrigins() = default;
                 
@@ -63,6 +65,16 @@ namespace storm {
                  */
                 std::string const& getChoiceInfo(uint_fast64_t choiceIndex) const;
                 
+                /*
+                 * Returns the information for the given choice origin identifier as a (human readable) string
+                 */
+                Json const& getIdentifierAsJson(uint_fast64_t identifier) const;
+                
+                /*
+                 * Returns the choice origin information as a (human readable) string.
+                 */
+                Json const& getChoiceAsJson(uint_fast64_t choiceIndex) const;
+                
                 /*
                  * Derive new choice origins from this by selecting the given choices.
                  */
@@ -95,11 +107,19 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const = 0;
                 
+                /*
+                 * Computes the identifier infos (i.e., human readable strings representing the choice origins).
+                 */
+                virtual void computeIdentifierJson() const = 0;
+                
                 std::vector<uint_fast64_t> indexToIdentifier;
                 
                 // cached identifier infos might be empty if identifiers have not been generated yet.
                 mutable std::vector<std::string> identifierToInfo;
                 
+                // cached identifier infos might be empty if identifiers have not been generated yet.
+                mutable std::vector<Json> identifierToJson;
+
             };
         }
     }

src/storm/storage/sparse/JaniChoiceOrigins.cpp

@@ -1,6 +1,7 @@
 #include "storm/storage/sparse/JaniChoiceOrigins.h"
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/JSONExporter.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -52,6 +53,32 @@ namespace storm {
                 }
             }
             
+            void JaniChoiceOrigins::computeIdentifierJson() const {
+                this->identifierToJson.clear();
+                this->identifierToJson.reserve(this->getNumberOfIdentifiers());
+                for (auto const& set : identifierToEdgeIndexSet) {
+                    Json setJson;
+                    if (set.empty()) {
+                        setJson = "No origin";
+                    } else {
+                        bool first = true;
+                        std::vector<Json> edgesJson;
+                        for (auto const& edgeIndex : set) {
+                            auto autAndEdgeOffset = model->decodeAutomatonAndEdgeIndices(edgeIndex);
+                            auto const& automaton = model->getAutomaton(autAndEdgeOffset.first);
+                            auto const& edge = automaton.getEdge(autAndEdgeOffset.second);
+                            if (first) {
+                                setJson["action-label"] = model->getAction(edge.getActionIndex()).getName();
+                                first = false;
+                            }
+                            edgesJson.push_back(storm::jani::JsonExporter::getEdgeAsJson(*model, autAndEdgeOffset.first, autAndEdgeOffset.second));
+                            edgesJson.back()["automaton"] = automaton.getName();
+                        }
+                        setJson["transitions"] = std::move(edgesJson);
+                    }
+                    this->identifierToJson.push_back(std::move(setJson));
+                }
+            }
         }
     }
 }

src/storm/storage/sparse/JaniChoiceOrigins.h

@@ -59,6 +59,11 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const override;
                 
+                /*
+                 * Computes the identifier infos as json (i.e., a machine readable representation of the choice origins).
+                 */
+                virtual void computeIdentifierJson() const override;
+                
                 std::shared_ptr<storm::jani::Model const> model;
                 std::vector<EdgeIndexSet> identifierToEdgeIndexSet;
             };

src/storm/storage/sparse/PrismChoiceOrigins.cpp

@@ -108,6 +108,54 @@ namespace storm {
                 STORM_LOG_DEBUG("Generated the following names for the choice origins: " << storm::utility::vector::toString(this->identifierToInfo));
                 STORM_LOG_ASSERT(storm::utility::vector::isUnique(this->identifierToInfo), "The generated names for the prism choice origins are not unique.");
             }
+            
+            void PrismChoiceOrigins::computeIdentifierJson() const {
+                this->identifierToJson.clear();
+                this->identifierToJson.reserve(this->getNumberOfIdentifiers());
+                for (CommandSet const& set : identifierToCommandSet) {
+                    // Get a string representation of this command set.
+                    Json setJson;
+                    if (set.empty()) {
+                        setJson = "No origin";
+                    } else {
+                        bool first = true;
+                        std::vector<Json> commandsJson;
+                        for (auto const& commandIndex : set) {
+                            Json commandJson;
+                            auto moduleCommandPair = program->getModuleCommandIndexByGlobalCommandIndex(commandIndex);
+                            storm::prism::Module const& module = program->getModule(moduleCommandPair.first);
+                            storm::prism::Command const& command = module.getCommand(moduleCommandPair.second);
+                            if (first) {
+                                setJson["action-label"] = command.getActionName();
+                                first = false;
+                            }
+                            commandJson["module"] = module.getName();
+                            commandJson["guard"] = command.getGuardExpression().toString();
+                            std::vector<Json> updatesJson;
+                            for (auto const& update : command.getUpdates()) {
+                                Json updateJson;
+                                updateJson["prob"] = update.getLikelihoodExpression().toString();
+                                std::stringstream assignmentsString;
+                                bool firstAssignment = true;
+                                for (auto const& a : update.getAssignments()) {
+                                    if (firstAssignment) {
+                                        firstAssignment = false;
+                                    } else {
+                                        assignmentsString << " & ";
+                                    }
+                                    assignmentsString << a;
+                                }
+                                updateJson["result"] = assignmentsString.str();
+                                updatesJson.push_back(std::move(updateJson));
+                            }
+                            commandJson["updates"] = updatesJson;
+                            commandsJson.push_back(std::move(commandJson));
+                        }
+                        setJson["transitions"] = commandsJson;
+                    }
+                    this->identifierToJson.push_back(std::move(setJson));
+                }
+            }
         }
     }
 }

src/storm/storage/sparse/PrismChoiceOrigins.h

@@ -62,6 +62,11 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const override;
                 
+                /*
+                 * Computes the identifier infos as json (i.e., a machine readable representation of the choice origins).
+                 */
+                virtual void computeIdentifierJson() const override;
+                
                 std::shared_ptr<storm::prism::Program const> program;
                 std::vector<CommandSet> identifierToCommandSet;
             };

src/storm/utility/graph.cpp

@@ -552,9 +552,11 @@ namespace storm {
                 // set an arbitrary (valid) choice for the psi states.
                 for (auto const& psiState : psiStates) {
                     for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) {
+                        if (!scheduler.getChoice(psiState, memState).isDefined()) {
                             scheduler.setChoice(0, psiState, memState);
                         }
                     }
+                }
                 
                 // Now perform a backwards search from the psi states and store choices with prob. 1
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();

src/storm/utility/random.cpp

@@ -0,0 +1,24 @@
+#include "storm/utility/random.h"
+
+namespace storm {
+    namespace utility {
+        RandomProbabilityGenerator<double>::RandomProbabilityGenerator()
+        : distribution(0.0, 1.0)
+        {
+            std::random_device rd;
+            engine = std::mt19937(rd());
+        }
+
+        RandomProbabilityGenerator<double>::RandomProbabilityGenerator(uint64_t seed)
+        : engine(seed), distribution(0.0, 1.0)
+        {
+
+        }
+
+        double RandomProbabilityGenerator<double>::random() {
+            return distribution(engine);
+        }
+
+
+    }
+}

src/storm/utility/random.h

@@ -0,0 +1,29 @@
+#include <random>
+
+namespace storm {
+    namespace utility {
+        template<typename ValueType>
+        class RandomProbabilityGenerator {
+        public:
+            RandomProbabilityGenerator();
+            RandomProbabilityGenerator(uint64_t seed);
+            ValueType random() const;
+
+        };
+
+        template<>
+        class RandomProbabilityGenerator<double> {
+        public:
+            RandomProbabilityGenerator();
+            RandomProbabilityGenerator(uint64_t seed);
+            double random();
+        private:
+            std::uniform_real_distribution<double> distribution;
+            std::mt19937 engine;
+
+        };
+
+
+
+    }
+}