From 0d3687cf5e89d629431d2cb6ed3d530e1d86ef88 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 18 Feb 2016 23:23:00 +0100 Subject: [PATCH] Refactored and sorted bitvector Former-commit-id: 28ca00af502f334cbb6a10c03277d3f39b592072 --- src/builder/ExplicitDFTModelBuilder.cpp | 43 ++++++++- src/builder/ExplicitDFTModelBuilder.h | 8 +- src/storage/dft/DFT.cpp | 100 ++++++++++++++++++--- src/storage/dft/DFT.h | 115 ++++++++++++++---------- src/storage/dft/DFTElements.h | 23 +---- src/storage/dft/DFTState.cpp | 72 ++++++++++----- src/storage/dft/DFTState.h | 16 ++-- 7 files changed, 261 insertions(+), 116 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 160535443..91a16f2d2 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -13,11 +13,52 @@ namespace storm { ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } + + template + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { + // stateSize is bound for size of bitvector + // 2^nrBE is upper bound for state space + + // Find symmetries + // TODO activate + // Currently using hack to test + std::vector> symmetries; + std::vector vecB; + std::vector vecC; + std::vector vecD; + if (false) { + for (size_t i = 0; i < mDft.nrElements(); ++i) { + std::string name = mDft.getElement(i)->name(); + size_t id = mDft.getElement(i)->id(); + if (boost::starts_with(name, "B")) { + vecB.push_back(id); + } else if (boost::starts_with(name, "C")) { + vecC.push_back(id); + } else if (boost::starts_with(name, "D")) { + vecD.push_back(id); + } + } + symmetries.push_back(vecB); + symmetries.push_back(vecC); + symmetries.push_back(vecD); + std::cout << "Found the following symmetries:" << std::endl; + for (auto const& symmetry : symmetries) { + for (auto const& elem : symmetry) { + std::cout << elem << " -> "; + } + std::cout << std::endl; + } + } else { + vecB.push_back(mDft.getTopLevelIndex()); + } + mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(vecB, symmetries)); + } + template std::shared_ptr> ExplicitDFTModelBuilder::buildModel() { // Initialize - DFTStatePointer state = std::make_shared>(mDft, newIndex++); + DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex++); mStates.findOrAdd(state->status(), state); std::queue stateQueue; diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 0b80608cf..eacf2568c 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -44,15 +44,13 @@ namespace storm { boost::optional>> choiceLabeling; }; - storm::storage::DFT const &mDft; + storm::storage::DFT const& mDft; + std::shared_ptr mStateGenerationInfo; storm::storage::BitVectorHashMap mStates; size_t newIndex = 0; public: - ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { - // stateSize is bound for size of bitvector - // 2^nrBE is upper bound for state space - } + ExplicitDFTModelBuilder(storm::storage::DFT const& dft); std::shared_ptr> buildModel(); diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 9506b29a5..62f7fe704 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -10,15 +10,18 @@ namespace storm { namespace storage { template - DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mTopLevelIndex(tle->id()), mNrOfBEs(0), mNrOfSpares(0) - { + DFT::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()) { assert(elementIndicesCorrect()); - mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; - size_t stateIndex = 0; + size_t stateVectorIndex = 0; + std::set tmpRepresentatives; + size_t usageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; + size_t nrRepresentatives = 0; for (auto& elem : mElements) { - mIdToFailureIndex.push_back(stateIndex); - stateIndex += 2; + stateVectorIndex += 2; + if (isRepresentative(elem->id())) { + ++nrRepresentatives; + } if(elem->isBasicElement()) { ++mNrOfBEs; } @@ -26,9 +29,7 @@ namespace storm { ++mNrOfSpares; bool firstChild = true; for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { - if(mActivationIndex.count(spareReprs->id()) == 0) { - mActivationIndex[spareReprs->id()] = stateIndex++; - } + tmpRepresentatives.insert(spareReprs->id()); std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); std::vector sparesAndBes; @@ -44,14 +45,13 @@ namespace storm { mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes)); firstChild = false; } - std::static_pointer_cast>(elem)->setUseIndex(stateIndex); - mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); - stateIndex += mUsageInfoBits; + stateVectorIndex += usageInfoBits; } else if (elem->isDependency()) { mDependencies.push_back(elem->id()); } } + stateVectorIndex += tmpRepresentatives.size(); // For the top module, we assume, contrary to [Jun15], that we have all spare gates and basic elements which are not in another module. std::set topModuleSet; @@ -68,12 +68,84 @@ namespace storm { } } mTopModule = std::vector(topModuleSet.begin(), topModuleSet.end()); - - mStateVectorSize = stateIndex; + + std::cout << tmpRepresentatives.size() << ", " << nrRepresentatives << std::endl; + std::cout << stateVectorIndex << ", " << (nrElements() * 2 + mNrOfSpares * usageInfoBits + tmpRepresentatives.size()) << std::endl; + assert(tmpRepresentatives.size() == nrRepresentatives); + assert(stateVectorIndex == nrElements() * 2 + mNrOfSpares * usageInfoBits + tmpRepresentatives.size()); + mStateVectorSize = stateVectorIndex; } + template + DFTStateGenerationInfo DFT::buildStateGenerationInfo(std::vector const& subTreeRoots, std::vector> const& symmetries) const { + // Use symmetry + // Collect all elements in the first subtree + // TODO make recursive to use for nested subtrees + + DFTStateGenerationInfo generationInfo(nrElements()); + + // Perform DFS and insert all elements of subtree sequentially + size_t stateIndex = 0; + std::queue visitQueue; + std::set visited; + visitQueue.push(subTreeRoots[0]); + bool consideredDependencies = false; + while (true) { + while (!visitQueue.empty()) { + size_t id = visitQueue.front(); + visitQueue.pop(); + if (visited.count(id) == 1) { + // Already visited + continue; + } + visited.insert(id); + DFTElementPointer element = mElements[id]; + + // Insert children + if (element->isGate()) { + for (auto const& child : std::static_pointer_cast>(element)->children()) { + visitQueue.push(child->id()); + } + } + + // Reserve bits for element + generationInfo.addStateIndex(id, stateIndex); + stateIndex += 2; + + if (isRepresentative(id)) { + generationInfo.addSpareActivationIndex(id, stateIndex); + ++stateIndex; + } + + if (element->isSpareGate()) { + generationInfo.addSpareUsageIndex(id, stateIndex); + stateIndex += generationInfo.usageInfoBits(); + } + + } + + if (consideredDependencies) { + break; + } + + // Consider dependencies + for (size_t idDependency : getDependencies()) { + std::shared_ptr const> dependency = getDependency(idDependency); + visitQueue.push(dependency->id()); + visitQueue.push(dependency->triggerEvent()->id()); + visitQueue.push(dependency->dependentEvent()->id()); + } + consideredDependencies = true; + } + assert(stateIndex = mStateVectorSize); + + STORM_LOG_TRACE(generationInfo); + + return generationInfo; } + + template std::string DFT::getElementsString() const { std::stringstream stream; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index ca860d074..015f26c7d 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -33,6 +33,69 @@ namespace storm { // Forward declarations template class DFTColouring; + + class DFTStateGenerationInfo { + private: + const size_t mUsageInfoBits; + 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 + + public: + + DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(storm::utility::math::uint64_log2(nrElements-1)+1), mIdToStateIndex(nrElements) { + } + + size_t usageInfoBits() const { + return mUsageInfoBits; + } + + void addStateIndex(size_t id, size_t index) { + assert(id < mIdToStateIndex.size()); + mIdToStateIndex[id] = index; + } + + void addSpareActivationIndex(size_t id, size_t index) { + mSpareActivationIndex[id] = index; + } + + void addSpareUsageIndex(size_t id, size_t index) { + mSpareUsageIndex[id] = index; + } + + size_t getStateIndex(size_t id) const { + assert(id < mIdToStateIndex.size()); + return mIdToStateIndex[id]; + } + + size_t getSpareUsageIndex(size_t id) const { + assert(mSpareUsageIndex.count(id) > 0); + return mSpareUsageIndex.at(id); + } + + size_t getSpareActivationIndex(size_t id) const { + assert(mSpareActivationIndex.count(id) > 0); + return mSpareActivationIndex.at(id); + } + + friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) { + os << "Id to state index:" << std::endl; + for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) { + os << id << " -> " << info.getStateIndex(id) << std::endl; + } + os << "Spare usage index with usage InfoBits of size " << info.mUsageInfoBits << ":" << std::endl; + for (auto pair : info.mSpareUsageIndex) { + os << pair.first << " -> " << pair.second << std::endl; + } + os << "Spare activation index:" << std::endl; + for (auto pair : info.mSpareActivationIndex) { + os << pair.first << " -> " << pair.second << std::endl; + } + return os; + } + + }; + /** * Represents a Dynamic Fault Tree @@ -52,18 +115,17 @@ namespace storm { size_t mNrOfBEs; size_t mNrOfSpares; size_t mTopLevelIndex; - size_t mUsageInfoBits; size_t mStateVectorSize; - std::map mActivationIndex; std::map> mSpareModules; std::vector mDependencies; std::vector mTopModule; - std::vector mIdToFailureIndex; - std::map mUsageIndex; - std::map mRepresentants; + std::map mRepresentants; // id element -> id representative + std::vector> mSymmetries; public: DFT(DFTElementVector const& elements, DFTElementPointer const& tle); + + DFTStateGenerationInfo buildStateGenerationInfo(std::vector const& subTreeRoots, std::vector> const& symmetries) const; size_t stateVectorSize() const { return mStateVectorSize; @@ -77,34 +139,8 @@ namespace storm { return mNrOfBEs; } - size_t usageInfoBits() const { - return mUsageInfoBits; - } - - size_t usageIndex(size_t id) const { - assert(mUsageIndex.find(id) != mUsageIndex.end()); - return mUsageIndex.find(id)->second; - } - - size_t failureIndex(size_t id) const { - return mIdToFailureIndex[id]; - } - - void initializeUses(DFTState& state) const { - for(auto const& elem : mElements) { - if(elem->isSpareGate()) { - std::static_pointer_cast>(elem)->initializeUses(state); - } - } - } - - void initializeActivation(DFTState& state) const { - state.activate(mTopLevelIndex); - for(auto const& elem : mTopModule) { - if(mElements[elem]->isSpareGate()) { - propagateActivation(state, state.uses(elem)); - } - } + size_t getTopLevelIndex() const { + return mTopLevelIndex; } std::vector getSpareIndices() const { @@ -130,15 +166,6 @@ namespace storm { return mDependencies; } - void propagateActivation(DFTState& state, size_t representativeId) const { - state.activate(representativeId); - for(size_t id : module(representativeId)) { - if(mElements[id]->isSpareGate()) { - propagateActivation(state, state.uses(id)); - } - } - } - std::vector nonColdBEs() const { std::vector result; for(DFTElementPointer elem : mElements) { @@ -170,10 +197,6 @@ namespace storm { return getElement(index)->isDependency(); } -// std::shared_ptr const> getGate(size_t index) const { -// return -// } - std::shared_ptr const> getBasicElement(size_t index) const { assert(isBasicElement(index)); return std::static_pointer_cast const>(mElements[index]); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 36075d005..db407fb85 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -898,10 +898,6 @@ namespace storm { template class DFTSpare : public DFTGate { - private: - size_t mUseIndex; - size_t mActiveIndex; - public: DFTSpare(size_t id, std::string const& name, std::vector>> const& children = {}) : DFTGate(id, name, children) @@ -919,24 +915,11 @@ namespace storm { return true; } - void setUseIndex(size_t useIndex) { - mUseIndex = useIndex; - } - - void setActiveIndex(size_t activeIndex) { - mActiveIndex = activeIndex; - } - - void initializeUses(storm::storage::DFTState& state) { - assert(this->mChildren.size() > 0); - state.setUsesAtPosition(mUseIndex, this->mChildren[0]->id()); - } - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if(state.isOperational(this->mId)) { - size_t uses = state.extractUses(mUseIndex); + size_t uses = state.uses(this->mId); if(!state.isOperational(uses)) { - bool claimingSuccessful = state.claimNew(this->mId, mUseIndex, uses, this->mChildren); + bool claimingSuccessful = state.claimNew(this->mId, uses, this->mChildren); if(!claimingSuccessful) { this->fail(state, queues); } @@ -946,7 +929,7 @@ namespace storm { void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if(state.isOperational(this->mId)) { - if(state.isFailsafe(state.extractUses((mUseIndex)))) { + if(state.isFailsafe(state.uses(this->mId))) { this->failsafe(state, queues); this->childrenDontCare(state, queues); } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 7e8429fdd..c3f7c9f32 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -6,10 +6,25 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft) { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { mInactiveSpares = dft.getSpareIndices(); - dft.initializeUses(*this); - dft.initializeActivation(*this); + + // Initialize uses + for(size_t id : mDft.getSpareIndices()) { + std::shared_ptr const> elem = mDft.getGate(id); + assert(elem->isSpareGate()); + assert(elem->nrChildren() > 0); + this->setUses(id, elem->children()[0]->id()); + } + + // Initialize activation + this->activate(mDft.getTopLevelIndex()); + for(auto const& id : mDft.module(mDft.getTopLevelIndex())) { + if(mDft.getElement(id)->isSpareGate()) { + propagateActivation(uses(id)); + } + } + std::vector alwaysActiveBEs = dft.nonColdBEs(); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); } @@ -26,7 +41,7 @@ namespace storm { template int DFTState::getElementStateInt(size_t id) const { - return mStatus.getAsInt(mDft.failureIndex(id), 2); + return mStatus.getAsInt(mStateGenerationInfo.getStateIndex(id), 2); } template @@ -46,12 +61,12 @@ namespace storm { template bool DFTState::hasFailed(size_t id) const { - return mStatus[mDft.failureIndex(id)]; + return mStatus[mStateGenerationInfo.getStateIndex(id)]; } template bool DFTState::isFailsafe(size_t id) const { - return mStatus[mDft.failureIndex(id)+1]; + return mStatus[mStateGenerationInfo.getStateIndex(id)+1]; } template @@ -66,38 +81,38 @@ namespace storm { template bool DFTState::dependencySuccessful(size_t id) const { - return mStatus[mDft.failureIndex(id)]; + return mStatus[mStateGenerationInfo.getStateIndex(id)]; } template bool DFTState::dependencyUnsuccessful(size_t id) const { - return mStatus[mDft.failureIndex(id)+1]; + return mStatus[mStateGenerationInfo.getStateIndex(id)+1]; } template void DFTState::setFailed(size_t id) { - mStatus.set(mDft.failureIndex(id)); + mStatus.set(mStateGenerationInfo.getStateIndex(id)); } template void DFTState::setFailsafe(size_t id) { - mStatus.set(mDft.failureIndex(id)+1); + mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); } template void DFTState::setDontCare(size_t id) { - mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast(DFTElementState::DontCare) ); + mStatus.setFromInt(mStateGenerationInfo.getStateIndex(id), 2, static_cast(DFTElementState::DontCare) ); } template void DFTState::setDependencySuccessful(size_t id) { // No distinction between successful dependency and no dependency at all - // -> we do not set bit - //mStatus.set(mDft.failureIndex(id)); + // => we do not set bit + //mStatus.set(mStateGenerationInfo.mIdToStateIndex(id)); } template void DFTState::setDependencyUnsuccessful(size_t id) { - mStatus.set(mDft.failureIndex(id)+1); + mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); } template @@ -157,8 +172,7 @@ namespace storm { template void DFTState::activate(size_t repr) { - std::vector const& module = mDft.module(repr); - for(size_t elem : module) { + for(size_t elem : mDft.module(repr)) { if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { mIsCurrentlyFailableBE.push_back(elem); } @@ -174,16 +188,26 @@ namespace storm { assert(mDft.getElement(id)->isSpareGate()); return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end()); } + + template + void DFTState::propagateActivation(size_t representativeId) { + activate(representativeId); + for(size_t id : mDft.module(representativeId)) { + if(mDft.getElement(id)->isSpareGate()) { + propagateActivation(uses(id)); + } + } + } template uint_fast64_t DFTState::uses(size_t id) const { - return extractUses(mDft.usageIndex(id)); + return extractUses(mStateGenerationInfo.getSpareUsageIndex(id)); } template uint_fast64_t DFTState::extractUses(size_t from) const { - assert(mDft.usageInfoBits() < 64); - return mStatus.getAsInt(from, mDft.usageInfoBits()); + assert(mStateGenerationInfo.usageInfoBits() < 64); + return mStatus.getAsInt(from, mStateGenerationInfo.usageInfoBits()); } template @@ -192,13 +216,13 @@ namespace storm { } template - void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) { - mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child); + void DFTState::setUses(size_t spareId, size_t child) { + mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), child); mUsedRepresentants.push_back(child); } template - bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector>> const& children) { + bool DFTState::claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children) { auto it = children.begin(); while ((*it)->id() != currentlyUses) { assert(it != children.end()); @@ -208,9 +232,9 @@ namespace storm { while(it != children.end()) { size_t childId = (*it)->id(); if(!hasFailed(childId) && !isUsed(childId)) { - setUsesAtPosition(usageIndex, childId); + setUses(spareId, childId); if(isActiveSpare(spareId)) { - mDft.propagateActivation(*this, childId); + propagateActivation(childId); } return true; } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 450953bd7..fcbcdc62d 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -17,6 +17,7 @@ namespace storm { class DFTBE; template class DFTElement; + class DFTStateGenerationInfo; template class DFTState { @@ -31,9 +32,10 @@ namespace storm { std::vector mUsedRepresentants; bool mValid = true; const DFT& mDft; + const DFTStateGenerationInfo& mStateGenerationInfo; public: - DFTState(DFT const& dft, size_t id); + DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id); DFTElementState getElementState(size_t id) const; @@ -75,6 +77,8 @@ namespace storm { bool isActiveSpare(size_t id) const; + void propagateActivation(size_t representativeId); + void markAsInvalid() { mValid = false; } @@ -109,13 +113,13 @@ namespace storm { bool isUsed(size_t child) const; /** - * Sets to to the usageIndex which child is now used. - * @param usageIndex - * @param child + * Sets for the spare which child is now used. + * @param spareId Id of the spare + * @param child Id of the child which is now used */ - void setUsesAtPosition(size_t usageIndex, size_t child); + void setUses(size_t spareId, size_t child); - bool claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector>> const& children); + bool claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children); bool hasOutgoingEdges() const { return !mIsCurrentlyFailableBE.empty();