From 69a464d5ef6d3ed3187b3291f8acfd25560e9c5a Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 1 Feb 2016 18:45:18 +0100 Subject: [PATCH] Changed unordered_set to BitVectorHashMap for DFTState Former-commit-id: 35f57aa25040796690fadc21d764f53efb103be4 --- src/builder/ExplicitDFTModelBuilder.cpp | 66 ++++++++++++------------- src/builder/ExplicitDFTModelBuilder.h | 11 +++-- src/storage/BitVectorHashMap.cpp | 7 +++ src/storage/dft/DFT.cpp | 18 +++---- src/storage/dft/DFT.h | 13 ++--- 5 files changed, 63 insertions(+), 52 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 10534d0a5..1b777fb54 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -14,10 +14,10 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilder::buildCTMC() { // Initialize - storm::storage::DFTState state(mDft, newIndex++); - mStates.insert(state); + DFTStatePointer state = std::make_shared>(mDft, newIndex++); + mStates.findOrAdd(state->status(), state); - std::queue> stateQueue; + std::queue stateQueue; stateQueue.push(state); bool deterministicModel = true; @@ -47,17 +47,18 @@ namespace storm { modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); } - for (storm::storage::DFTState state : mStates) { + for (auto const& stateVectorPair : mStates) { + DFTStatePointer state = stateVectorPair.second; if (mDft.hasFailed(state)) { - modelComponents.stateLabeling.addLabelToState("failed", state.getId()); + modelComponents.stateLabeling.addLabelToState("failed", state->getId()); } if (mDft.isFailsafe(state)) { - modelComponents.stateLabeling.addLabelToState("failsafe", state.getId()); + modelComponents.stateLabeling.addLabelToState("failsafe", state->getId()); }; // Set fail status for each BE for (std::shared_ptr> elem : basicElements) { - if (state.hasFailed(elem->id())) { - modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state.getId()); + if (state->hasFailed(elem->id())) { + modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", state->getId()); } } } @@ -69,7 +70,7 @@ namespace storm { } template - void ExplicitDFTModelBuilder::exploreStates(std::queue>& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder) { + void ExplicitDFTModelBuilder::exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder) { std::map outgoingTransitions; @@ -79,25 +80,26 @@ namespace storm { ValueType sum = storm::utility::zero(); // Consider next state - storm::storage::DFTState state = stateQueue.front(); + DFTStatePointer state = stateQueue.front(); stateQueue.pop(); size_t smallest = 0; // Add self loop for target states if (mDft.hasFailed(state) || mDft.isFailsafe(state)) { - transitionMatrixBuilder.addNextValue(state.getId(), state.getId(), storm::utility::one()); - STORM_LOG_TRACE("Added self loop for " << state.getId()); + transitionMatrixBuilder.addNextValue(state->getId(), state->getId(), storm::utility::one()); + STORM_LOG_TRACE("Added self loop for " << state->getId()); // No further exploration required continue; } // Let BE fail - while (smallest < state.nrFailableBEs()) { + while (smallest < state->nrFailableBEs()) { STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state)); - storm::storage::DFTState newState(state); - std::pair>, bool> nextBEPair = newState.letNextBEFail(smallest++); + // Construct new state as copy from original one + DFTStatePointer newState = std::make_shared>(*state); + std::pair>, bool> nextBEPair = newState->letNextBEFail(smallest++); std::shared_ptr> nextBE = nextBEPair.first; if (nextBE == nullptr) { break; @@ -107,57 +109,55 @@ namespace storm { storm::storage::DFTStateSpaceGenerationQueues queues; for (DFTGatePointer parent : nextBE->parents()) { - if (newState.isOperational(parent->id())) { + if (newState->isOperational(parent->id())) { queues.propagateFailure(parent); } } while (!queues.failurePropagationDone()) { DFTGatePointer next = queues.nextFailurePropagation(); - next->checkFails(newState, queues); + next->checkFails(*newState, queues); } while (!queues.failsafePropagationDone()) { DFTGatePointer next = queues.nextFailsafePropagation(); - next->checkFailsafe(newState, queues); + next->checkFailsafe(*newState, queues); } while (!queues.dontCarePropagationDone()) { DFTElementPointer next = queues.nextDontCarePropagation(); - next->checkDontCareAnymore(newState, queues); + next->checkDontCareAnymore(*newState, queues); } - auto itState = mStates.find(newState); - if (itState == mStates.end()) { + if (mStates.contains(newState->status())) { + // State already exists + newState = mStates.findOrAdd(newState->status(), newState); + STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists"); + } else { // New state - newState.setId(newIndex++); - auto itInsert = mStates.insert(newState); - assert(itInsert.second); - itState = itInsert.first; + newState->setId(newIndex++); + mStates.findOrAdd(newState->status(), newState); STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); // Add state to search stateQueue.push(newState); - } else { - // State already exists - STORM_LOG_TRACE("State " << mDft.getStateString(*itState) << " already exists"); } // Set failure rate according to usage bool isUsed = true; if (mDft.hasRepresentant(nextBE->id())) { DFTElementPointer representant = mDft.getRepresentant(nextBE->id()); - isUsed = newState.isUsed(representant->id()); + isUsed = newState->isUsed(representant->id()); } STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); - auto resultFind = outgoingTransitions.find(itState->getId()); + auto resultFind = outgoingTransitions.find(newState->getId()); if (resultFind != outgoingTransitions.end()) { // Add to existing transition resultFind->second += rate; } else { // Insert new transition - outgoingTransitions.insert(std::make_pair(itState->getId(), rate)); + outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); } sum += rate; } // end while failing BE @@ -167,8 +167,8 @@ namespace storm { { // TODO Matthias: correct? ValueType rate = it->second;// / sum; - transitionMatrixBuilder.addNextValue(state.getId(), it->first, rate); - STORM_LOG_TRACE("Added transition from " << state.getId() << " to " << it->first << " with " << rate); + transitionMatrixBuilder.addNextValue(state->getId(), it->first, rate); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << it->first << " with " << rate); } } // end while queue diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index 8148559c3..ed02e60d4 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -7,6 +7,7 @@ #include #include #include +#include #include #include #include @@ -20,6 +21,7 @@ namespace storm { using DFTElementPointer = std::shared_ptr>; using DFTGatePointer = std::shared_ptr>; + using DFTStatePointer = std::shared_ptr>; // A structure holding the individual components of a model. struct ModelComponents { @@ -39,18 +41,19 @@ namespace storm { }; storm::storage::DFT const &mDft; - std::unordered_set> mStates; + storm::storage::BitVectorHashMap mStates; size_t newIndex = 0; public: - ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) { - + ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft), mStates(((mDft.stateSize() / 64) + 1) * 64, std::pow(2, mDft.nrBasicElements())) { + // stateSize is bound for size of bitvector + // 2^nrBE is upper bound for state space } std::shared_ptr> buildCTMC(); private: - void exploreStates(std::queue>& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder); + void exploreStates(std::queue& stateQueue, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder); }; } diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 9237dfde3..be0e32325 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -4,6 +4,9 @@ #include "src/utility/macros.h" +#include "src/storage/dft/DFTState.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace storage { template @@ -240,5 +243,9 @@ namespace storm { template class BitVectorHashMap; template class BitVectorHashMap; + template class BitVectorHashMap>>; +#ifdef STORM_HAVE_CARL + template class BitVectorHashMap>>; +#endif } } diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index ae4ec62eb..c36f0a9e0 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -109,17 +109,17 @@ namespace storm { } template - std::string DFT::getElementsWithStateString(DFTState const& state) const{ + std::string DFT::getElementsWithStateString(DFTStatePointer const& state) const{ std::stringstream stream; for (auto const& elem : mElements) { stream << "[" << elem->id() << "]"; stream << elem->toString(); - stream << "\t** " << state.getElementState(elem->id()); + stream << "\t** " << state->getElementState(elem->id()); if(elem->isSpareGate()) { - if(state.isActiveSpare(elem->id())) { + if(state->isActiveSpare(elem->id())) { stream << " actively"; } - stream << " using " << state.uses(elem->id()); + stream << " using " << state->uses(elem->id()); } stream << std::endl; } @@ -127,16 +127,16 @@ namespace storm { } template - std::string DFT::getStateString(DFTState const& state) const{ + std::string DFT::getStateString(DFTStatePointer const& state) const{ std::stringstream stream; - stream << "(" << state.getId() << ") "; + stream << "(" << state->getId() << ") "; for (auto const& elem : mElements) { - stream << state.getElementStateInt(elem->id()); + stream << state->getElementStateInt(elem->id()); if(elem->isSpareGate()) { - if(state.isActiveSpare(elem->id())) { + if(state->isActiveSpare(elem->id())) { stream << " actively"; } - stream << " using " << state.uses(elem->id()); + stream << " using " << state->uses(elem->id()); } } return stream.str(); diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 17d6c7fd5..81cfdf99b 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -37,6 +37,7 @@ namespace storm { using DFTElementVector = std::vector; using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; + using DFTStatePointer = std::shared_ptr>; private: DFTElementVector mElements; @@ -164,12 +165,12 @@ namespace storm { return getElement(mRepresentants.find(id)->second); } - bool hasFailed(DFTState const& state) const { - return state.hasFailed(mTopLevelIndex); + bool hasFailed(DFTStatePointer const& state) const { + return state->hasFailed(mTopLevelIndex); } - bool isFailsafe(DFTState const& state) const { - return state.isFailsafe(mTopLevelIndex); + bool isFailsafe(DFTStatePointer const& state) const { + return state->isFailsafe(mTopLevelIndex); } std::string getElementsString() const; @@ -178,9 +179,9 @@ namespace storm { std::string getSpareModulesString() const; - std::string getElementsWithStateString(DFTState const& state) const; + std::string getElementsWithStateString(DFTStatePointer const& state) const; - std::string getStateString(DFTState const& state) const; + std::string getStateString(DFTStatePointer const& state) const; private: bool elementIndicesCorrect() const {