Second try to improve performance for relevant events

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -42,8 +42,6 @@ namespace storm {
         {
             // Set relevant events
             this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents);
-            // Mark top level element as relevant
-            this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true);
             STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString());
             if (this->relevantEvents.empty()) {
                 // Only interested in top level event -> introduce unique failed state
@@ -477,9 +475,10 @@ namespace storm {
             modelComponents.stateLabeling.addLabel("init");
             STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped.");
             modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
-            // Label all states corresponding to their status (failed, failed/dont care BE)
+            // System failure
             modelComponents.stateLabeling.addLabel("failed");
 
+            // Label all states corresponding to their status (failed, don't care BE)
             // Collect labels for all necessary elements
             for (size_t id = 0; id < dft.nrElements(); ++id) {
                 std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
@@ -491,6 +490,7 @@ namespace storm {
 
             // Set labels to states
             if (this->uniqueFailedState) {
+                // Unique failed state has label 0
                 modelComponents.stateLabeling.addLabelToState("failed", 0);
             }
             for (auto const& stateIdPair : stateStorage.stateToId) {
@@ -499,7 +499,7 @@ namespace storm {
                 if (dft.hasFailed(state, *stateGenerationInfo)) {
                     modelComponents.stateLabeling.addLabelToState("failed", stateId);
                 }
-                // Set fail/dont care status for each necessary element
+                // Set failed/don't care status for each necessary element
                 for (size_t id = 0; id < dft.nrElements(); ++id) {
                     std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id);
                     if (element->isRelevant()){

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -61,22 +61,10 @@ namespace storm {
             //size_t currentFailable = 0;
             state->getFailableElements().init(exploreDependencies);
 
-            // Check whether operational relevant event remains
-            bool remainingRelevantEvent = true;
-            if (mDft.hasFailed(state)) {
-                remainingRelevantEvent = false;
-                // Toplevel has failed already -> check for possible other relevant events
-                for (auto const& event : mDft.getRelevantEvents()) {
-                    if (state->isOperational(event)) {
-                        remainingRelevantEvent = true;
-                        break;
-                    }
-                }
-            }
             // Check for absorbing state:
             // - either no relevant event remains (i.e., all relevant events have failed already), or
             // - no BE can fail
-            if (!remainingRelevantEvent || state->getFailableElements().isEnd()) {
+            if (!state->hasOperationalRelevantEvent() || state->getFailableElements().isEnd()) {
                 Choice<ValueType, StateType> choice(0, true);
                 // Add self loop
                 choice.addProbability(state->getId(), storm::utility::one<ValueType>());

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

@@ -873,11 +873,16 @@ namespace storm {
         template<typename ValueType>
         void DFT<ValueType>::setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const {
             mRelevantEvents.clear();
+            // Top level element is first element
+            mRelevantEvents.push_back(this->getTopLevelIndex());
             for (auto const& elem : mElements) {
-                if (relevantEvents.find(elem->id()) != relevantEvents.end()) {
+                if (relevantEvents.find(elem->id()) != relevantEvents.end() || elem->id() == this->getTopLevelIndex()) {
                     elem->setRelevance(true);
                     elem->setAllowDC(allowDCForRelevantEvents);
-                    mRelevantEvents.insert(elem->id());
+                    if (elem->id() != this->getTopLevelIndex()) {
+                        // Top level element was already added
+                        mRelevantEvents.push_back(elem->id());
+                    }
                 } else {
                     elem->setRelevance(false);
                     elem->setAllowDC(true);
@@ -886,7 +891,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::set<size_t> DFT<ValueType>::getRelevantEvents() const {
+        std::vector<size_t> const& DFT<ValueType>::getRelevantEvents() const {
             return mRelevantEvents;
         }
 

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

@@ -68,7 +68,7 @@ namespace storm {
             std::map<size_t, size_t> mRepresentants; // id element -> id representative
             std::vector<std::vector<size_t>> mSymmetries;
             std::map<size_t, DFTLayoutInfo> mLayoutInfo;
-            mutable std::set<size_t> mRelevantEvents;
+            mutable std::vector<size_t> mRelevantEvents;
 
         public:
             DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
@@ -324,7 +324,7 @@ namespace storm {
              * Get all relevant events.
              * @return List of all relevant events.
              */
-            std::set<size_t> getRelevantEvents() const;
+            std::vector<size_t> const& getRelevantEvents() const;
 
             /*!
              * Set the relevance flag for all elements according to the given relevant events.

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()), indexRelevant(0), 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()), indexRelevant(0), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
             // Intentionally left empty
         }
         
@@ -470,6 +470,22 @@ namespace storm {
             return false;
         }
 
+        template<typename ValueType>
+        bool DFTState<ValueType>::hasOperationalRelevantEvent() {
+            // Iterate over remaining relevant events
+            // All events with index < indexRelevant are already failed
+            while (indexRelevant < mDft.getRelevantEvents().size()) {
+                if (isOperational(mDft.getRelevantEvents()[indexRelevant])) {
+                    // Relevant event is still operational
+                    return true;
+                } else {
+                    // Consider next relevant event
+                    ++indexRelevant;
+                }
+            }
+            return false;
+        }
+
         template<typename ValueType>
         bool DFTState<ValueType>::claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children) {
             auto it = children.begin();

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

@@ -119,6 +119,7 @@ namespace storm {
             size_t mId;
             FailableElements failableElements;
             std::vector<size_t> mUsedRepresentants;
+            size_t indexRelevant;
             bool mPseudoState;
             bool mValid = true;
             const DFT<ValueType>& mDft;
@@ -330,12 +331,18 @@ namespace storm {
              */
             bool isEventDisabledViaRestriction(size_t id) const;
             
-            /**
+            /*!
              * Checks whether operational post seq elements are present
              * @param id
              * @return 
              */
             bool hasOperationalPostSeqElements(size_t id) const;
+
+            /*!
+             * Check whether at least one relevant event is still operational.
+             * @return True iff one operational relevant event exists.
+             */
+            bool hasOperationalRelevantEvent();
             
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;