Moved failableBE/Dependencies to own struct

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -387,7 +387,7 @@ namespace storm {
                                     // Initialize heuristic values
                                     ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass());
                                     iter->second.second = heuristic;
-                                    if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) {
+                                    if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && state->getFailableElements().hasBEs())) {
                                         // Do not skip absorbing state or if reached by dependencies
                                         iter->second.second->markExpand();
                                     }
@@ -642,8 +642,8 @@ namespace storm {
         ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
             // Get the lower bound by considering the failure of all possible BEs
             ValueType lowerBound = storm::utility::zero<ValueType>();
-            for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
-                lowerBound += state->getFailableBERate(index);
+            for (state->getFailableElements().init(false); !state->getFailableElements().isEnd(); state->getFailableElements().next()) {
+                lowerBound += state->getBERate(state->getFailableElements().get());
             }
             return lowerBound;
         }

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -51,12 +51,13 @@ namespace storm {
             StateBehavior<ValueType, StateType> result;
 
             // Initialization
-            bool hasDependencies = state->nrFailableDependencies() > 0;
-            size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
-            size_t currentFailable = 0;
+            bool hasDependencies = state->getFailableElements().hasDependencies();
+            //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
+            //size_t currentFailable = 0;
+            state->getFailableElements().init(hasDependencies);
 
             // Check for absorbing state
-            if (mDft.hasFailed(state) || mDft.isFailsafe(state) || failableCount == 0) {
+            if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->getFailableElements().isEnd()) {
                 Choice<ValueType, StateType> choice(0, true);
                 // Add self loop
                 choice.addProbability(state->getId(), storm::utility::one<ValueType>());
@@ -70,16 +71,18 @@ namespace storm {
             Choice<ValueType, StateType> choice(0, !hasDependencies);
 
             // Let BE fail
-            while (currentFailable < failableCount) {
-                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
+            bool isFirst = true;
+            while (!state->getFailableElements().isEnd()) {
+                if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && hasDependencies && !isFirst) {
                     // 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
                 DFTStatePointer newState = state->copy();
-                std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(currentFailable);
+                std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get());
                 std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
                 STORM_LOG_ASSERT(nextBE, "NextBE is null.");
                 STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
@@ -114,7 +117,7 @@ namespace storm {
 
                 if(newState->isInvalid() || (nextBE->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex()))) {
                     // Continue with next possible state
-                    ++currentFailable;
+                    state->getFailableElements().next();
                     STORM_LOG_TRACE("State is ignored because " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored"));
                     continue;
                 }
@@ -148,14 +151,14 @@ namespace storm {
                 // Set transitions
                 if (hasDependencies) {
                     // Failure is due to dependency -> add non-deterministic choice
-                    ValueType probability = mDft.getDependency(state->getDependencyId(currentFailable))->probability();
+                    ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability();
                     choice.addProbability(newStateId, probability);
                     STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability);
 
                     if (!storm::utility::isOne(probability)) {
                         // Add transition to state where dependency was unsuccessful
                         DFTStatePointer unsuccessfulState = state->copy();
-                        unsuccessfulState->letDependencyBeUnsuccessful(currentFailable);
+                        unsuccessfulState->letDependencyBeUnsuccessful(state->getFailableElements().get());
                         // Add state
                         StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState);
                         ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
@@ -179,7 +182,7 @@ namespace storm {
                 }
                 STORM_LOG_ASSERT(newStateId != state->getId(), "Self loop was added for " << newStateId << " and failure of " << nextBE->name());
 
-                ++currentFailable;
+                state->getFailableElements().next();
             } // end while failing BE
             
             if (!hasDependencies) {

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

@@ -6,7 +6,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), 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 Matthias: use construct()
             
             // Initialize uses
@@ -20,12 +20,14 @@ namespace storm {
             // Initialize activation
             propagateActivation(mDft.getTopLevelIndex());
 
-            std::vector<size_t> alwaysActiveBEs = mDft.nonColdBEs();
-            mCurrentlyFailableBE.insert(mCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
+            // Initialize currently failable BEs
+            for (size_t id : mDft.nonColdBEs()) {
+                failableElements.addBE(id);
+            }
         }
 
         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), 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
         }
         
@@ -33,8 +35,7 @@ namespace storm {
         void DFTState<ValueType>::construct() {
             STORM_LOG_TRACE("Construct concrete state from pseudo state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId));
             // Clear information from pseudo state
-            mCurrentlyFailableBE.clear();
-            mFailableDependencies.clear();
+            failableElements.clear();
             mUsedRepresentants.clear();
             STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed.");
             for(size_t index = 0; index < mDft.nrElements(); ++index) {
@@ -42,7 +43,7 @@ namespace storm {
                 if (mDft.isBasicElement(index) && isOperational(index)) {
                     std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(index);
                     if (be->canFail() && (!be->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)))) {
-                        mCurrentlyFailableBE.push_back(index);
+                        failableElements.addBE(index);
                         STORM_LOG_TRACE("Currently failable: " << be->toString());
                     }
                 } else if (mDft.getElement(index)->isSpareGate()) {
@@ -59,7 +60,7 @@ namespace storm {
                 STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match.");
                 assert(dependency->dependentEvents().size() == 1);
                 if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
-                    mFailableDependencies.push_back(dependencyId);
+                    failableElements.addDependency(dependencyId);
                     STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
                 }
             }
@@ -185,10 +186,7 @@ namespace storm {
 
         template<typename ValueType>
         void DFTState<ValueType>::beNoLongerFailable(size_t id) {
-            auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id);
-            if (it != mCurrentlyFailableBE.end()) {
-                mCurrentlyFailableBE.erase(it);
-            }
+            failableElements.removeBE(id);
         }
 
         template<typename ValueType>
@@ -202,13 +200,11 @@ namespace storm {
                 assert(dependency->dependentEvents().size() == 1);
                 if (getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
                     STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe.");
-                    if (std::find(mFailableDependencies.begin(), mFailableDependencies.end(), dependency->id()) == mFailableDependencies.end()) {
-                        mFailableDependencies.push_back(dependency->id());
-                        STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
-                    }
+                    failableElements.addDependency(dependency->id());
+                    STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
                 }
             }
-            return nrFailableDependencies() > 0;
+            return failableElements.hasDependencies();
         }
         
         template<typename ValueType>
@@ -237,43 +233,35 @@ namespace storm {
         }
 
         template<typename ValueType>
-        ValueType DFTState<ValueType>::getFailableBERate(size_t index) const {
-            STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid.");
-            return getBERate(mCurrentlyFailableBE[index]);
-        }
-
-        template<typename ValueType>
-        std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> DFTState<ValueType>::letNextBEFail(size_t index) {
+        std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> DFTState<ValueType>::letNextBEFail(size_t id) {
             STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
-            if (nrFailableDependencies() > 0) {
+            if (failableElements.hasDependencies()) {
                 // Consider failure due to dependency
-                STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
-                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
-                assert(dependency->dependentEvents().size() == 1);
+                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(id);
+                STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event");
                 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);
+                failableElements.removeDependency(id);
                 setFailed(res.first->id());
                 setDependencySuccessful(dependency->id());
                 beNoLongerFailable(res.first->id());
                 return res;
             } else {
                 // 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);
+                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(id), 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);
+                failableElements.removeBE(id);
                 setFailed(res.first->id());
                 return res;
             }
         }
  
         template<typename ValueType>
-        void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t index) {
-            STORM_LOG_ASSERT(nrFailableDependencies() > 0 && index < nrFailableDependencies(), "Index invalid.");
-            std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
-            mFailableDependencies.erase(mFailableDependencies.begin() + index);
+        void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t id) {
+            STORM_LOG_ASSERT(failableElements.hasDependencies(), "Index invalid.");
+            std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(id);
+            failableElements.removeDependency(id);
             setDependencyUnsuccessful(dependency->id());
         }
 
@@ -299,7 +287,7 @@ namespace storm {
                     std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(elem);
                     if (be->isColdBasicElement() && be->canFail()) {
                         // Add to failable BEs
-                        mCurrentlyFailableBE.push_back(elem);
+                        failableElements.addBE(elem);
                     }
                 } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
                     propagateActivation(uses(elem));

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

@@ -22,12 +22,102 @@ namespace storm {
         template<typename ValueType>
         class DFTState {
             friend struct std::hash<DFTState>;
+
+            struct FailableElements {
+
+                FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) {
+                    // Intentionally left empty
+                }
+
+                void addBE(size_t id) {
+                    currentlyFailableBE.set(id);
+                }
+
+                void addDependency(size_t id) {
+                    if (std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id) == mFailableDependencies.end()) {
+                        mFailableDependencies.push_back(id);
+                    }
+                }
+
+                void removeBE(size_t id) {
+                    currentlyFailableBE.set(id, false);
+                }
+
+                void removeDependency(size_t id) {
+                    auto it = std::find(mFailableDependencies.begin(), mFailableDependencies.end(), id);
+                    if (it != mFailableDependencies.end()) {
+                        mFailableDependencies.erase(it);
+                    }
+                }
+
+                void clear() {
+                    currentlyFailableBE.clear();
+                    mFailableDependencies.clear();
+                }
+
+                void init(bool dependency) const {
+                    this->dependency = dependency;
+                    if (this->dependency) {
+                        itDep = mFailableDependencies.begin();
+                    } else {
+                        it = currentlyFailableBE.begin();
+                    }
+                }
+
+                /**
+                 * Increment iterator.
+                 */
+                void next() const {
+                    if (dependency) {
+                        ++itDep;
+                    } else {
+                        ++it;
+                    }
+                }
+
+                bool isEnd() const {
+                    if (dependency) {
+                        return itDep == mFailableDependencies.end();
+                    } else {
+                        return it == currentlyFailableBE.end();
+                    }
+                }
+
+                /**
+                 * Get underlying element of iterator.
+                 * @return Id of element.
+                 */
+                size_t get() const {
+                    if (dependency) {
+                        return *itDep;
+                    } else {
+                        return *it;
+                    }
+                };
+
+                bool hasDependencies() const {
+                    return !mFailableDependencies.empty();
+                }
+
+                bool hasBEs() const {
+                    return !currentlyFailableBE.empty();
+                }
+
+                mutable bool dependency;
+
+                storm::storage::BitVector currentlyFailableBE;
+                std::vector<size_t> mFailableDependencies;
+
+                mutable storm::storage::BitVector::const_iterator it;
+                mutable std::vector<size_t>::const_iterator itDep;
+            };
+
+
         private:
             // Status is bitvector where each element has two bits with the meaning according to DFTElementState
             storm::storage::BitVector mStatus;
             size_t mId;
-            std::vector<size_t> mCurrentlyFailableBE;
-            std::vector<size_t> mFailableDependencies;
+            FailableElements failableElements;
             std::vector<size_t> mUsedRepresentants;
             bool mPseudoState;
             bool mValid = true;
@@ -125,6 +215,10 @@ namespace storm {
                 return mStatus;
             }
 
+            FailableElements& getFailableElements() {
+                return failableElements;
+            }
+           
             /**
              * This method returns the id of the used child for a spare. If no element is used, it returns the given id.
              * @param id Id of the spare
@@ -171,15 +265,6 @@ namespace storm {
              */
             bool claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children);
 
-            /**
-             * Get number of currently failable BEs.
-             *
-             * @return Number of failable BEs.
-             */
-            size_t nrFailableBEs() const {
-                return mCurrentlyFailableBE.size();
-            }
-
             /**
              * Get the failure rate of the currently failable BE on the given index.
              *
@@ -198,24 +283,6 @@ namespace storm {
              */
             ValueType getBERate(size_t id) const;
 
-            /** Get number of currently failable dependencies.
-             *
-             * @return Number of failable dependencies.
-             */
-            size_t nrFailableDependencies() const {
-                return mFailableDependencies.size();
-            }
-            
-            /**
-             * Gets the id of the dependency at index in the list of failable dependencies.
-             * @param index Index in list of failable dependencies.
-             * @return Id of the dependency
-             */
-            size_t getDependencyId(size_t index) const {
-                STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
-                return mFailableDependencies[index];
-            }
-
             /**
              * Sets all failable BEs due to dependencies from newly failed element
              * @param id Id of the newly failed element
@@ -257,28 +324,26 @@ namespace storm {
             
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;
-                if (nrFailableDependencies() > 0) {
-                    auto it = mFailableDependencies.begin();
+                if (failableElements.hasDependencies()) {
+                    failableElements.init(true);
                     stream << "{Dependencies: ";
-                    if (it != mFailableDependencies.end()) {
-                        stream << *it;
-                    }
-                    ++it;
-                    while(it != mFailableDependencies.end()) {
-                        stream << ", " << *it;
-                        ++it;
+                    stream << failableElements.get();
+                    failableElements.next();
+                    while(!failableElements.isEnd()) {
+                        stream << ", " << failableElements.get();
+                        failableElements.next();
                     }
                     stream << "} ";
                 } else {
-                    auto it = mCurrentlyFailableBE.begin();
+                    failableElements.init(false);
                     stream << "{";
-                    if(it != mCurrentlyFailableBE.end()) {
-                        stream << *it;
-                    }
-                    ++it;
-                    while(it != mCurrentlyFailableBE.end()) {
-                        stream << ", " << *it;
-                        ++it;
+                    if (!failableElements.isEnd()) {
+                        stream << failableElements.get();
+                        failableElements.next();
+                        while (!failableElements.isEnd()) {
+                            stream << ", " << failableElements.get();
+                            failableElements.next();
+                        }
                     }
                     stream << "}";
                 }