diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 495631817..1e9a53045 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/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()); + 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)); } diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 6a926e3a3..8ae059104 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -18,9 +18,10 @@ namespace storm { template DFT::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;