diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 87c6aafa9..117ee9c43 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -92,6 +92,17 @@ void processOptions() { } #ifdef STORM_HAVE_Z3 + if(debug.isTestSet()){ + dft->setDynamicBehaviorInfo(); + for(size_t i = 0; i < dft->nrElements(); ++i){ + if(dft->getDynamicBehavior()[i]) { + STORM_LOG_DEBUG("Element " << dft->getElement(i)->name() << " has dynamic behavior"); + } else { + STORM_LOG_DEBUG("Element " << dft->getElement(i)->name() << " has static behavior"); + } + } + } + if (faultTreeSettings.solveWithSMT()) { dft = dftTransformator.transformUniqueFailedBe(*dft); if (dft->getDependencies().size() > 0) { @@ -100,6 +111,8 @@ void processOptions() { } // Solve with SMT STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + // Set dynamic behavior vector + dft->setDynamicBehaviorInfo(); storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet()); return; } diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index af9569eb5..c02fb3364 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -97,7 +97,7 @@ namespace storm { } STORM_LOG_THROW(!mTopLevelIdentifier.empty(), storm::exceptions::WrongFormatException, "No top level element defined."); - storm::storage::DFT dft(elems, mElements[mTopLevelIdentifier], computeHasDynamicBehavior(elems)); + storm::storage::DFT dft(elems, mElements[mTopLevelIdentifier]); // Set layout info for (auto& elem : mElements) { @@ -135,90 +135,6 @@ namespace storm { return elem->rank(); } - template - std::vector DFTBuilder::computeHasDynamicBehavior(DFTElementVector elements) { - std::vector dynamicBehaviorVector(elements.size()); - // Initialize with false - std::fill(dynamicBehaviorVector.begin(), dynamicBehaviorVector.end(), false); - - std::queue elementQueue; - - // deal with all dynamic elements - for (auto const &element : elements) { - switch (element->type()) { - case storage::DFTElementType::PAND: - case storage::DFTElementType::POR: - // TODO check SPAREs, SEQs, MUTEXs - case storage::DFTElementType::SPARE: - case storage::DFTElementType::SEQ: - case storage::DFTElementType::MUTEX: { - auto gate = std::static_pointer_cast>(element); - dynamicBehaviorVector[gate->id()] = true; - for (auto const &child : gate->children()) { - // only enqueue static children - if (!dynamicBehaviorVector.at(child->id())) { - elementQueue.push(child); - } - } - break; - } - default: { - break; - } - - } - } - // propagate dynamic behavior - while (!elementQueue.empty()) { - DFTElementPointer currentElement = elementQueue.front(); - elementQueue.pop(); - switch (currentElement->type()) { - // Static Gates - case storage::DFTElementType::AND: - case storage::DFTElementType::OR: - case storage::DFTElementType::VOT: { - // check all parents and if one has dynamic behavior, propagate it - dynamicBehaviorVector[currentElement->id()] = true; - auto gate = std::static_pointer_cast>(currentElement); - for (auto const &child : gate->children()) { - // only enqueue static children - if (!dynamicBehaviorVector.at(child->id())) { - elementQueue.push(child); - } - } - break; - } - //BEs - case storage::DFTElementType::BE_EXP: - case storage::DFTElementType::BE_CONST: - case storage::DFTElementType::BE: { - auto be = std::static_pointer_cast>(currentElement); - dynamicBehaviorVector[be->id()] = true; - // add all ingoing dependencies to queue - for (auto const &dep : be->ingoingDependencies()) { - if (!dynamicBehaviorVector.at(dep->id())) { - elementQueue.push(dep); - } - } - break; - } - case storage::DFTElementType::PDEP: { - auto dep = std::static_pointer_cast>(currentElement); - dynamicBehaviorVector[dep->id()] = true; - // add all ingoing dependencies to queue - auto trigger = dep->triggerEvent(); - if (!dynamicBehaviorVector.at(trigger->id())) { - elementQueue.push(trigger); - } - break; - } - default: - break; - } - } - return dynamicBehaviorVector; - } - template bool DFTBuilder::addRestriction(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp) { if (children.size() <= 1) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 133a5ea14..c30b365a1 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -948,7 +948,7 @@ namespace storm { dep1Index = dft.getDependencies().at(i); for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { dep2Index = dft.getDependencies().at(j); - if (dft.getDynamicBehavior()[dep1Index] || dft.getDynamicBehavior()[dep2Index]) { + if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { if (dft.getDependency(dep1Index)->triggerEvent() == dft.getDependency(dep2Index)->triggerEvent()) { STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 78ecfe8bb..b65638691 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -17,12 +17,15 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const &elements, DFTElementPointer const &tle, - std::vector const &dynamicBehavior) : - mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0), - mDynamicBehavior(dynamicBehavior) { + DFT::DFT(DFTElementVector const &elements, DFTElementPointer const &tle) : + mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { // Check that ids correspond to indices in the element vector STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect."); + + // Initialize dynamic behavior vector with TRUE to preserve correct behavior + // We don't directly call setDynamicBehaviorInfo to not slow down DFT generation if possible + mDynamicBehavior = std::vector(mElements.size()); + std::fill(mDynamicBehavior.begin(), mDynamicBehavior.end(), true); size_t nrRepresentatives = 0; for (auto& elem : mElements) { @@ -88,6 +91,151 @@ namespace storm { mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives; } + template + void DFT::setDynamicBehaviorInfo() { + std::vector dynamicBehaviorVector(mElements.size()); + + std::queue elementQueue; + + // deal with all dynamic elements + for (auto const &element : mElements) { + switch (element->type()) { + case storage::DFTElementType::PAND: + case storage::DFTElementType::POR: + case storage::DFTElementType::MUTEX: { + auto gate = std::static_pointer_cast>(element); + dynamicBehaviorVector[gate->id()] = true; + for (auto const &child : gate->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + break; + } + // TODO different cases + case storage::DFTElementType::SPARE: { + auto spare = std::static_pointer_cast>(element); + + // Iterate over all children (representatives of spare modules) + for (auto const &child : spare->children()) { + // Case 1: Shared Module + // If child only has one parent, it is this SPARE -> nothing to check + if (child->nrParents() > 1) { + // TODO make more efficient by directly setting ALL spares which share a module to be dynamic + for (auto const &parent : child->parents()) { + if (parent->isSpareGate() and parent->id() != spare->id()) { + dynamicBehaviorVector[spare->id()] = true; + break; // inner loop + } + } + } + // Case 2: Triggering outside events + // If the SPARE was already detected to have dynamic behavior, do not proceed + if (!dynamicBehaviorVector[spare->id()]) { + for (auto const &memberID : module(child->id())) { + // Iterate over all members of the module child represents + auto member = getElement(memberID); + for (auto const dep : member->outgoingDependencies()) { + // If the member has outgoing dependencies, check if those trigger something outside the module + for (auto const depEvent : dep->dependentEvents()) { + // If a dependent event is not found in the module, SPARE is dynamic + if (std::find(module(child->id()).begin(), module(child->id()).end(), + depEvent->id()) == module(child->id()).end()) { + dynamicBehaviorVector[spare->id()] = true; + break; //depEvent-loop + } + } + if (dynamicBehaviorVector[spare->id()]) { break; } //dependency-loop + } + if (dynamicBehaviorVector[spare->id()]) { break; } //module-loop + } + + } + if (dynamicBehaviorVector[spare->id()]) { break; } //child-loop + } + // if during the computation, dynamic behavior was detected, add children to queue + if (dynamicBehaviorVector[spare->id()]) { + for (auto const &child : spare->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + } + break; + } + case storage::DFTElementType::SEQ: { + auto seq = std::static_pointer_cast>(element); + // A SEQ only has dynamic behavior if not all children are BEs + if (!seq->allChildrenBEs()) { + dynamicBehaviorVector[seq->id()] = true; + for (auto const &child : seq->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + } + break; + } + default: { + break; + } + + } + } + // propagate dynamic behavior + while (!elementQueue.empty()) { + DFTElementPointer currentElement = elementQueue.front(); + elementQueue.pop(); + switch (currentElement->type()) { + // Static Gates + case storage::DFTElementType::AND: + case storage::DFTElementType::OR: + case storage::DFTElementType::VOT: { + // check all parents and if one has dynamic behavior, propagate it + dynamicBehaviorVector[currentElement->id()] = true; + auto gate = std::static_pointer_cast>(currentElement); + for (auto const &child : gate->children()) { + // only enqueue static children + if (!dynamicBehaviorVector.at(child->id())) { + elementQueue.push(child); + } + } + break; + } + //BEs + case storage::DFTElementType::BE_EXP: + case storage::DFTElementType::BE_CONST: + case storage::DFTElementType::BE: { + auto be = std::static_pointer_cast>(currentElement); + dynamicBehaviorVector[be->id()] = true; + // add all ingoing dependencies to queue + for (auto const &dep : be->ingoingDependencies()) { + if (!dynamicBehaviorVector.at(dep->id())) { + elementQueue.push(dep); + } + } + break; + } + case storage::DFTElementType::PDEP: { + auto dep = std::static_pointer_cast>(currentElement); + dynamicBehaviorVector[dep->id()] = true; + // add all ingoing dependencies to queue + auto trigger = dep->triggerEvent(); + if (!dynamicBehaviorVector.at(trigger->id())) { + elementQueue.push(trigger); + } + break; + } + default: + break; + } + } + mDynamicBehavior = dynamicBehaviorVector; + } + template DFTStateGenerationInfo DFT::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const { DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount); diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 37ebe58d2..2133a54ab 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -70,8 +70,7 @@ namespace storm { std::vector mDynamicBehavior; public: - DFT(DFTElementVector const &elements, DFTElementPointer const &tle, - std::vector const &dynamicBehavior); + DFT(DFTElementVector const &elements, DFTElementPointer const &tle); DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const; @@ -82,6 +81,8 @@ namespace storm { DFT optimize() const; void copyElements(std::vector elements, storm::builder::DFTBuilder builder) const; + + void setDynamicBehaviorInfo(); size_t stateBitVectorSize() const { // Ensure multiple of 64