diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 1e9a53045..253e0e0a2 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -105,6 +105,7 @@ namespace storm { DFTGatePointer next = queues.nextFailurePropagation(); next->checkFails(*newState, queues); newState->updateFailableDependencies(next->id()); + newState->updateFailableInRestrictions(next->id()); } // Check restrictions @@ -116,6 +117,7 @@ namespace storm { DFTRestrictionPointer next = queues.nextRestrictionCheck(); next->checkFails(*newState, queues); newState->updateFailableDependencies(next->id()); + newState->updateFailableInRestrictions(next->id()); } bool transient = false; @@ -153,6 +155,7 @@ namespace storm { // Update failable dependencies newState->updateFailableDependencies(nextBE->id()); newState->updateDontCareDependencies(nextBE->id()); + newState->updateFailableInRestrictions(nextBE->id()); // Add new state newStateId = stateToIdCallback(newState); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 8ae059104..1aa04eaa6 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -89,11 +89,12 @@ namespace storm { DFTStateGenerationInfo DFT::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const { DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount); - // Generate Pre and Post info for restrictions + // Generate Pre and Post info for restrictions, and mutexes for(auto const& elem : mElements) { if(!elem->isDependency() && !elem->isRestriction()) { generationInfo.setRestrictionPreElements(elem->id(), elem->seqRestrictionPres()); generationInfo.setRestrictionPostElements(elem->id(), elem->seqRestrictionPosts()); + generationInfo.setMutexElements(elem->id(), elem->mutexRestrictionElements()); } } diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 804068576..778c571b8 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -1,6 +1,7 @@ #include "DFTState.h" #include "storm-dft/storage/dft/DFTElements.h" #include "storm-dft/storage/dft/DFT.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace storage { @@ -22,7 +23,12 @@ namespace storm { // Initialize currently failable BEs for (size_t id : mDft.nonColdBEs()) { - failableElements.addBE(id); + // Check if restriction might prevent failure + if (!isEventDisabledViaRestriction(id)) { + failableElements.addBE(id); + } else { + STORM_LOG_TRACE("BE " << id << " is disabled due to a restriction."); + } } } @@ -40,7 +46,7 @@ namespace storm { STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed."); for(size_t index = 0; index < mDft.nrElements(); ++index) { // Initialize currently failable BE - if (mDft.isBasicElement(index) && isOperational(index)) { + if (mDft.isBasicElement(index) && isOperational(index) && !isEventDisabledViaRestriction(index)) { std::shared_ptr> be = mDft.getBasicElement(index); if (be->canFail()) { switch (be->type()) { @@ -215,16 +221,69 @@ namespace storm { bool addedFailableDependency = false; for (auto dependency : mDft.getElement(id)->outgoingDependencies()) { STORM_LOG_ASSERT(dependency->triggerEvent()->id() == id, "Ids do not match."); - assert(dependency->dependentEvents().size() == 1); + STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "Only one dependent event is allowed."); if (getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) { STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe."); - failableElements.addDependency(dependency->id()); - STORM_LOG_TRACE("New dependency failure: " << *dependency); - addedFailableDependency = true; + // By assertion we have only one dependent event + // Check if restriction prevents failure of dependent event + if (!isEventDisabledViaRestriction(dependency->dependentEvents()[0]->id())) { + // Add dependency as possible failure + failableElements.addDependency(dependency->id()); + STORM_LOG_TRACE("New dependency failure: " << *dependency); + addedFailableDependency = true; + } } } return addedFailableDependency; } + + template + bool DFTState::updateFailableInRestrictions(size_t id) { + if (!hasFailed(id)) { + // Non-failure does not change anything in a restriction + return false; + } + + bool addedFailableEvent = false; + for (auto restriction : mDft.getElement(id)->restrictions()) { + STORM_LOG_ASSERT(restriction->containsChild(id), "Ids do not match."); + if (restriction->isSeqEnforcer()) { + for (auto it = restriction->children().cbegin(); it != restriction->children().cend(); ++it) { + if ((*it)->isBasicElement()) { + if ((*it)->id() != id) { + if (!hasFailed((*it)->id())) { + // Failure should be prevented later on + STORM_LOG_TRACE("Child " << (*it)->id() << " should have failed."); + } + } else { + // Current event has failed + ++it; + if (it != restriction->children().cend()) { + // Enable next event + failableElements.addBE((*it)->id()); + STORM_LOG_TRACE("Added possible BE failure: " << *(*it)); + addedFailableEvent = true; + } + break; + } + } + } + } else if (restriction->isMutex()) { + // Current element has failed and disables all other children + for (auto const& child : restriction->children()) { + if (child->isBasicElement() && child->id() != id && getElementState(child->id()) == DFTElementState::Operational) { + // Disable child + failableElements.removeBE(child->id()); + STORM_LOG_TRACE("Disabled child: " << *child); + addedFailableEvent = true; + } + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Restriction must be SEQ or MUTEX"); + } + } + return addedFailableEvent; + } template void DFTState::updateDontCareDependencies(size_t id) { @@ -304,7 +363,7 @@ namespace storm { activate(representativeId); } for(size_t elem : mDft.module(representativeId)) { - if(mDft.isBasicElement(elem) && isOperational(elem)) { + if(mDft.isBasicElement(elem) && isOperational(elem) && !isEventDisabledViaRestriction(elem)) { std::shared_ptr> be = mDft.getBasicElement(elem); if (be->canFail()) { switch (be->type()) { @@ -361,6 +420,28 @@ namespace storm { STORM_LOG_ASSERT(hasFailed(spareId), "Spare has not failed."); mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount()); } + + template + bool DFTState::isEventDisabledViaRestriction(size_t id) const { + STORM_LOG_ASSERT(!mDft.isDependency(id), "Event " << id << " is dependency."); + STORM_LOG_ASSERT(!mDft.isRestriction(id), "Event " << id << " is restriction."); + // First check sequence enforcer + auto const& preIds = mStateGenerationInfo.seqRestrictionPreElements(id); + for (size_t id : preIds) { + if (isOperational(id)) { + return true; + } + } + + // Second check mutexes + auto const& mutexIds = mStateGenerationInfo.mutexRestrictionElements(id); + for (size_t id : mutexIds) { + if (!isOperational(id)) { + return true; + } + } + return false; + } template bool DFTState::hasOperationalPostSeqElements(size_t id) const { diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index e569e8d49..97048fd2d 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -289,6 +289,13 @@ namespace storm { * @return true if failable dependent events exist */ bool updateFailableDependencies(size_t id); + + /** + * Sets all failable BEs due to restrictions from newly failed element. + * @param id Id of the newly failed element + * @return true if newly failable events exist + */ + bool updateFailableInRestrictions(size_t id); /** * Sets all dependencies dont care whose dependent event is the newly failed BE. @@ -315,6 +322,13 @@ namespace storm { * @return True, if elements were swapped, false if nothing changed. */ bool orderBySymmetry(); + + /*! + * Check whether the event cannot fail at the moment due to a restriction. + * @param id Event id. + * @return True iff a restriction prevents the failure of the event. + */ + bool isEventDisabledViaRestriction(size_t id) const; /** * Checks whether operational post seq elements are present diff --git a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h index bc7e56140..ec2ed993a 100644 --- a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h +++ b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h @@ -8,8 +8,9 @@ namespace storm { std::map mSpareUsageIndex; // id spare -> index first bit in state std::map mSpareActivationIndex; // id spare representative -> index in state std::vector mIdToStateIndex; // id -> index first bit in state - std::map> mSeqRestrictionPreElements; // id -> list of restriction pre elements; - std::map> mSeqRestrictionPostElements; // id -> list of restriction post elements; + std::map> mSeqRestrictionPreElements; // id -> list of restriction pre elements + std::map> mSeqRestrictionPostElements; // id -> list of restriction post elements + std::map> mMutexRestrictionElements; // id -> list of elments in the same mutexes std::vector>> mSymmetries; // pair (length of symmetry group, vector indicating the starting points of the symmetry groups) public: @@ -37,12 +38,25 @@ namespace storm { void setRestrictionPostElements(size_t id, std::vector const& elems) { mSeqRestrictionPostElements[id] = elems; } + + void setMutexElements(size_t id, std::vector const& elems) { + mMutexRestrictionElements[id] = elems; + } + + std::vector const& seqRestrictionPreElements(size_t index) const { + STORM_LOG_ASSERT(mSeqRestrictionPreElements.count(index) > 0, "Index invalid."); + return mSeqRestrictionPreElements.at(index); + } std::vector const& seqRestrictionPostElements(size_t index) const { STORM_LOG_ASSERT(mSeqRestrictionPostElements.count(index) > 0, "Index invalid."); return mSeqRestrictionPostElements.at(index); } - + + std::vector const& mutexRestrictionElements(size_t index) const { + STORM_LOG_ASSERT(mMutexRestrictionElements.count(index) > 0, "Index invalid."); + return mMutexRestrictionElements.at(index); + } void addSpareActivationIndex(size_t id, size_t index) { mSpareActivationIndex[id] = index; diff --git a/src/storm-dft/storage/dft/elements/DFTChildren.h b/src/storm-dft/storage/dft/elements/DFTChildren.h index a9d0c7290..8aeb1381f 100644 --- a/src/storm-dft/storage/dft/elements/DFTChildren.h +++ b/src/storm-dft/storage/dft/elements/DFTChildren.h @@ -52,6 +52,18 @@ namespace storm { return mChildren.size(); } + /*! + * Check whether the given element is contained in the list of children. + * @param id Id of element to search for. + * @return True iff element was found in list of children. + */ + bool containsChild(size_t id) { + auto it = std::find_if(this->mChildren.begin(), this->mChildren.end(), [&id](DFTElementPointer element) -> bool { + return element->id() == id; + }); + return it != this->mChildren.end(); + } + virtual std::vector independentUnit() const override { std::set unit = {this->mId}; for (auto const& child : mChildren) { diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index a7cca4f36..955d3b9be 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -113,7 +113,6 @@ namespace storm { return it != this->mDependentEvents.end(); } - virtual size_t nrChildren() const override { return 1; } diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h index b287ae863..80fff512c 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.h +++ b/src/storm-dft/storage/dft/elements/DFTElement.h @@ -338,6 +338,29 @@ namespace storm { return res; } + /** + * Obtains ids of elements which are under the same mutex. + * @return A vector of ids + */ + std::vector mutexRestrictionElements() const { + std::vector res; + for (auto const& restr : mRestrictions) { + if (!restr->isMutex()) { + continue; + } + bool found = false; + for (auto it = restr->children().cbegin(); it != restr->children().cend(); ++it) { + if ((*it)->id() != mId) { + res.push_back((*it)->id()); + } else { + found = true; + } + } + STORM_LOG_ASSERT(found, "Child " << mId << " is not included in restriction " << *restr); + } + return res; + } + virtual void extendSpareModule(std::set& elementsInModule) const; // virtual void extendImmediateFailureCausePathEvents(std::set& ) const; diff --git a/src/storm-dft/storage/dft/elements/DFTMutex.h b/src/storm-dft/storage/dft/elements/DFTMutex.h index cbc18a69b..ff50d0f9f 100644 --- a/src/storm-dft/storage/dft/elements/DFTMutex.h +++ b/src/storm-dft/storage/dft/elements/DFTMutex.h @@ -28,7 +28,7 @@ namespace storm { return DFTElementType::MUTEX; } - bool isSeqEnforcer() const override { + bool isMutex() const override { return true; } diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h index 92c9a69ec..54421d556 100644 --- a/src/storm-dft/storage/dft/elements/DFTRestriction.h +++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h @@ -44,6 +44,14 @@ namespace storm { return false; } + /*! + * Return whether the restriction is a mutex. + * @return True iff the restriction is a MUTEX. + */ + virtual bool isMutex() const { + return false; + } + /*! * Returns whether all children are BEs. * @return True iff all children are BEs.