Explore relevant events further even if the DFT has already failed

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -59,8 +59,10 @@ namespace storm {
             //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
             //size_t currentFailable = 0;
             state->getFailableElements().init(exploreDependencies);
-            // Check for absorbing state
-            if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->getFailableElements().isEnd()) {
+            // Check for absorbing state:
+            // - either no relevant event remains (i.e., all relevant events have failed already), or
+            // - no BE can fail
+            if (!state->getFailableElements().hasRemainingRelevantEvent() || state->getFailableElements().isEnd()) {
                 Choice<ValueType, StateType> choice(0, true);
                 // Add self loop
                 choice.addProbability(state->getId(), storm::utility::one<ValueType>());
@@ -80,7 +82,6 @@ namespace storm {
                     // We discard further exploration as we already chose one dependent event
                     break;
                 }
-                STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
                 isFirst = false;
 
                 // Construct new state as copy from original one
@@ -120,6 +121,8 @@ namespace storm {
                     newState->updateFailableInRestrictions(next->id());
                 }
 
+                newState->updateRemainingRelevantEvents();
+
                 bool transient = false;
                 if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) {
                     auto beExp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(nextBE);

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

@@ -874,6 +874,18 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        std::set<size_t> DFT<ValueType>::getRelevantEvents() const {
+            std::set<size_t> relevantEvents;
+            for (auto const& elem : mElements) {
+                if (elem->isRelevant()) {
+                    relevantEvents.insert(elem->id());
+                }
+            }
+            return relevantEvents;
+        }
+
+
         template<typename ValueType>
         std::string DFT<ValueType>::getRelevantEventsString() const {
             std::stringstream stream;

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

@@ -318,6 +318,12 @@ namespace storm {
              */
             size_t getIndex(std::string const& name) const;
 
+            /*!
+             * Get all relevant events.
+             * @return List of all relevant events.
+             */
+            std::set<size_t> getRelevantEvents() const;
+
             /*!
              * Set the relevance flag for all elements according to the given relevant events.
              * @param relevantEvents All elements which should be to relevant. All elements not occuring are set to irrelevant.

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

@@ -7,7 +7,7 @@ namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
+        DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements(), dft.getRelevantEvents()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
             // TODO: use construct()
             
             // Initialize uses
@@ -33,7 +33,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        DFTState<ValueType>::DFTState(storm::storage::BitVector const& status, DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
+        DFTState<ValueType>::DFTState(storm::storage::BitVector const& status, DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements(), dft.getRelevantEvents()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
             // Intentionally left empty
         }
         
@@ -86,6 +86,11 @@ namespace storm {
                     STORM_LOG_TRACE("New dependency failure: " << *dependency);
                 }
             }
+
+            // Initialize remaining relevant events
+            failableElements.remainingRelevantEvents = mDft.getRelevantEvents();
+            this->updateRemainingRelevantEvents();
+
             mPseudoState = false;
         }
 
@@ -311,6 +316,18 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        void DFTState<ValueType>::updateRemainingRelevantEvents() {
+            for (auto it = failableElements.remainingRelevantEvents.begin(); it != failableElements.remainingRelevantEvents.end(); ) {
+                if (isOperational(*it)) {
+                    ++it;
+                } else {
+                    // Element is not relevant anymore
+                    it = failableElements.remainingRelevantEvents.erase(it);
+                }
+            }
+        }
+
         template<typename ValueType>
         ValueType DFTState<ValueType>::getBERate(size_t id) const {
             STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE.");

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

@@ -25,7 +25,7 @@ namespace storm {
 
             struct FailableElements {
 
-                FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) {
+                FailableElements(size_t nrElements, std::set<size_t> relevantEvents) : currentlyFailableBE(nrElements), remainingRelevantEvents(relevantEvents), it(currentlyFailableBE.begin()) {
                     // Intentionally left empty
                 }
 
@@ -103,10 +103,19 @@ namespace storm {
                     return !currentlyFailableBE.empty();
                 }
 
+                /*!
+                 * Check whether at least one relevant event has not failed yet.
+                 * @return True iff one relevant event is still operational.
+                 */
+                bool hasRemainingRelevantEvent() const {
+                    return !remainingRelevantEvents.empty();
+                }
+
                 mutable bool dependency;
 
                 storm::storage::BitVector currentlyFailableBE;
                 std::vector<size_t> mFailableDependencies;
+                std::set<size_t> remainingRelevantEvents;
 
                 mutable storm::storage::BitVector::const_iterator it;
                 mutable std::vector<size_t>::const_iterator itDep;
@@ -303,6 +312,11 @@ namespace storm {
              */
             void updateDontCareDependencies(size_t id);
 
+            /*!
+             * Update remaining relevant events.
+             */
+            void updateRemainingRelevantEvents();
+
             /**
              * Sets the next BE as failed
              * @param index Index in currentlyFailableBE of BE to fail

src/test/storm-dft/api/DftModelBuildingTest.cpp

@@ -32,8 +32,8 @@ namespace {
         storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries, relevantEvents, false);
         builder2.buildModel(0, 0.0);
         model = builder2.getModel();
-        EXPECT_EQ(448ul, model->getNumberOfStates());
-        EXPECT_EQ(1260ul, model->getNumberOfTransitions());
+        EXPECT_EQ(512ul, model->getNumberOfStates());
+        EXPECT_EQ(2305ul, model->getNumberOfTransitions());
 
         // Set relevant events (H)
         relevantEvents.clear();