diff --git a/src/storage/dft/elements/DFTElement.cpp b/src/storage/dft/elements/DFTElement.cpp new file mode 100644 index 000000000..b71e0672b --- /dev/null +++ b/src/storage/dft/elements/DFTElement.cpp @@ -0,0 +1,120 @@ +#include +#include +#include +#include "DFTElement.h" +#include "../DFTElements.h" + +namespace storm { + namespace storage { + + template + bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if (state.dontCare(mId)) { + return false; + } + + // Check that no outgoing dependencies can be triggered anymore + for (DFTDependencyPointer dependency : mOutgoingDependencies) { + if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) { + return false; + } + } + + bool hasParentSpare = false; + + // Check that no parent can fail anymore + for(DFTGatePointer const& parent : mParents) { + if(state.isOperational(parent->id())) { + return false; + } + if (parent->isSpareGate()) { + hasParentSpare = true; + } + } + + state.setDontCare(mId); + if (hasParentSpare && !state.isActive(mId)) { + // Activate child for consistency in failed spares + state.activate(mId); + } + return true; + } + + template + void DFTElement::extendSpareModule(std::set& elementsInModule) const { + for(auto const& parent : mParents) { + if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) { + elementsInModule.insert(parent->id()); + parent->extendSpareModule(elementsInModule); + } + } + } + + template + std::vector DFTElement::independentUnit() const { + std::vector res; + res.push_back(this->id()); + // Extend for pdeps. + return res; + } + + template + void DFTElement::extendUnit(std::set& unit) const { + unit.insert(mId); + } + + template + std::vector DFTElement::independentSubDft(bool blockParents) const { + //std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl; + std::vector res; + res.push_back(this->id()); + return res; + } + + template + void DFTElement::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents) const { + if(elemsInSubtree.count(this->id()) > 0) return; + if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) { + // This is a parent of the suspected root, thus it is not a subdft. + elemsInSubtree.clear(); + return; + } + elemsInSubtree.insert(mId); + for(auto const& parent : mParents) { + if(blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) { + continue; + } + parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + if(elemsInSubtree.empty()) { + return; + } + } + for(auto const& dep : mOutgoingDependencies) { + dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + if(elemsInSubtree.empty()) { + return; + } + + } + + for(auto const& restr : mRestrictions) { + restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents); + if(elemsInSubtree.empty()) { + return; + } + } + + } + + + + // Explicitly instantiate the class. + template class DFTElement; + +#ifdef STORM_HAVE_CARL + template class DFTElement; +#endif + + + } +}