From d35bc5ed367419b685f8c7a252680a6fb85991e7 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 15 Dec 2016 02:13:30 +0100 Subject: [PATCH] n-ary pdeps supported as a datastructure --- src/storm-dft/storage/dft/DFT.cpp | 3 +- src/storm-dft/storage/dft/DFTBuilder.cpp | 4 ++- src/storm-dft/storage/dft/DFTIsomorphism.h | 23 +++++++++++++-- src/storm-dft/storage/dft/DFTState.cpp | 14 +++++---- src/storm-dft/storage/dft/elements/DFTBE.h | 3 +- .../storage/dft/elements/DFTDependency.h | 29 ++++++++++++------- .../storage/dft/elements/DFTElement.cpp | 4 ++- 7 files changed, 58 insertions(+), 22 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 3e06299f1..e38c40ce1 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -174,7 +174,8 @@ namespace storm { std::shared_ptr 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); diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 35ed767b8..44846612f 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -268,7 +268,9 @@ namespace storm { { DFTDependencyPointer dependency = std::static_pointer_cast>(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; } diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index 86625c975..081b76f0b 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -258,7 +258,8 @@ namespace storage { } void colourize(std::shared_ptr> const& dep) { - depColour[dep->id()] = std::pair(dep->probability(), dep->dependentEvent()->activeFailureRate()); + // TODO this can be improved for n-ary dependencies. + depColour[dep->id()] = std::pair(dep->probability(), dep->dependentEvents()[0]->activeFailureRate()); } void colourize(std::shared_ptr> 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 dependenciesLeftMapped; + for (auto const& depEv : lDep->dependentEvents()) { + if (bleft.has(depEv->id())) { + dependenciesLeftMapped.insert(bijection.at(depEv->id())); + } + } + + std::set 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)) { diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 78c0937d8..ec6509944 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -57,7 +57,8 @@ namespace storm { for (size_t dependencyId : mDft.getDependencies()) { std::shared_ptr 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 const> dependency = mDft.getDependency(mFailableDependencies[index]); - std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true); + assert(dependency->dependentEvents().size() == 1); + std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true); mFailableDependencies.erase(mFailableDependencies.begin() + index); setFailed(res.first->id()); setDependencySuccessful(dependency->id()); diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 216227af6..3be82d9f1 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/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; } diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index 957048d68..e389f519e 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -14,7 +14,7 @@ namespace storm { protected: ValueType mProbability; DFTGatePointer mTriggerEvent; - DFTBEPointer mDependentEvent; + std::vector 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 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 independentUnit() const override { std::set 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(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; } diff --git a/src/storm-dft/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp index 61a087bdb..287af8e98 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.cpp +++ b/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; } }