diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 13628a7ff..3ecc69498 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -743,8 +743,9 @@ namespace storm { ValueType ExplicitDFTModelBuilder::getLowerBound(DFTStatePointer const& state) const { // Get the lower bound by considering the failure of all possible BEs ValueType lowerBound = storm::utility::zero(); - for (state->getFailableElements().init(false); !state->getFailableElements().isEnd(); state->getFailableElements().next()) { - lowerBound += state->getBERate(state->getFailableElements().get()); + STORM_LOG_ASSERT(!state->getFailableElements().hasDependencies(), "Lower bound should only be computed if dependencies were already handled."); + for (auto it = state->getFailableElements().begin(); it != state->getFailableElements().end(); ++it) { + lowerBound += state->getBERate(*it); } STORM_LOG_TRACE("Lower bound is " << lowerBound << " for state " << state->getId()); return lowerBound; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index ab49cad13..7d4894284 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -41,7 +41,7 @@ namespace storm { // Register initial state id = stateToIdCallback(initialState); } else { - initialState->letNextBEFail(constFailedBE->id(), false); + initialState->letBEFail(constFailedBE, nullptr); // Propagate the constant failure to reach the real initial state storm::storage::DFTStateSpaceGenerationQueues queues; propagateFailure(initialState, constFailedBE, queues); @@ -99,14 +99,16 @@ namespace storm { // Prepare the result, in case we return early. StateBehavior result; + STORM_LOG_TRACE("Currently failable: " << state->getFailableElements().getCurrentlyFailableString()); //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); //size_t currentFailable = 0; - state->getFailableElements().init(exploreDependencies); + // TODO remove exploreDependencies + auto iterFailable = state->getFailableElements().begin(!exploreDependencies); // Check for absorbing state: // - either no relevant event remains (i.e., all relevant events have failed already), or // - no BE can fail - if (!state->hasOperationalRelevantEvent() || state->getFailableElements().isEnd()) { + if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end(!exploreDependencies)) { Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); @@ -120,55 +122,29 @@ namespace storm { Choice choice(0, !exploreDependencies); // Let BE fail - bool isFirst = true; - while (!state->getFailableElements().isEnd()) { - //TODO outside - if (takeFirstDependency && exploreDependencies && !isFirst) { - // We discard further exploration as we already chose one dependent event - break; - } - isFirst = false; - - // Construct new state as copy from original one - DFTStatePointer newState = state->copy(); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get(), exploreDependencies); - std::shared_ptr const>& nextBE = nextBEPair.first; + for (; iterFailable != state->getFailableElements().end(!exploreDependencies); ++iterFailable) { + // Get BE which fails next + std::pair const>, std::shared_ptr const>> nextBEPair = iterFailable.getFailBE(mDft); + std::shared_ptr const> nextBE = nextBEPair.first; + std::shared_ptr const> dependency = nextBEPair.second; STORM_LOG_ASSERT(nextBE, "NextBE is null."); - STORM_LOG_ASSERT(nextBEPair.second == exploreDependencies, "Failure due to dependencies does not match."); - STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state)); + STORM_LOG_ASSERT(iterFailable.isFailureDueToDependency() == exploreDependencies, "Failure due to dependencies does not match."); + STORM_LOG_ASSERT((dependency != nullptr) == exploreDependencies, "Failure due to dependencies does not match."); - // Propagate - storm::storage::DFTStateSpaceGenerationQueues queues; - - propagateFailure(newState, nextBE, queues); - - bool transient = false; - // TODO handle for all types of BEs. - if (nextBE->beType() == storm::storage::BEType::EXPONENTIAL) { - auto beExp = std::static_pointer_cast const>(nextBE); - transient = beExp->isTransient(); - } + // Obtain successor state by propagating failure + DFTStatePointer newState = createSuccessorState(state, nextBE, dependency); - if(newState->isInvalid() || (transient && !newState->hasFailed(mDft.getTopLevelIndex()))) { - // Continue with next possible state - state->getFailableElements().next(); + if(newState->isInvalid() || newState->isTransient()) { STORM_LOG_TRACE("State is ignored because " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); + // Continue with next possible state continue; } - // Get the id of the successor state StateType newStateId; if (newState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) { // Use unique failed state newStateId = 0; } else { - propagateFailsafe(newState, nextBE, queues); - - // Update failable dependencies - newState->updateFailableDependencies(nextBE->id()); - newState->updateDontCareDependencies(nextBE->id()); - newState->updateFailableInRestrictions(nextBE->id()); - // Add new state newStateId = stateToIdCallback(newState); } @@ -176,14 +152,14 @@ namespace storm { // Set transitions if (exploreDependencies) { // Failure is due to dependency -> add non-deterministic choice if necessary - ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability(); + ValueType probability = mDft.getDependency(*iterFailable)->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(state->getFailableElements().get()); + unsuccessfulState->letDependencyBeUnsuccessful(*iterFailable); // Add state StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState); ValueType remainingProbability = storm::utility::one() - probability; @@ -195,22 +171,23 @@ namespace storm { } else { // Failure is due to "normal" BE failure // Set failure rate according to activation - STORM_LOG_THROW(nextBE->beType() == storm::storage::BEType::EXPONENTIAL, storm::exceptions::NotSupportedException, "BE of type '" << nextBE->type() << "' is not supported."); - auto beExp = std::static_pointer_cast const>(nextBE); - bool isActive = true; - if (mDft.hasRepresentant(beExp->id())) { - // Active must be checked for the state we are coming from as this state is responsible for the rate - isActive = state->isActive(mDft.getRepresentant(beExp->id())); - } - ValueType rate = isActive ? beExp->activeFailureRate() : beExp->passiveFailureRate(); + ValueType rate = state->getBERate(nextBE->id()); STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); choice.addProbability(newStateId, rate); - STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate); + STORM_LOG_TRACE("Added transition to " << newStateId << " with failure rate " << rate); } STORM_LOG_ASSERT(newStateId != state->getId(), "Self loop was added for " << newStateId << " and failure of " << nextBE->name()); - state->getFailableElements().next(); - } // end while failing BE + // Handle premature stop for dependencies + if (iterFailable.isFailureDueToDependency() && !iterFailable.isConflictingDependency()) { + // We only explore the first non-conflicting dependency because we can fix an order. + break; + } + if (takeFirstDependency && exploreDependencies) { + // We discard further exploration as we already chose one dependent event + break; + } + } // end iteration of failing BE if (exploreDependencies) { if (result.empty()) { @@ -236,6 +213,46 @@ namespace storm { return result; } + template + typename DftNextStateGenerator::DFTStatePointer DftNextStateGenerator::createSuccessorState(DFTStatePointer const state, std::shared_ptr const>& failedBE, std::shared_ptr const>& triggeringDependency) { + // Construct new state as copy from original one + DFTStatePointer newState = state->copy(); + STORM_LOG_TRACE("With the failure of: " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state)); + + newState->letBEFail(failedBE, triggeringDependency); + + // Propagate + storm::storage::DFTStateSpaceGenerationQueues queues; + propagateFailure(newState, failedBE, queues); + + // Check whether transient failure lead to TLE failure + // TODO handle for all types of BEs. + if (failedBE->beType() == storm::storage::BEType::EXPONENTIAL) { + auto beExp = std::static_pointer_cast const>(failedBE); + if (beExp->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex())) { + newState->markAsTransient(); + } + } + + // Check whether fail safe propagation can be discarded + bool discardFailSafe = false; + discardFailSafe |= newState->isInvalid(); + discardFailSafe |= newState->isTransient(); + discardFailSafe |= (newState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState); + + // Propagate fail safe (if necessary) + if (!discardFailSafe) { + propagateFailsafe(newState, failedBE, queues); + + // Update failable dependencies + newState->updateFailableDependencies(failedBE->id()); + newState->updateDontCareDependencies(failedBE->id()); + newState->updateFailableInRestrictions(failedBE->id()); + } + return newState; + } + + template void DftNextStateGenerator::propagateFailure(DFTStatePointer newState, std::shared_ptr const> &nextBE, @@ -265,7 +282,6 @@ namespace storm { newState->updateFailableDependencies(next->id()); newState->updateFailableInRestrictions(next->id()); } - } template diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 1e912655f..afac7041f 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -48,6 +48,17 @@ namespace storm { */ StateBehavior createMergeFailedState(StateToIdCallback const& stateToIdCallback); + /*! + * Create successor state from given state by letting the given BE fail next. + * + * @param state Current state. + * @param failedBE BE which fails next. + * @param triggeringDependency Dependency which triggered the failure (or nullptr if BE failed on its own). + * + * @return Successor state. + */ + DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr const> &failedBE, std::shared_ptr const> &triggeringDependency); + /** * Propagate the failures in a given state if the given BE fails * diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 4be919435..6c58b0923 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -51,14 +51,14 @@ namespace storm { if (be->canFail()) { switch (be->beType()) { case storm::storage::BEType::CONSTANT: - failableElements.addBE(index); + failableElements.addBE(be->id()); STORM_LOG_TRACE("Currently failable: " << *be); break; case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); if (!beExp->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { - failableElements.addBE(index); + failableElements.addBE(be->id()); STORM_LOG_TRACE("Currently failable: " << *beExp); } break; @@ -327,28 +327,19 @@ namespace storm { } template - std::pair const>, bool> DFTState::letNextBEFail(size_t id, bool dueToDependency) { - STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - if (dueToDependency) { + void DFTState::letBEFail(std::shared_ptr const> be, std::shared_ptr const> dependency) { + STORM_LOG_ASSERT(!hasFailed(be->id()), "Element " << *be << " has already failed."); + if (dependency != nullptr) { // Consider failure due to dependency - std::shared_ptr const> dependency = mDft.getDependency(id); - STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); - std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true); - STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << *(res.first) << " has already failed."); - failableElements.removeDependency(id); - setFailed(res.first->id()); + failableElements.removeDependency(dependency->id()); setDependencySuccessful(dependency->id()); - beNoLongerFailable(res.first->id()); - return res; } else { // Consider "normal" failure - std::pair const>,bool> res(mDft.getBasicElement(id), false); - STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << *(res.first) << " has already failed."); - STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail."); - failableElements.removeBE(id); - setFailed(res.first->id()); - return res; + STORM_LOG_ASSERT(be->canFail(), "Element " << *be << " cannot fail."); } + // Set BE as failed + setFailed(be->id()); + failableElements.removeBE(be->id()); } template diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 9ebe12dba..72774d166 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -1,11 +1,11 @@ #pragma once -#include #include #include "storm/storage/BitVector.h" #include "storm-dft/storage/dft/DFTElementState.h" +#include "storm-dft/storage/dft/FailableElements.h" #include "storm-dft/builder/DftExplorationHeuristic.h" namespace storm { @@ -16,6 +16,8 @@ namespace storm { template class DFTBE; template + class DFTDependency; + template class DFTElement; class DFTStateGenerationInfo; @@ -23,137 +25,16 @@ namespace storm { class DFTState { friend struct std::hash; - 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, bool isConflicting) { - if (isConflicting) { - if (std::find(mFailableConflictingDependencies.begin(), mFailableConflictingDependencies.end(), - id) == mFailableConflictingDependencies.end()) { - mFailableConflictingDependencies.push_back(id); - } - } else { - if (std::find(mFailableNonconflictingDependencies.begin(), - mFailableNonconflictingDependencies.end(), id) == - mFailableNonconflictingDependencies.end()) { - mFailableNonconflictingDependencies.push_back(id); - } - } - } - - void removeBE(size_t id) { - currentlyFailableBE.set(id, false); - } - - void removeDependency(size_t id) { - auto it1 = std::find(mFailableConflictingDependencies.begin(), - mFailableConflictingDependencies.end(), id); - if (it1 != mFailableConflictingDependencies.end()) { - mFailableConflictingDependencies.erase(it1); - return; - } - auto it2 = std::find(mFailableNonconflictingDependencies.begin(), - mFailableNonconflictingDependencies.end(), id); - if (it2 != mFailableNonconflictingDependencies.end()) { - mFailableNonconflictingDependencies.erase(it2); - return; - } - } - - void clear() { - currentlyFailableBE.clear(); - mFailableConflictingDependencies.clear(); - mFailableNonconflictingDependencies.clear(); - } - - void init(bool dependency) const { - this->dependency = dependency; - if (this->dependency) { - if (!mFailableNonconflictingDependencies.empty()) { - itDep = mFailableNonconflictingDependencies.begin(); - conflicting = false; - } else { - itDep = mFailableConflictingDependencies.begin(); - conflicting = true; - } - } else { - it = currentlyFailableBE.begin(); - } - } - - /** - * Increment iterator. - */ - void next() const { - if (dependency) { - ++itDep; - } else { - ++it; - } - } - - bool isEnd() const { - if (dependency) { - if (!conflicting) { - // If we are handling the non-conflicting FDEPs, end after the first element - return itDep != mFailableNonconflictingDependencies.begin(); - } else { - return itDep == mFailableConflictingDependencies.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 !mFailableConflictingDependencies.empty() || !mFailableNonconflictingDependencies.empty(); - } - - bool hasBEs() const { - return !currentlyFailableBE.empty(); - } - - mutable bool dependency; - mutable bool conflicting; - - storm::storage::BitVector currentlyFailableBE; - std::vector mFailableConflictingDependencies; - std::vector mFailableNonconflictingDependencies; - std::set remainingRelevantEvents; - - mutable storm::storage::BitVector::const_iterator it; - mutable std::vector::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; - FailableElements failableElements; + storm::dft::storage::FailableElements failableElements; std::vector mUsedRepresentants; size_t indexRelevant; bool mPseudoState; bool mValid = true; + bool mTransient = false; const DFT& mDft; const DFTStateGenerationInfo& mStateGenerationInfo; @@ -240,6 +121,14 @@ namespace storm { return !mValid; } + void markAsTransient() { + mTransient = true; + } + + bool isTransient() const { + return mTransient; + } + bool isPseudoState() const { return mPseudoState; } @@ -248,7 +137,7 @@ namespace storm { return mStatus; } - FailableElements& getFailableElements() { + storm::dft::storage::FailableElements& getFailableElements() { return failableElements; } @@ -348,12 +237,13 @@ namespace storm { void updateDontCareDependencies(size_t id); /** - * Sets the next BE as failed - * @param index Index in currentlyFailableBE of BE to fail - * @param dueToDependency Whether the failure is due to a dependency. - * @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies + * Sets the next BE as failed. + * Optionally also marks the triggering dependency as successful. + * + * @param be BE to fail. + * @param dependency Dependency which triggered the failure (or nullptr if the BE fails on its own). */ - std::pair const>, bool> letNextBEFail(size_t index, bool dueToDependency); + void letBEFail(std::shared_ptr const> be, std::shared_ptr const> dependency); /** * Sets the dependency as unsuccesful meaning no BE will fail. @@ -386,34 +276,6 @@ namespace storm { * @return True iff one operational relevant event exists. */ bool hasOperationalRelevantEvent(); - - std::string getCurrentlyFailableString() const { - std::stringstream stream; - if (failableElements.hasDependencies()) { - failableElements.init(true); - stream << "{Dependencies: "; - stream << failableElements.get(); - failableElements.next(); - while(!failableElements.isEnd()) { - stream << ", " << failableElements.get(); - failableElements.next(); - } - stream << "} "; - } else { - failableElements.init(false); - stream << "{"; - if (!failableElements.isEnd()) { - stream << failableElements.get(); - failableElements.next(); - while (!failableElements.isEnd()) { - stream << ", " << failableElements.get(); - failableElements.next(); - } - } - stream << "}"; - } - return stream.str(); - } friend bool operator==(DFTState const& a, DFTState const& b) { return a.mStatus == b.mStatus; diff --git a/src/storm-dft/storage/dft/FailableElements.cpp b/src/storm-dft/storage/dft/FailableElements.cpp new file mode 100644 index 000000000..66a268bfc --- /dev/null +++ b/src/storm-dft/storage/dft/FailableElements.cpp @@ -0,0 +1,163 @@ +#include "storm-dft/storage/dft/FailableElements.h" + +#include + +#include "storm-dft/storage/dft/DFT.h" + +namespace storm { + namespace dft { + namespace storage { + + FailableElements::const_iterator::const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE, std::list::const_iterator const& iterDependency, std::list::const_iterator nonConflictEnd, std::list::const_iterator conflictBegin) + : dependency(dependency), conflicting(conflicting), itBE(iterBE), itDep(iterDependency), nonConflictEnd(nonConflictEnd), conflictBegin(conflictBegin) { + STORM_LOG_ASSERT(conflicting || itDep != nonConflictEnd, "No non-conflicting dependencies present."); + } + + FailableElements::const_iterator& FailableElements::const_iterator::operator++() { + if (dependency) { + ++itDep; + if (!conflicting && itDep == nonConflictEnd) { + // All non-conflicting dependencies considered -> start with conflicting ones + conflicting = true; + itDep = conflictBegin; + } + } else { + ++itBE; + } + return *this; + } + + uint_fast64_t FailableElements::const_iterator::operator*() const { + if (dependency) { + return *itDep; + } else { + return *itBE; + } + } + + bool FailableElements::const_iterator::operator!=(const_iterator const& other) const { + if (dependency != other.dependency || conflicting != other.conflicting) { + return true; + } + if (dependency) { + return itDep != other.itDep; + } else { + return itBE != other.itBE; + } + } + + bool FailableElements::const_iterator::operator==(const_iterator const& other) const { + if (dependency != other.dependency || conflicting != other.conflicting) { + return false; + } + if (dependency) { + return itDep == other.itDep; + } else { + return itBE == other.itBE; + } + } + + bool FailableElements::const_iterator::isFailureDueToDependency() const { + return dependency; + } + + bool FailableElements::const_iterator::isConflictingDependency() const { + return conflicting; + } + + template + std::pair const>, std::shared_ptr const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT const& dft) const { + size_t nextFailId = **this; + if (isFailureDueToDependency()) { + // Consider failure due to dependency + std::shared_ptr const> dependency = dft.getDependency(nextFailId); + STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); + return std::make_pair(dft.getBasicElement(dependency->dependentEvents()[0]->id()), dependency); + } else { + // Consider "normal" failure + return std::make_pair(dft.getBasicElement(nextFailId), nullptr); + } + } + + void FailableElements::addBE(size_t id) { + currentlyFailableBE.set(id); + } + + void FailableElements::addDependency(size_t id, bool isConflicting) { + std::list& failableList = (isConflicting ? failableConflictingDependencies : failableNonconflictingDependencies); + for (auto it = failableList.begin(); it != failableList.end(); ++it) { + if (*it > id) { + failableList.insert(it, id); + return; + } else if (*it == id) { + // Dependency already contained + return; + } + } + failableList.push_back(id); + } + + void FailableElements::removeBE(size_t id) { + currentlyFailableBE.set(id, false); + } + + void FailableElements::removeDependency(size_t id) { + auto iter = std::find(failableConflictingDependencies.begin(), failableConflictingDependencies.end(), id); + if (iter != failableConflictingDependencies.end()) { + failableConflictingDependencies.erase(iter); + return; + } + iter = std::find(failableNonconflictingDependencies.begin(), failableNonconflictingDependencies.end(), id); + if (iter != failableNonconflictingDependencies.end()) { + failableNonconflictingDependencies.erase(iter); + return; + } + } + + void FailableElements::clear() { + currentlyFailableBE.clear(); + failableConflictingDependencies.clear(); + failableNonconflictingDependencies.clear(); + } + + FailableElements::const_iterator FailableElements::begin(bool forceBE) const { + bool dependency = hasDependencies() && !forceBE; + bool conflicting = failableNonconflictingDependencies.empty(); + auto itDep = conflicting ? failableConflictingDependencies.begin() : failableNonconflictingDependencies.begin(); + return FailableElements::const_iterator(dependency, conflicting, currentlyFailableBE.begin(), itDep, failableNonconflictingDependencies.end(), failableConflictingDependencies.begin()); + } + + FailableElements::const_iterator FailableElements::end(bool forceBE) const { + bool dependency = hasDependencies() && !forceBE; + return FailableElements::const_iterator(dependency, true, currentlyFailableBE.end(), failableConflictingDependencies.end(), failableNonconflictingDependencies.end(), failableConflictingDependencies.begin()); + } + + bool FailableElements::hasDependencies() const { + return !failableConflictingDependencies.empty() || !failableNonconflictingDependencies.empty(); + } + + bool FailableElements::hasBEs() const { + return !currentlyFailableBE.empty(); + } + + std::string FailableElements::getCurrentlyFailableString() const { + std::stringstream stream; + stream << "{"; + if (hasDependencies()) { + stream << "Dependencies: "; + } + for (auto it = begin(); it != end(); ++it) { + stream << *it << ", "; + } + stream << "}"; + return stream.str(); + } + + // Explicit instantiations. + template std::pair const>, std::shared_ptr const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT const& dft) const; + + template std::pair const>, std::shared_ptr const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT const& dft) const; + + } // namespace storage + } // namespace dft +} // namespace storm \ No newline at end of file diff --git a/src/storm-dft/storage/dft/FailableElements.h b/src/storm-dft/storage/dft/FailableElements.h new file mode 100644 index 000000000..5e048f6df --- /dev/null +++ b/src/storm-dft/storage/dft/FailableElements.h @@ -0,0 +1,241 @@ +#pragma once + +#include +#include + +#include "storm/storage/BitVector.h" + +namespace storm { + namespace storage { + // Forward declarations + template + class DFT; + template + class DFTBE; + template + class DFTDependency; + } + + namespace dft { + namespace storage { + + /*! + * Handling of currently failable elements (BEs) either due to their own failure or because of dependencies. + * + * We distinguish between failures of BEs and failures of dependencies. + * For dependencies, we further distinguish between non-conflicting and conflicting dependencies. + * Non-conflicting dependencies will lead to spurious non-determinsm. + * + * The class supports iterators for all failable elements (either BE or dependencies). + * + */ + class FailableElements { + + public: + /*! + * Iterator for failable elements. + * + */ + class const_iterator : public std::iterator { + + public: + /*! + * Construct a new iterator. + * We either iterate over all failable BEs or over all dependencies (if dependency is true). + * For dependencies, we start with non-conflicting dependencies before iterating over conflicting ones. + * For dependencies, we start with non-conflicting dependencies if they are present. + * + * @param dependency Whether dependencies should be iterated (or BEs if false). + * @param conflicting Whether conflicting dependencies should be iterated (or non-conflicting if false). + * @param iterBE Iterator for BEs. + * @param iterDependency Iterator for Dependencies. + * @param nonConflictEnd Iterator to end of non-conflicting dependencies. + * @param conflictBegin Iterator to begin of conflicting dependencies. + */ + const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE, std::list::const_iterator const& iterDependency, std::list::const_iterator nonConflictEnd, std::list::const_iterator conflictBegin); + + /*! + * Constructs an iterator by copying the given iterator. + * + * @param other The iterator to copy. + */ + const_iterator(const_iterator const& other) = default; + + /*! + * Assigns the contents of the given iterator to the current one via copying the former's contents. + * + * @param other The iterator from which to copy-assign. + */ + const_iterator& operator=(const_iterator const& other) = default; + + /*! + * Increment the iterator. + * + * @return A reference to this iterator. + */ + const_iterator& operator++(); + + /*! + * Returns the id of the current failable element. + * + * @return Element id. + */ + uint_fast64_t operator*() const; + + /*! + * Compares the iterator with another iterator for inequality. + * + * @param other The iterator with respect to which inequality is checked. + * @return True if the two iterators are unequal. + */ + bool operator!=(const_iterator const& other) const; + + /*! + * Compares the iterator with another iterator for equality. + * + * @param other The iterator with respect to which equality is checked. + * @return True if the two iterators are equal. + */ + bool operator==(const_iterator const& other) const; + + /*! + * Return whether the current failure is due to a dependency (or the BE itself). + * + * @return true iff current failure is due to dependency. + */ + bool isFailureDueToDependency() const; + + /*! + * Return whether the current dependency failure is conflicting. + * + * @return true iff current dependency failure is conflicting. + */ + bool isConflictingDependency() const; + + /*! + * Obtain the BE which fails from the current iterator. + * Optionally returns the dependency which triggered the BE failure. + * + * @tparam ValueType Value type. + * @param dft DFT. + * @return Pair of the BE which fails and the dependency which triggered the failure (or nullptr if the BE fails on its own). + */ + template + std::pair const>, std::shared_ptr const>> getFailBE(storm::storage::DFT const& dft) const; + + private: + // Whether dependencies are currently considered. + bool dependency; + // Whether the iterator currently points to a conflicting dependency. + bool conflicting; + // Iterators for underlying data structures + storm::storage::BitVector::const_iterator itBE; + std::list::const_iterator itDep; + + // Pointers marking end of non-conflict list and beginning of conflict list + // Used for sequential iteration over all dependencies + std::list::const_iterator nonConflictEnd; + std::list::const_iterator conflictBegin; + }; + + /*! + * Creator. + * + * @param maxBEId Maximal id of a BE. + */ + FailableElements(size_t maxBEId) : currentlyFailableBE(maxBEId) { + } + + /*! + * Add failable BE. + * Note that this invalidates the iterator. + * + * @param id Id of BE. + */ + void addBE(size_t id); + + /*! + * Add failable dependency. + * Note that this invalidates the iterator. + * + * @param id Id of dependency. + * @param isConflicting Whether the dependency is in conflict to other dependencies. In this case + * the conflict needs to be resolved non-deterministically. + */ + void addDependency(size_t id, bool isConflicting); + + /*! + * Remove BE from list of failable elements. + * Note that this invalidates the iterator. + * + * @param id Id of BE. + */ + void removeBE(size_t id); + + /*! + * Remove dependency from list of failable elements. + * Note that this invalidates the iterator. + * + * @param id Id of dependency. + */ + void removeDependency(size_t id); + + /*! + * Clear list of currently failable elements. + * Note that this invalidates the iterator. + */ + void clear(); + + /*! + * Iterator to first failable element. + * If dependencies are present, the iterator is for dependencies. Otherwise it is for BEs. + * For dependencies, the iterator considers non-conflicting dependencies first. + * + * @param forceBE If true, failable dependencies are ignored and only BEs are considered. + * @return Iterator. + */ + FailableElements::const_iterator begin(bool forceBE = false) const; + + /*! + * Iterator after last failable element. + * + * @param forceBE If true, failable dependencies are ignored and only BEs are considered. + * @return Iterator. + */ + FailableElements::const_iterator end(bool forceBE = false) const; + + /*! + * Whether failable dependencies are present. + * + * @return true iff dependencies can fail. + */ + bool hasDependencies() const; + + /*! + * Whether failable BEs are present. + * + * @return true iff BEs can fail. + */ + bool hasBEs() const; + + /*! + * Get a string representation of the currently failable elements. + * + * @return std::string Enumeration of currently failable elements. + */ + std::string getCurrentlyFailableString() const; + + private: + + // We use a BitVector for BEs but a list for dependencies, because usually only a few dependencies are failable at the same time. + // In contrast, usually most BEs are failable. + // The lists of failable elements are sorted by increasing id. + storm::storage::BitVector currentlyFailableBE; + std::list failableConflictingDependencies; + std::list failableNonconflictingDependencies; + + }; + + } // namespace storage + } // namespace dft +} // namespace storm \ No newline at end of file