Proper handling of disabling/enabling events for SEQ and MUTEX

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);

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

@@ -89,11 +89,12 @@ namespace storm {
         DFTStateGenerationInfo DFT<ValueType>::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());
                 }
             }
 

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<const DFTBE<ValueType>> 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<typename ValueType>
+        bool DFTState<ValueType>::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<typename ValueType>
         void DFTState<ValueType>::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<const DFTBE<ValueType>> 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<typename ValueType>
+        bool DFTState<ValueType>::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<typename ValueType>
         bool DFTState<ValueType>::hasOperationalPostSeqElements(size_t id) const {

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

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

@@ -8,8 +8,9 @@ namespace storm {
             std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
             std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
             std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
-            std::map<size_t, std::vector<size_t>> mSeqRestrictionPreElements; // id -> list of restriction pre elements;
-            std::map<size_t, std::vector<size_t>> mSeqRestrictionPostElements; // id -> list of restriction post elements;
+            std::map<size_t, std::vector<size_t>> mSeqRestrictionPreElements; // id -> list of restriction pre elements
+            std::map<size_t, std::vector<size_t>> mSeqRestrictionPostElements; // id -> list of restriction post elements
+            std::map<size_t, std::vector<size_t>> mMutexRestrictionElements; // id -> list of elments in the same mutexes
             std::vector<std::pair<size_t, std::vector<size_t>>> 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<size_t> const& elems) {
                 mSeqRestrictionPostElements[id] = elems;
             }
+
+            void setMutexElements(size_t id, std::vector<size_t> const& elems) {
+                mMutexRestrictionElements[id] = elems;
+            }
+
+            std::vector<size_t> const& seqRestrictionPreElements(size_t index) const {
+                STORM_LOG_ASSERT(mSeqRestrictionPreElements.count(index) > 0, "Index invalid.");
+                return mSeqRestrictionPreElements.at(index);
+            }
             
             std::vector<size_t> const& seqRestrictionPostElements(size_t index) const {
                 STORM_LOG_ASSERT(mSeqRestrictionPostElements.count(index) > 0, "Index invalid.");
                 return mSeqRestrictionPostElements.at(index);
             }
-            
+
+            std::vector<size_t> 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;

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<size_t> independentUnit() const override {
                 std::set<size_t> unit = {this->mId};
                 for (auto const& child : mChildren) {

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;
             }

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<size_t> mutexRestrictionElements() const {
+                std::vector<size_t> 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<size_t>& elementsInModule) const;
 
             // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;

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;
             }
 

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.