From d160bb1b134784612d0d6a1508102c803a3bcff4 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 19 Feb 2016 15:47:16 +0100 Subject: [PATCH] Use only state ids instead of complete data structure Former-commit-id: 0852cce6d7ba5e7c6b35630ffdb2631cecf64534 --- src/builder/ExplicitDFTModelBuilder.cpp | 65 +++++++++++++------------ src/builder/ExplicitDFTModelBuilder.h | 4 +- src/storage/BitVectorHashMap.cpp | 8 +-- src/storage/dft/DFT.cpp | 1 + src/storage/dft/DFT.h | 8 +++ src/storage/dft/DFTState.cpp | 10 ++++ src/storage/dft/DFTState.h | 8 ++- 7 files changed, 62 insertions(+), 42 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index a7284cb9c..2d466dec8 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -15,14 +15,13 @@ namespace storm { } 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 + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE) { + // stateVectorSize is bound for size of bitvector // Find symmetries // TODO activate // Currently using hack to test - std::vector> symmetries; + std::vector> symmetriesTmp; std::vector vecB; std::vector vecC; std::vector vecD; @@ -38,11 +37,11 @@ namespace storm { vecD.push_back(id); } } - symmetries.push_back(vecB); - symmetries.push_back(vecC); - symmetries.push_back(vecD); + symmetriesTmp.push_back(vecB); + symmetriesTmp.push_back(vecC); + symmetriesTmp.push_back(vecD); std::cout << "Found the following symmetries:" << std::endl; - for (auto const& symmetry : symmetries) { + for (auto const& symmetry : symmetriesTmp) { for (auto const& elem : symmetry) { std::cout << elem << " -> "; } @@ -51,7 +50,7 @@ namespace storm { } else { vecB.push_back(mDft.getTopLevelIndex()); } - mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(vecB, symmetries)); + mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(vecB, symmetriesTmp)); } @@ -59,7 +58,7 @@ namespace storm { std::shared_ptr> ExplicitDFTModelBuilder::buildModel() { // Initialize DFTStatePointer state = std::make_shared>(mDft, *mStateGenerationInfo, newIndex++); - mStates.findOrAdd(state->status(), state); + mStates.findOrAdd(state->status(), state->getId()); std::queue stateQueue; stateQueue.push(state); @@ -97,18 +96,19 @@ namespace storm { modelComponents.stateLabeling.addLabel(elem->name() + "_fail"); } - for (auto const& stateVectorPair : mStates) { - DFTStatePointer state = stateVectorPair.second; - if (mDft.hasFailed(state)) { - modelComponents.stateLabeling.addLabelToState("failed", state->getId()); + for (auto const& stateIdPair : mStates) { + storm::storage::BitVector state = stateIdPair.first; + size_t stateId = stateIdPair.second; + if (mDft.hasFailed(state, *mStateGenerationInfo)) { + modelComponents.stateLabeling.addLabelToState("failed", stateId); } - if (mDft.isFailsafe(state)) { - modelComponents.stateLabeling.addLabelToState("failsafe", state->getId()); + if (mDft.isFailsafe(state, *mStateGenerationInfo)) { + modelComponents.stateLabeling.addLabelToState("failsafe", stateId); }; // 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 (storm::storage::DFTState::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id()))) { + modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId); } } } @@ -213,15 +213,16 @@ namespace storm { // Update failable dependencies newState->updateFailableDependencies(nextBE->id()); - + + size_t newStateId; if (mStates.contains(newState->status())) { // State already exists - newState = mStates.findOrAdd(newState->status(), newState); + newStateId = mStates.getValue(newState->status()); STORM_LOG_TRACE("State " << mDft.getStateString(newState) << " already exists"); } else { // New state newState->setId(newIndex++); - mStates.findOrAdd(newState->status(), newState); + newStateId = mStates.findOrAdd(newState->status(), newState->getId()); STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); // Add state to search queue @@ -232,22 +233,22 @@ namespace storm { if (hasDependencies) { // Failure is due to dependency -> add non-deterministic choice std::shared_ptr const> dependency = mDft.getDependency(state->getDependencyId(smallest-1)); - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, newState->getId(), dependency->probability()); - STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with probability " << dependency->probability()); + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, newStateId, dependency->probability()); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newStateId << " with probability " << dependency->probability()); if (!storm::utility::isOne(dependency->probability())) { // Add transition to state where dependency was unsuccessful DFTStatePointer unsuccessfulState = std::make_shared>(*state); unsuccessfulState->letDependencyBeUnsuccessful(smallest-1); - + size_t unsuccessfulStateId; if (mStates.contains(unsuccessfulState->status())) { // Unsuccessful state already exists - unsuccessfulState = mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState); + unsuccessfulStateId = mStates.getValue(unsuccessfulState->status()); STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists"); } else { // New unsuccessful state unsuccessfulState->setId(newIndex++); - mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState); + unsuccessfulStateId = mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState->getId()); STORM_LOG_TRACE("New state " << mDft.getStateString(unsuccessfulState)); // Add unsuccessful state to search queue @@ -255,11 +256,11 @@ namespace storm { } ValueType remainingProbability = storm::utility::one() - dependency->probability(); - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, unsuccessfulState->getId(), remainingProbability); - STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << unsuccessfulState->getId() << " with probability " << remainingProbability); + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, unsuccessfulStateId, remainingProbability); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << unsuccessfulStateId << " with probability " << remainingProbability); } else { // Self-loop with probability one cannot be eliminated later one. - assert(state->getId() != newState->getId()); + assert(state->getId() != newStateId); } ++rowOffset; @@ -274,15 +275,15 @@ namespace storm { } STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); - auto resultFind = outgoingTransitions.find(newState->getId()); + auto resultFind = outgoingTransitions.find(newStateId); if (resultFind != outgoingTransitions.end()) { // Add to existing transition resultFind->second += rate; STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second); } else { // Insert new transition - outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); - STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with rate " << rate); + outgoingTransitions.insert(std::make_pair(newStateId, rate)); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newStateId << " with rate " << rate); } exitRate += rate; } diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index eacf2568c..322790aa4 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -43,10 +43,12 @@ namespace storm { // A vector that stores a labeling for each choice. boost::optional>> choiceLabeling; }; + + const size_t INITIAL_BUCKETSIZE = 20000; storm::storage::DFT const& mDft; std::shared_ptr mStateGenerationInfo; - storm::storage::BitVectorHashMap mStates; + storm::storage::BitVectorHashMap mStates; size_t newIndex = 0; public: diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index be0e32325..4d6238350 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -4,9 +4,6 @@ #include "src/utility/macros.h" -#include "src/storage/dft/DFTState.h" -#include "src/adapters/CarlAdapter.h" - namespace storm { namespace storage { template @@ -243,9 +240,6 @@ namespace storm { template class BitVectorHashMap; template class BitVectorHashMap; - template class BitVectorHashMap>>; -#ifdef STORM_HAVE_CARL - template class BitVectorHashMap>>; -#endif + template class BitVectorHashMap; } } diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 654fb269e..522173d81 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -204,6 +204,7 @@ namespace storm { return stream.str(); } + // TODO rewrite to only use bitvector and id template std::string DFT::getStateString(DFTStatePointer const& state) const{ std::stringstream stream; diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 0cedfbfa7..2ee1a2edf 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -244,10 +244,18 @@ namespace storm { return state->hasFailed(mTopLevelIndex); } + bool hasFailed(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo) const { + return storm::storage::DFTState::hasFailed(state, stateGenerationInfo.getStateIndex(mTopLevelIndex)); + } + bool isFailsafe(DFTStatePointer const& state) const { return state->isFailsafe(mTopLevelIndex); } + bool isFailsafe(storm::storage::BitVector const& state, DFTStateGenerationInfo const& stateGenerationInfo) const { + return storm::storage::DFTState::isFailsafe(state, stateGenerationInfo.getStateIndex(mTopLevelIndex)); + } + std::string getElementsString() const; std::string getInfoString() const; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index c3f7c9f32..0bad03f78 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -63,11 +63,21 @@ namespace storm { bool DFTState::hasFailed(size_t id) const { return mStatus[mStateGenerationInfo.getStateIndex(id)]; } + + template + bool DFTState::hasFailed(storm::storage::BitVector const& state, size_t indexId) { + return state[indexId]; + } template bool DFTState::isFailsafe(size_t id) const { return mStatus[mStateGenerationInfo.getStateIndex(id)+1]; } + + template + bool DFTState::isFailsafe(storm::storage::BitVector const& state, size_t indexId) { + return state[indexId+1]; + } template bool DFTState::dontCare(size_t id) const { diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index fcbcdc62d..821aa2fcb 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -51,10 +51,14 @@ namespace storm { bool hasFailed(size_t id) const; - bool isFailsafe(size_t id) const ; + static bool hasFailed(storm::storage::BitVector const& state, size_t indexId); + bool isFailsafe(size_t id) const; + + static bool isFailsafe(storm::storage::BitVector const& state, size_t indexId); + bool dontCare(size_t id) const; - + bool dependencyTriggered(size_t id) const; bool dependencySuccessful(size_t id) const;