Allow empty choices due to restrictions in state exploration

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -204,7 +204,14 @@ namespace storm {
                     return exploreState(stateToIdCallback, false);
                 }
             } else {
-                STORM_LOG_ASSERT(choice.size() > 0, "No transitions were generated");
+                if (choice.size() == 0) {
+                    // No transition was generated
+                    STORM_LOG_TRACE("No transitions were generated.");
+                    // Add self loop
+                    choice.addProbability(state->getId(), storm::utility::one<ValueType>());
+                    STORM_LOG_TRACE("Added self loop for " << state->getId());
+                }
+                STORM_LOG_ASSERT(choice.size() > 0, "At least one choice should have been generated.");
                 // Add all rates as one choice
                 result.addChoice(std::move(choice));
             }

src/storm-dft/storage/dft/DFT.cpp

@@ -18,9 +18,10 @@ namespace storm {
 
         template<typename ValueType>
         DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
+            // Check that ids correspond to indices in the element vector
             STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect.");
             size_t nrRepresentatives = 0;
-            
+
             for (auto& elem : mElements) {
                 if (isRepresentative(elem->id())) {
                     ++nrRepresentatives;