From bec75813b1f9b7ecc2f3f75c400e973604f45021 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 7 Jun 2019 15:34:44 +0200 Subject: [PATCH] Added computation of dynamic behavior vector for DFTs --- src/storm-dft/builder/DFTBuilder.cpp | 86 +++++++++++++++++++++++++++- src/storm-dft/builder/DFTBuilder.h | 2 + src/storm-dft/storage/dft/DFT.cpp | 5 +- src/storm-dft/storage/dft/DFT.h | 8 ++- 4 files changed, 98 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index c02fb3364..af9569eb5 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]); + storm::storage::DFT dft(elems, mElements[mTopLevelIdentifier], computeHasDynamicBehavior(elems)); // Set layout info for (auto& elem : mElements) { @@ -135,6 +135,90 @@ 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/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 31764e2b8..2529ff5c1 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -236,6 +236,8 @@ namespace storm { void topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L); DFTElementVector topoSort(); + + std::vector computeHasDynamicBehavior(DFTElementVector elements); // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. bool pandDefaultInclusive; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 28b7d29d0..78ecfe8bb 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -17,7 +17,10 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { + 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) { // Check that ids correspond to indices in the element vector STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect."); size_t nrRepresentatives = 0; diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 5c885ef59..37ebe58d2 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -67,9 +67,11 @@ namespace storm { std::map mRepresentants; // id element -> id representative std::vector> mSymmetries; std::map mLayoutInfo; + std::vector mDynamicBehavior; public: - DFT(DFTElementVector const& elements, DFTElementPointer const& tle); + DFT(DFTElementVector const &elements, DFTElementPointer const &tle, + std::vector const &dynamicBehavior); DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const; @@ -133,6 +135,10 @@ namespace storm { return mDependencies; } + std::vector const &getDynamicBehavior() const { + return mDynamicBehavior; + } + std::vector nonColdBEs() const { std::vector result; for (DFTElementPointer elem : mElements) {