diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 9a1b086fc..ea4417915 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -79,10 +79,6 @@ namespace storm { template DFTStateGenerationInfo DFT::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const { - // Use symmetry - // Collect all elements in the first subtree - // TODO make recursive to use for nested subtrees - DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount); // Generate Pre and Post info for restrictions @@ -92,19 +88,17 @@ namespace storm { generationInfo.setRestrictionPostElements(elem->id(), elem->seqRestrictionPosts()); } } - - // Perform DFS and insert all elements of subtree sequentially size_t stateIndex = 0; std::queue visitQueue; storm::storage::BitVector visited(nrElements(), false); - // TODO make subfunction for this? if (symmetries.groups.empty()) { // Perform DFS for whole tree visitQueue.push(mTopLevelIndex); stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); } else { + // Generate information according to symmetries for (size_t symmetryIndex : symmetries.sortedSymmetries) { assert(!visited[symmetryIndex]); auto const& symmetryGroup = symmetries.groups.at(symmetryIndex); @@ -430,7 +424,7 @@ namespace storm { stream << "[" << elem->id() << "]"; stream << elem->toString(); if (elem->isDependency()) { - stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id())); + stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]"; } else { stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id())); if(elem->isSpareGate()) { @@ -445,10 +439,9 @@ namespace storm { } return stream.str(); } - - // TODO rewrite to only use bitvector and id + template - std::string DFT::getStateString(DFTStatePointer const& state) const{ + std::string DFT::getStateString(DFTStatePointer const& state) const { std::stringstream stream; stream << "(" << state->getId() << ") "; for (auto const& elem : mElements) { @@ -467,6 +460,37 @@ namespace storm { } } return stream.str(); + } + + template + std::string DFT::getStateString(storm::storage::BitVector const& status, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const { + std::stringstream stream; + stream << "(" << id << ") "; + for (auto const& elem : mElements) { + size_t elemIndex = stateGenerationInfo.getStateIndex(elem->id()); + int elementState = DFTState::getElementStateInt(status, elemIndex); + if (elem->isDependency()) { + stream << storm::storage::toChar(static_cast(elementState)) << "[dep]"; + } else { + stream << storm::storage::toChar(static_cast(elementState)); + if(elem->isSpareGate()) { + stream << "["; + size_t nrUsedChild = status.getAsInt(stateGenerationInfo.getSpareUsageIndex(elem->id()), stateGenerationInfo.usageInfoBits()); + size_t useId; + if (nrUsedChild == getMaxSpareChildCount()) { + useId = elem->id(); + } else { + useId = getChild(elem->id(), nrUsedChild); + } + bool isActive = status[stateGenerationInfo.getSpareActivationIndex(useId)]; + if(useId == elem->id() || isActive) { + stream << "actively "; + } + stream << "using " << useId << "]"; + } + } + } + return stream.str(); } template diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 071a7e56a..6fdfd08ef 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -130,8 +130,11 @@ namespace storm { std::vector nonColdBEs() const { std::vector result; for(DFTElementPointer elem : mElements) { - if(elem->isBasicElement() && std::static_pointer_cast>(elem)->canFail() && !elem->isColdBasicElement()) { - result.push_back(elem->id()); + if(elem->isBasicElement()) { + std::shared_ptr> be = std::static_pointer_cast>(elem); + if (be->canFail() && !be->isColdBasicElement()) { + result.push_back(be->id()); + } } } return result; @@ -246,6 +249,8 @@ namespace storm { std::string getStateString(DFTStatePointer const& state) const; + std::string getStateString(storm::storage::BitVector const& status, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const; + std::vector getIndependentSubDftRoots(size_t index) const; DFTColouring colourDFT() const; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 4d603e501..b1c9a4fc1 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -67,6 +67,11 @@ namespace storm { int DFTState::getElementStateInt(size_t id) const { return mStatus.getAsInt(mStateGenerationInfo.getStateIndex(id), 2); } + + template + int DFTState::getElementStateInt(storm::storage::BitVector const& state, size_t indexId) { + return state.getAsInt(indexId, 2); + } template size_t DFTState::getId() const { @@ -246,8 +251,11 @@ namespace storm { activate(representativeId); } for(size_t elem : mDft.module(representativeId)) { - if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem) && mDft.getBasicElement(elem)->canFail()) { - mIsCurrentlyFailableBE.push_back(elem); + if(mDft.isBasicElement(elem) && isOperational(elem)) { + std::shared_ptr> be = mDft.getBasicElement(elem); + if (be->isColdBasicElement() && be->canFail()) { + mIsCurrentlyFailableBE.push_back(elem); + } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { propagateActivation(uses(elem)); } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 1311d74ae..5b68d46ae 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -47,6 +47,8 @@ namespace storm { int getElementStateInt(size_t id) const; + static int getElementStateInt(storm::storage::BitVector const& state, size_t indexId); + size_t getId() const; void setId(size_t id); diff --git a/src/storage/dft/elements/DFTBE.h b/src/storage/dft/elements/DFTBE.h index e7f912fd4..d41e37344 100644 --- a/src/storage/dft/elements/DFTBE.h +++ b/src/storage/dft/elements/DFTBE.h @@ -67,11 +67,11 @@ namespace storm { return stream.str(); } - bool isBasicElement() const override{ + bool isBasicElement() const override { return true; } - bool isColdBasicElement() const override{ + bool isColdBasicElement() const { return storm::utility::isZero(mPassiveFailureRate); } diff --git a/src/storage/dft/elements/DFTElement.h b/src/storage/dft/elements/DFTElement.h index 8a8a35d28..366d0fe91 100644 --- a/src/storage/dft/elements/DFTElement.h +++ b/src/storage/dft/elements/DFTElement.h @@ -93,10 +93,6 @@ namespace storm { return false; } - virtual bool isColdBasicElement() const { - return false; - } - /** * Returns true if the element is a spare gate */