n-ary pdeps supported as a datastructure

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

@@ -174,7 +174,8 @@ namespace storm {
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
                 visitQueue.push(dependency->id());
                 visitQueue.push(dependency->triggerEvent()->id());
-                visitQueue.push(dependency->dependentEvent()->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.");
+                visitQueue.push(dependency->dependentEvents()[0]->id());
             }
             stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
 

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

@@ -268,7 +268,9 @@ namespace storm {
                 {
                     DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
                     children.push_back(dependency->triggerEvent()->name());
-                    children.push_back(dependency->dependentEvent()->name());
+                    for(auto const& depEv : dependency->dependentEvents()) {
+                        children.push_back(depEv->name());
+                    }
                     addDepElement(element->name(), children, dependency->probability());
                     break;
                 }

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

@@ -258,7 +258,8 @@ namespace storage {
         }
         
         void colourize(std::shared_ptr<const DFTDependency<ValueType>> const& dep) {
-            depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), dep->dependentEvent()->activeFailureRate());
+            // TODO this can be improved for n-ary dependencies.
+            depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), dep->dependentEvents()[0]->activeFailureRate());
         }
         
         void colourize(std::shared_ptr<const DFTRestriction<ValueType>> const& restr) {
@@ -486,10 +487,26 @@ namespace storage {
                     STORM_LOG_ASSERT(dft.isDependency(indexpair.second), "Element is no dependency.");
                     auto const& lDep = dft.getDependency(indexpair.first);
                     auto const& rDep = dft.getDependency(indexpair.second);
+
                     if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) {
                         return false;
-                    } 
-                    if(bijection.at(lDep->dependentEvent()->id()) != rDep->dependentEvent()->id()) {
+                    }
+
+                    std::set<size_t> dependenciesLeftMapped;
+                    for (auto const& depEv : lDep->dependentEvents()) {
+                        if (bleft.has(depEv->id())) {
+                            dependenciesLeftMapped.insert(bijection.at(depEv->id()));
+                        }
+                    }
+
+                    std::set<size_t> dependenciesRight;
+                    for (auto const& depEv : rDep->dependentEvents()) {
+                        if (bright.has(depEv->id())) {
+                            dependenciesRight.insert(depEv->id());
+                        }
+                    }
+
+                    if (dependenciesLeftMapped != dependenciesRight) {
                         return false;
                     }
                 } else if(dft.isRestriction(indexpair.first)) {

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

@@ -57,7 +57,8 @@ namespace storm {
             for (size_t dependencyId : mDft.getDependencies()) {
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(dependencyId);
                 STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match.");
-                if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
+                assert(dependency->dependentEvents().size() == 1);
+                if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
                     mFailableDependencies.push_back(dependencyId);
                     STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
                 }
@@ -198,8 +199,9 @@ namespace storm {
             
             for (auto dependency : mDft.getElement(id)->outgoingDependencies()) {
                 STORM_LOG_ASSERT(dependency->triggerEvent()->id() == id, "Ids do not match.");
-                if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
-                    STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvent()->id()), "Dependent event is failsafe.");
+                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.");
                     mFailableDependencies.push_back(dependency->id());
                     STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
                 }
@@ -213,7 +215,8 @@ namespace storm {
             STORM_LOG_ASSERT(hasFailed(id), "Element has not failed.");
             
             for (auto dependency : mDft.getBasicElement(id)->ingoingDependencies()) {
-                STORM_LOG_ASSERT(dependency->dependentEvent()->id() == id, "Ids do not match.");
+                assert(dependency->dependentEvents().size() == 1);
+                STORM_LOG_ASSERT(dependency->dependentEvents()[0]->id() == id, "Ids do not match.");
                 setDependencyDontCare(dependency->id());
             }
         }
@@ -244,7 +247,8 @@ namespace storm {
                 // Consider failure due to dependency
                 STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
-                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
+                assert(dependency->dependentEvents().size() == 1);
+                std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true);
                 mFailableDependencies.erase(mFailableDependencies.begin() + index);
                 setFailed(res.first->id());
                 setDependencySuccessful(dependency->id());

src/storm-dft/storage/dft/elements/DFTBE.h

@@ -38,7 +38,8 @@ namespace storm {
             }
             
             bool addIngoingDependency(DFTDependencyPointer const& e) {
-                STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match.");
+                // TODO write this assertion for n-ary dependencies, probably by addign a method to the dependencies to support this.
+                //STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match.");
                 if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
                     return false;
                 }

src/storm-dft/storage/dft/elements/DFTDependency.h

@@ -14,7 +14,7 @@ namespace storm {
         protected:
             ValueType mProbability;
             DFTGatePointer mTriggerEvent;
-            DFTBEPointer mDependentEvent;
+            std::vector<DFTBEPointer> mDependentEvents;
 
         public:
             DFTDependency(size_t id, std::string const& name, ValueType probability) :
@@ -30,7 +30,7 @@ namespace storm {
             }
 
             void setDependentEvent(DFTBEPointer const& dependentEvent) {
-                mDependentEvent = dependentEvent;
+                mDependentEvents = { dependentEvent };
             }
 
 
@@ -43,9 +43,9 @@ namespace storm {
                 return mTriggerEvent;
             }
 
-            DFTBEPointer const& dependentEvent() const {
-                STORM_LOG_ASSERT(mDependentEvent, "Dependent element does not exists.");
-                return mDependentEvent;
+            std::vector<DFTBEPointer> const& dependentEvents() const {
+                STORM_LOG_ASSERT(mDependentEvents.size() > 0, "Dependent element does not exists.");
+                return mDependentEvents;
             }
 
             DFTElementType type() const override {
@@ -69,9 +69,11 @@ namespace storm {
 
             virtual std::vector<size_t> independentUnit() const override {
                 std::set<size_t> unit = {this->mId};
-                mDependentEvent->extendUnit(unit);
-                if(unit.count(mTriggerEvent->id()) != 0) {
-                    return {};
+                for(auto const& depEv : mDependentEvents) {
+                    depEv->extendUnit(unit);
+                    if(unit.count(mTriggerEvent->id()) != 0) {
+                        return {};
+                    }
                 }
                 return std::vector<size_t>(unit.begin(), unit.end());
             }
@@ -83,7 +85,10 @@ namespace storm {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
-                mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+                for (auto const& depEv : mDependentEvents) {
+                    depEv->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+                    if (elemsInSubtree.empty()) return;
+                }
                 if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
@@ -95,7 +100,11 @@ namespace storm {
             virtual std::string toString() const override {
                 std::stringstream stream;
                 bool fdep = storm::utility::isOne(mProbability);
-                stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+                stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => { ";
+                for(auto const& depEv : mDependentEvents) {
+                    stream << depEv->name() << " ";
+                }
+                stream << "}";
                 if (!fdep) {
                     stream << " with probability " << mProbability;
                 }

src/storm-dft/storage/dft/elements/DFTElement.cpp

@@ -14,8 +14,10 @@ namespace storm {
             }
             
             // Check that no outgoing dependencies can be triggered anymore
+            // Notice that n-ary dependencies are supported via rewriting them during build-time
             for (DFTDependencyPointer dependency : mOutgoingDependencies) {
-                if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) {
+                assert(dependency->dependentEvents().size() == 1);
+                if (state.isOperational(dependency->dependentEvents()[0]->id()) && state.isOperational(dependency->triggerEvent()->id())) {
                     return false;
                 }
             }