diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index f35a09f0f..f0d1db5ac 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -41,7 +41,8 @@ namespace storm { assert(mElements[dependency->nameDependent()]->isBasicElement()); std::shared_ptr> dependentEvent = std::static_pointer_cast>(mElements[dependency->nameDependent()]); dependency->initialize(triggerEvent, dependentEvent); - triggerEvent->addDependency(dependency); + triggerEvent->addOutgoingDependency(dependency); + dependentEvent->addIngoingDependency(dependency); } // Sort elements topologically diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index 5597f1c5e..c7fc1d960 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -7,7 +7,7 @@ namespace storm { template bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(!state.dontCare(mId) && !hasDependencies()) + if(!state.dontCare(mId) && !hasOutgoingDependencies()) { for(DFTGatePointer const& parent : mParents) { if(state.isOperational(parent->id())) { diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index e49b91901..d7060654f 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -35,13 +35,12 @@ namespace storm { using DFTDependencyPointer = std::shared_ptr>; using DFTDependencyVector = std::vector; - protected: size_t mId; std::string mName; size_t mRank = -1; DFTGateVector mParents; - DFTDependencyVector dependencies; + DFTDependencyVector mOutgoingDependencies; public: DFTElement(size_t id, std::string const& name) : @@ -139,29 +138,30 @@ namespace storm { return res; } - bool addDependency(DFTDependencyPointer const& e) { - if(std::find(dependencies.begin(), dependencies.end(), e) != dependencies.end()) { + bool addOutgoingDependency(DFTDependencyPointer const& e) { + assert(e->triggerEvent()->id() == this->id()); + if(std::find(mOutgoingDependencies.begin(), mOutgoingDependencies.end(), e) != mOutgoingDependencies.end()) { return false; } else { - dependencies.push_back(e); + mOutgoingDependencies.push_back(e); return true; } } - bool hasDependencies() const { - return !dependencies.empty(); + bool hasOutgoingDependencies() const { + return !mOutgoingDependencies.empty(); } - size_t nrDependencies() const { - return dependencies.size(); + size_t nrOutgoingDependencies() const { + return mOutgoingDependencies.size(); } - DFTDependencyVector const& getDependencies() const { - return dependencies; + DFTDependencyVector const& getOutgoingDependencies() const { + return mOutgoingDependencies; } - + virtual void extendSpareModule(std::set& elementsInModule) const; virtual size_t nrChildren() const = 0; @@ -375,9 +375,14 @@ namespace storm { template class DFTBE : public DFTElement { + + using DFTDependencyPointer = std::shared_ptr>; + using DFTDependencyVector = std::vector; + protected: ValueType mActiveFailureRate; ValueType mPassiveFailureRate; + DFTDependencyVector mIngoingDependencies; public: DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) : @@ -399,6 +404,30 @@ namespace storm { ValueType const& passiveFailureRate() const { return mPassiveFailureRate; } + + bool addIngoingDependency(DFTDependencyPointer const& e) { + assert(e->dependentEvent()->id() == this->id()); + if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) { + return false; + } + else + { + mIngoingDependencies.push_back(e); + return true; + } + } + + bool hasIngoingDependencies() const { + return !mIngoingDependencies.empty(); + } + + size_t nrIngoingDependencies() const { + return mIngoingDependencies.size(); + } + + DFTDependencyVector const& getIngoingDependencies() const { + return mIngoingDependencies; + } std::string toString() const override { std::stringstream stream;