Added assertions to exclude self-loops in DFT state generation

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -161,6 +161,7 @@ namespace storm {
                         ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
                         choice.addProbability(unsuccessfulStateId, remainingProbability);
                         STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
+                        STORM_LOG_ASSERT(unsuccessfulStateId != state->getId(), "Self loop was added (through PDEP) for " << unsuccessfulStateId << " and failure of " << nextBE->name());
                     }
                     result.addChoice(std::move(choice));
                 } else {
@@ -176,6 +177,7 @@ namespace storm {
                     choice.addProbability(newStateId, rate);
                     STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate);
                 }
+                STORM_LOG_ASSERT(newStateId != state->getId(), "Self loop was added for " << newStateId << " and failure of " << nextBE->name());
 
                 ++currentFailable;
             } // end while failing BE

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

@@ -249,6 +249,7 @@ namespace storm {
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
                 assert(dependency->dependentEvents().size() == 1);
                 std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true);
+                STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << res.first->toString() << " has already failed.");
                 mFailableDependencies.erase(mFailableDependencies.begin() + index);
                 setFailed(res.first->id());
                 setDependencySuccessful(dependency->id());
@@ -257,6 +258,7 @@ namespace storm {
                 // Consider "normal" failure
                 STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid.");
                 std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(mCurrentlyFailableBE[index]), false);
+                STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << res.first->toString() << " has already failed.");
                 STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail.");
                 mCurrentlyFailableBE.erase(mCurrentlyFailableBE.begin() + index);
                 setFailed(res.first->id());