Try to improve performance for relevant events

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -60,10 +60,23 @@ namespace storm {
             //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
             //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 (!state->getFailableElements().hasRemainingRelevantEvent() || state->getFailableElements().isEnd()) {
+            if (!remainingRelevantEvent || state->getFailableElements().isEnd()) {
                 Choice<ValueType, StateType> choice(0, true);
                 // Add self loop
                 choice.addProbability(state->getId(), storm::utility::one<ValueType>());
@@ -122,8 +135,6 @@ 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

@@ -17,7 +17,8 @@ namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
+        DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0),
+                                                                                              mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
             // Check that ids correspond to indices in the element vector
             STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect.");
 
@@ -32,7 +33,8 @@ namespace storm {
                     ++mNrOfSpares;
                     mMaxSpareChildCount = std::max(mMaxSpareChildCount, std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children().size());
                     for (auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
-                        STORM_LOG_THROW(spareReprs->isGate() || spareReprs->isBasicElement(), storm::exceptions::WrongFormatException, "Child '" << spareReprs->name() << "' of spare '" << elem->name() << "' must be gate or BE.");
+                        STORM_LOG_THROW(spareReprs->isGate() || spareReprs->isBasicElement(), storm::exceptions::WrongFormatException,
+                                        "Child '" << spareReprs->name() << "' of spare '" << elem->name() << "' must be gate or BE.");
                         std::set<size_t> module = {spareReprs->id()};
                         spareReprs->extendSpareModule(module);
                         std::vector<size_t> sparesAndBes;
@@ -72,7 +74,8 @@ namespace storm {
             if (!mTopModule.empty()) {
                 for (auto& module : mSpareModules) {
                     if (std::find(module.second.begin(), module.second.end(), mTopModule.front()) != module.second.end()) {
-                        STORM_LOG_WARN("Elements of spare module '" << getElement(module.first)->name() << "' also contained in top module. All elements of this spare module will be activated from the beginning on.");
+                        STORM_LOG_WARN("Elements of spare module '" << getElement(module.first)->name()
+                                                                    << "' also contained in top module. All elements of this spare module will be activated from the beginning on.");
                         module.second.clear();
                     }
                 }
@@ -179,7 +182,8 @@ namespace storm {
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
                 visitQueue.push(dependency->id());
                 visitQueue.push(dependency->triggerEvent()->id());
-                STORM_LOG_THROW(dependency->dependentEvents().size() == 1, storm::exceptions::NotSupportedException, "Direct state generation does not support n-ary dependencies. Consider rewriting them by setting the binary dependency flag.");
+                STORM_LOG_THROW(dependency->dependentEvents().size() == 1, storm::exceptions::NotSupportedException,
+                                "Direct state generation does not support n-ary dependencies. Consider rewriting them by setting the binary dependency flag.");
                 visitQueue.push(dependency->dependentEvents()[0]->id());
             }
             stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
@@ -225,7 +229,8 @@ namespace storm {
         }
 
         template<typename ValueType>
-        size_t DFT<ValueType>::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const {
+        size_t DFT<ValueType>::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, storm::storage::BitVector& visited,
+                                                             size_t stateIndex) const {
             while (!visitQueue.empty()) {
                 size_t id = visitQueue.front();
                 visitQueue.pop();
@@ -338,7 +343,8 @@ namespace storm {
                 // Accumulate children names
                 std::vector<std::string> childrenNames;
                 for (size_t i = 1; i < rewrites.size(); ++i) {
-                    STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have not the same father for rewrite " << mElements[rewrites[i]]->name());
+                    STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(),
+                                     "Children have not the same father for rewrite " << mElements[rewrites[i]]->name());
                     childrenNames.push_back(mElements[rewrites[i]]->name());
                 }
 
@@ -621,6 +627,7 @@ namespace storm {
                 }
             }
             // TODO check VOT gates
+            // TODO check only one constant failed event
             return wellformed;
         }
 
@@ -744,7 +751,8 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void DFT<ValueType>::findSymmetriesHelper(std::vector<size_t> const& candidates, DFTColouring<ValueType> const& colouring, std::map<size_t, std::vector<std::vector<size_t>>>& result) const {
+        void DFT<ValueType>::findSymmetriesHelper(std::vector<size_t> const& candidates, DFTColouring<ValueType> const& colouring,
+                                                  std::map<size_t, std::vector<std::vector<size_t>>>& result) const {
             if (candidates.size() <= 0) {
                 return;
             }
@@ -807,7 +815,8 @@ namespace storm {
                         std::vector<size_t> rewrite = {e->id(), child->id()};
                         for (size_t isdElemId : ISD) {
                             if (isdElemId == child->id()) continue;
-                           if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr<DFTElement<ValueType>> const& e) { return e->id() == isdElemId; } ) != children.end()) {
+                            if (std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr<DFTElement<ValueType>> const& e) { return e->id() == isdElemId; }) !=
+                                children.end()) {
                                 // element in subtree is also child
                                 rewrite.push_back(isdElemId);
                             }
@@ -863,10 +872,12 @@ namespace storm {
 
         template<typename ValueType>
         void DFT<ValueType>::setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const {
+            mRelevantEvents.clear();
             for (auto const& elem : mElements) {
                 if (relevantEvents.find(elem->id()) != relevantEvents.end()) {
                     elem->setRelevance(true);
                     elem->setAllowDC(allowDCForRelevantEvents);
+                    mRelevantEvents.insert(elem->id());
                 } else {
                     elem->setRelevance(false);
                     elem->setAllowDC(true);
@@ -876,29 +887,20 @@ 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 mRelevantEvents;
         }
-            return relevantEvents;
-        }
-
 
         template<typename ValueType>
         std::string DFT<ValueType>::getRelevantEventsString() const {
             std::stringstream stream;
             bool first = true;
-            for (auto const& elem : mElements) {
-                if (elem->isRelevant()) {
+            for (size_t relevant_id : getRelevantEvents()) {
                 if (first) {
                     first = false;
                 } else {
                     stream << ", ";
                 }
-                    stream << elem->name() << " [" << elem->id() << "]";
-                }
+                stream << getElement(relevant_id)->name() << " [" << relevant_id << "]";
             }
             return stream.str();
         }
@@ -1000,10 +1002,14 @@ namespace storm {
         }
 
         // Explicitly instantiate the class.
-        template class DFT<double>;
+        template
+        class DFT<double>;
 
 #ifdef STORM_HAVE_CARL
-        template class DFT<RationalFunction>;
+
+        template
+        class DFT<RationalFunction>;
+
 #endif
 
     }

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

@@ -68,6 +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;
 
         public:
             DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
@@ -327,7 +328,7 @@ namespace storm {
 
             /*!
              * 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.
+             * @param relevantEvents All elements which should be to relevant. All elements not occurring are set to irrelevant.
              * @param allowDCForRelevantEvents Flag whether Don't Care propagation is allowed even for relevant events.
              */
             void setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const;

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(), dft.getRelevantEvents()), 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()), 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(), dft.getRelevantEvents()), 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()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
             // Intentionally left empty
         }
         
@@ -87,10 +87,6 @@ namespace storm {
                 }
             }
 
-            // Initialize remaining relevant events
-            failableElements.remainingRelevantEvents = mDft.getRelevantEvents();
-            this->updateRemainingRelevantEvents();
-
             mPseudoState = false;
         }
 
@@ -316,18 +312,6 @@ 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, std::set<size_t> relevantEvents) : currentlyFailableBE(nrElements), remainingRelevantEvents(relevantEvents), it(currentlyFailableBE.begin()) {
+                FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) {
                     // Intentionally left empty
                 }
 
@@ -103,19 +103,10 @@ 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;
@@ -312,11 +303,6 @@ 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