From 3033d5444caf8ec084fb87f55ed2f73a92c5ee8e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 29 May 2019 18:22:24 +0200 Subject: [PATCH] Refactoring --- src/storm-dft/storage/dft/DFT.cpp | 10 ++-- src/storm-dft/storage/dft/DFT.h | 1 + .../storage/dft/DFTStateGenerationInfo.h | 49 ++++++++++++++----- 3 files changed, 43 insertions(+), 17 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 28b7d29d0..3e6bb8570 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -17,14 +17,13 @@ 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) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mNrRepresentatives(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) { // Check that ids correspond to indices in the element vector STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect."); - size_t nrRepresentatives = 0; for (auto& elem : mElements) { if (isRepresentative(elem->id())) { - ++nrRepresentatives; + ++mNrRepresentatives; } if(elem->isBasicElement()) { ++mNrOfBEs; @@ -81,13 +80,12 @@ namespace storm { //Reserve space for failed spares ++mMaxSpareChildCount; - size_t usageInfoBits = storm::utility::math::uint64_log2(mMaxSpareChildCount) + 1; - mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives; + mStateVectorSize = DFTStateGenerationInfo::getStateVectorSize(nrElements(), mNrOfSpares, mNrRepresentatives, mMaxSpareChildCount); } template DFTStateGenerationInfo DFT::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const { - DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount); + DFTStateGenerationInfo generationInfo(nrElements(), mNrOfSpares, mNrRepresentatives, mMaxSpareChildCount); // Generate Pre and Post info for restrictions, and mutexes for(auto const& elem : mElements) { diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 5c885ef59..53f901408 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -58,6 +58,7 @@ namespace storm { DFTElementVector mElements; size_t mNrOfBEs; size_t mNrOfSpares; + size_t mNrRepresentatives; size_t mTopLevelIndex; size_t mStateVectorSize; size_t mMaxSpareChildCount; diff --git a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h index ec2ed993a..7055d6682 100644 --- a/src/storm-dft/storage/dft/DFTStateGenerationInfo.h +++ b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h @@ -5,36 +5,59 @@ namespace storm { class DFTStateGenerationInfo { private: const size_t mUsageInfoBits; + const size_t stateIndexSize; std::map mSpareUsageIndex; // id spare -> index first bit in state std::map mSpareActivationIndex; // id spare representative -> index in state std::vector mIdToStateIndex; // id -> index first bit in state std::map> mSeqRestrictionPreElements; // id -> list of restriction pre elements std::map> mSeqRestrictionPostElements; // id -> list of restriction post elements - std::map> mMutexRestrictionElements; // id -> list of elments in the same mutexes + std::map> mMutexRestrictionElements; // id -> list of elements in the same mutexes std::vector>> mSymmetries; // pair (length of symmetry group, vector indicating the starting points of the symmetry groups) public: - DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : - mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), - mIdToStateIndex(nrElements) - { + DFTStateGenerationInfo(size_t nrElements, size_t nrOfSpares, size_t nrRepresentatives, size_t maxSpareChildCount) : + mUsageInfoBits(getUsageInfoBits(maxSpareChildCount)), + stateIndexSize(getStateVectorSize(nrElements, nrOfSpares, nrRepresentatives, maxSpareChildCount)), + mIdToStateIndex(nrElements) { STORM_LOG_ASSERT(maxSpareChildCount < pow(2, mUsageInfoBits), "Bit length incorrect."); } + /*! + * Get number of bits required to store claiming information for spares in binary format. + * @param maxSpareChildCount Maximal number of children of a spare. + * @return Number of bits required to store claiming information. + */ + static size_t getUsageInfoBits(size_t maxSpareChildCount) { + return storm::utility::math::uint64_log2(maxSpareChildCount) + 1; + } + + /*! + * Get length of BitVector capturing DFT state. + * @param nrElements Number of DFT elements. + * @param nrOfSpares Number of Spares (needed for claiming). + * @param nrRepresentatives Number of representatives (needed for activation). + * @param maxSpareChildCount Maximal number of children of a spare. + * @return Length of required BitVector. + */ + static size_t getStateVectorSize(size_t nrElements, size_t nrOfSpares, size_t nrRepresentatives, size_t maxSpareChildCount) { + return nrElements * 2 + nrOfSpares * getUsageInfoBits(maxSpareChildCount) + nrRepresentatives; + } + size_t usageInfoBits() const { return mUsageInfoBits; } void addStateIndex(size_t id, size_t index) { STORM_LOG_ASSERT(id < mIdToStateIndex.size(), "Id invalid."); + STORM_LOG_ASSERT(index < stateIndexSize, "Index invalid"); mIdToStateIndex[id] = index; } void setRestrictionPreElements(size_t id, std::vector const& elems) { mSeqRestrictionPreElements[id] = elems; } - + void setRestrictionPostElements(size_t id, std::vector const& elems) { mSeqRestrictionPostElements[id] = elems; } @@ -47,7 +70,7 @@ namespace storm { STORM_LOG_ASSERT(mSeqRestrictionPreElements.count(index) > 0, "Index invalid."); return mSeqRestrictionPreElements.at(index); } - + std::vector const& seqRestrictionPostElements(size_t index) const { STORM_LOG_ASSERT(mSeqRestrictionPostElements.count(index) > 0, "Index invalid."); return mSeqRestrictionPostElements.at(index); @@ -57,12 +80,14 @@ namespace storm { STORM_LOG_ASSERT(mMutexRestrictionElements.count(index) > 0, "Index invalid."); return mMutexRestrictionElements.at(index); } - + void addSpareActivationIndex(size_t id, size_t index) { + STORM_LOG_ASSERT(index < stateIndexSize, "Index invalid"); mSpareActivationIndex[id] = index; } void addSpareUsageIndex(size_t id, size_t index) { + STORM_LOG_ASSERT(index < stateIndexSize, "Index invalid"); mSpareUsageIndex[id] = index; } @@ -84,7 +109,7 @@ namespace storm { void addSymmetry(size_t length, std::vector& startingIndices) { mSymmetries.push_back(std::make_pair(length, startingIndices)); } - + /** * Generate more symmetries by combining two symmetries */ @@ -94,7 +119,7 @@ namespace storm { size_t childStart = mSymmetries[i].second[0]; size_t childLength = mSymmetries[i].first; // Iterate over possible parents - for (size_t j = i+1; j < mSymmetries.size(); ++j) { + for (size_t j = i + 1; j < mSymmetries.size(); ++j) { size_t parentStart = mSymmetries[j].second[0]; size_t parentLength = mSymmetries[j].first; // Check if child lies in parent @@ -122,7 +147,7 @@ namespace storm { size_t getSymmetrySize() const { return mSymmetries.size(); } - + bool hasSymmetries() const { return !mSymmetries.empty(); } @@ -138,6 +163,8 @@ namespace storm { } friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) { + os << "StateGenerationInfo:" << std::endl; + os << "Length of state vector: " << info.stateIndexSize << std::endl; os << "Id to state index:" << std::endl; for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) { os << id << " -> " << info.getStateIndex(id) << std::endl;