From 5b6dcd0eed4fb795c810ab41f947ccb2fb57af92 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 24 Feb 2016 18:14:18 +0100 Subject: [PATCH] UsageIndex is number of used child now Former-commit-id: 629aeae3182982c94900a8b890f4a1b81ac8021c --- examples/dft/spare_symmetry.dft | 9 +++++++++ src/storage/dft/DFT.cpp | 29 +++++++++++++++++++++++++---- src/storage/dft/DFT.h | 12 +++++++++++- src/storage/dft/DFTElements.h | 4 ++-- src/storage/dft/DFTState.cpp | 15 +++++++++++++-- src/storage/dft/DFTState.h | 11 +++++++++-- 6 files changed, 69 insertions(+), 11 deletions(-) create mode 100644 examples/dft/spare_symmetry.dft diff --git a/examples/dft/spare_symmetry.dft b/examples/dft/spare_symmetry.dft new file mode 100644 index 000000000..04b5c253b --- /dev/null +++ b/examples/dft/spare_symmetry.dft @@ -0,0 +1,9 @@ +toplevel "A"; +"A" and "B" "C"; +"B" wsp "I" "J"; +"C" wsp "K" "L"; +"I" lambda=0.5 dorm=0.3; +"J" lambda=0.5 dorm=0.3; +"K" lambda=0.5 dorm=0.3; +"L" lambda=0.5 dorm=0.3; + diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index eef83928d..2924789fd 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -11,7 +11,7 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()) { + DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { assert(elementIndicesCorrect()); size_t nrRepresentatives = 0; @@ -25,6 +25,7 @@ namespace storm { else if (elem->isSpareGate()) { ++mNrOfSpares; bool firstChild = true; + mMaxSpareChildCount = std::max(mMaxSpareChildCount, std::static_pointer_cast>(elem)->children().size()); for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); @@ -63,7 +64,9 @@ namespace storm { } mTopModule = std::vector(topModuleSet.begin(), topModuleSet.end()); - size_t usageInfoBits = mElements.size() > 1 ? storm::utility::math::uint64_log2(mElements.size()-1) + 1 : 1; + //Reserve space for failed spares + ++mMaxSpareChildCount; + size_t usageInfoBits = storm::utility::math::uint64_log2(mMaxSpareChildCount) + 1; mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives; } @@ -73,7 +76,7 @@ namespace storm { // Collect all elements in the first subtree // TODO make recursive to use for nested subtrees - DFTStateGenerationInfo generationInfo(nrElements()); + DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount); // Perform DFS and insert all elements of subtree sequentially size_t stateIndex = 0; @@ -296,7 +299,25 @@ namespace storm { } return stream.str(); } - + + template + size_t DFT::getChild(size_t spareId, size_t nrUsedChild) const { + assert(mElements[spareId]->isSpareGate()); + return getGate(spareId)->children()[nrUsedChild]->id(); + } + + template + size_t DFT::getNrChild(size_t spareId, size_t childId) const { + assert(mElements[spareId]->isSpareGate()); + DFTElementVector children = getGate(spareId)->children(); + for (size_t nrChild = 0; nrChild < children.size(); ++nrChild) { + if (children[nrChild]->id() == childId) { + return nrChild; + } + } + assert(false); + } + template std::vector DFT::getIndependentSubDftRoots(size_t index) const { auto elem = getElement(index); diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 453db1443..48bb60f68 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -45,7 +45,8 @@ namespace storm { public: - DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(nrElements > 1 ? storm::utility::math::uint64_log2(nrElements-1) + 1 : 1), mIdToStateIndex(nrElements) { + DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), mIdToStateIndex(nrElements) { + assert(maxSpareChildCount < pow(2, mUsageInfoBits)); } size_t usageInfoBits() const { @@ -144,6 +145,7 @@ namespace storm { size_t mNrOfSpares; size_t mTopLevelIndex; size_t mStateVectorSize; + size_t mMaxSpareChildCount; std::map> mSpareModules; std::vector mDependencies; std::vector mTopModule; @@ -175,6 +177,10 @@ namespace storm { return mTopLevelIndex; } + size_t getMaxSpareChildCount() const { + return mMaxSpareChildCount; + } + std::vector getSpareIndices() const { std::vector indices; for(auto const& elem : mElements) { @@ -288,6 +294,10 @@ namespace storm { return storm::storage::DFTState::isFailsafe(state, stateGenerationInfo.getStateIndex(mTopLevelIndex)); } + size_t getChild(size_t spareId, size_t nrUsedChild) const; + + size_t getNrChild(size_t spareId, size_t childId) const; + std::string getElementsString() const; std::string getInfoString() const; diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 3236a5551..48318d0ae 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -412,12 +412,12 @@ namespace storm { } /** - * Finish failed/failsafe spare gate by activating the children and setting the useIndex to the spare id. + * Finish failed/failsafe spare gate by activating the children and setting the useIndex to the maximum value. * This prevents multiple fail states with different usages or activations. * @param state The current state. */ void finalizeSpare(DFTState& state) const { - state.setUses(this->mId, this->mId); + state.finalizeUses(this->mId); for (auto child : this->children()) { if (!state.isActive(child->id())) { state.activate(child->id()); diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index be5c33060..8af84255c 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -201,7 +201,12 @@ namespace storm { template uint_fast64_t DFTState::uses(size_t id) const { - return extractUses(mStateGenerationInfo.getSpareUsageIndex(id)); + size_t nrUsedChild = extractUses(mStateGenerationInfo.getSpareUsageIndex(id)); + if (nrUsedChild == mDft.getMaxSpareChildCount()) { + return id; + } else { + return mDft.getChild(id, nrUsedChild); + } } template @@ -217,9 +222,15 @@ namespace storm { template void DFTState::setUses(size_t spareId, size_t child) { - mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), child); + mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getNrChild(spareId, child)); mUsedRepresentants.push_back(child); } + + template + void DFTState::finalizeUses(size_t spareId) { + assert(hasFailed(spareId)); + mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount()); + } template bool DFTState::claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children) { diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index eccf7f01d..ea874cf1b 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -93,9 +93,10 @@ namespace storm { } /** - * This method gets the usage information for a spare + * This method returns the id of the used child for a spare. If no element is used, it returns the given id. * @param id Id of the spare - * @return The child that currently is used. + * @return The id of the currently used child or if non is used (because of spare failure) the id of + * the spare. */ uint_fast64_t uses(size_t id) const; @@ -120,6 +121,12 @@ namespace storm { */ void setUses(size_t spareId, size_t child); + /** + * Sets the use for the spare to a default value to gain consistent states after failures. + * @param spareId Id of the spare + */ + void finalizeUses(size_t spareId); + bool claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children); bool hasOutgoingEdges() const {