From 84467267e09b380ae5cceba5c157f308eefe8d03 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 7 Jun 2019 15:56:08 +0200 Subject: [PATCH] Second try to improve performance for relevant events --- .../builder/ExplicitDFTModelBuilder.cpp | 8 ++++---- .../generator/DftNextStateGenerator.cpp | 14 +------------ src/storm-dft/storage/dft/DFT.cpp | 11 +++++++--- src/storm-dft/storage/dft/DFT.h | 4 ++-- src/storm-dft/storage/dft/DFTState.cpp | 20 +++++++++++++++++-- src/storm-dft/storage/dft/DFTState.h | 9 ++++++++- 6 files changed, 41 insertions(+), 25 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index e71f8e4b9..d673e57c5 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -42,8 +42,6 @@ namespace storm { { // Set relevant events this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents); - // Mark top level element as relevant - this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true); STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString()); if (this->relevantEvents.empty()) { // Only interested in top level event -> introduce unique failed state @@ -477,9 +475,10 @@ namespace storm { modelComponents.stateLabeling.addLabel("init"); STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped."); modelComponents.stateLabeling.addLabelToState("init", initialStateIndex); - // Label all states corresponding to their status (failed, failed/dont care BE) + // System failure modelComponents.stateLabeling.addLabel("failed"); + // Label all states corresponding to their status (failed, don't care BE) // Collect labels for all necessary elements for (size_t id = 0; id < dft.nrElements(); ++id) { std::shared_ptr const> element = dft.getElement(id); @@ -491,6 +490,7 @@ namespace storm { // Set labels to states if (this->uniqueFailedState) { + // Unique failed state has label 0 modelComponents.stateLabeling.addLabelToState("failed", 0); } for (auto const& stateIdPair : stateStorage.stateToId) { @@ -499,7 +499,7 @@ namespace storm { if (dft.hasFailed(state, *stateGenerationInfo)) { modelComponents.stateLabeling.addLabelToState("failed", stateId); } - // Set fail/dont care status for each necessary element + // Set failed/don't care status for each necessary element for (size_t id = 0; id < dft.nrElements(); ++id) { std::shared_ptr const> element = dft.getElement(id); if (element->isRelevant()){ diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index c8825fff1..fcec7bb70 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -61,22 +61,10 @@ namespace storm { //size_t currentFailable = 0; state->getFailableElements().init(exploreDependencies); - // Check whether operational relevant event remains - bool remainingRelevantEvent = true; - if (mDft.hasFailed(state)) { - remainingRelevantEvent = false; - // Toplevel has failed already -> check for possible other relevant events - for (auto const& event : mDft.getRelevantEvents()) { - if (state->isOperational(event)) { - remainingRelevantEvent = true; - break; - } - } - } // Check for absorbing state: // - either no relevant event remains (i.e., all relevant events have failed already), or // - no BE can fail - if (!remainingRelevantEvent || state->getFailableElements().isEnd()) { + if (!state->hasOperationalRelevantEvent() || state->getFailableElements().isEnd()) { Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 5132813d8..9a5df355a 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -873,11 +873,16 @@ namespace storm { template void DFT::setRelevantEvents(std::set const& relevantEvents, bool allowDCForRelevantEvents) const { mRelevantEvents.clear(); + // Top level element is first element + mRelevantEvents.push_back(this->getTopLevelIndex()); for (auto const& elem : mElements) { - if (relevantEvents.find(elem->id()) != relevantEvents.end()) { + if (relevantEvents.find(elem->id()) != relevantEvents.end() || elem->id() == this->getTopLevelIndex()) { elem->setRelevance(true); elem->setAllowDC(allowDCForRelevantEvents); - mRelevantEvents.insert(elem->id()); + if (elem->id() != this->getTopLevelIndex()) { + // Top level element was already added + mRelevantEvents.push_back(elem->id()); + } } else { elem->setRelevance(false); elem->setAllowDC(true); @@ -886,7 +891,7 @@ namespace storm { } template - std::set DFT::getRelevantEvents() const { + std::vector const& DFT::getRelevantEvents() const { return mRelevantEvents; } diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 831795cce..f3eaecc63 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -68,7 +68,7 @@ namespace storm { std::map mRepresentants; // id element -> id representative std::vector> mSymmetries; std::map mLayoutInfo; - mutable std::set mRelevantEvents; + mutable std::vector mRelevantEvents; public: DFT(DFTElementVector const& elements, DFTElementPointer const& tle); @@ -324,7 +324,7 @@ namespace storm { * Get all relevant events. * @return List of all relevant events. */ - std::set getRelevantEvents() const; + std::vector const& getRelevantEvents() const; /*! * Set the relevance flag for all elements according to the given relevant events. diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index d528035d3..cd174c553 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -7,7 +7,7 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements()), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateBitVectorSize()), mId(id), failableElements(dft.nrElements()), indexRelevant(0), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // TODO: use construct() // Initialize uses @@ -33,7 +33,7 @@ namespace storm { } template - DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { + DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), failableElements(dft.nrElements()), indexRelevant(0), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // Intentionally left empty } @@ -470,6 +470,22 @@ namespace storm { return false; } + template + bool DFTState::hasOperationalRelevantEvent() { + // Iterate over remaining relevant events + // All events with index < indexRelevant are already failed + while (indexRelevant < mDft.getRelevantEvents().size()) { + if (isOperational(mDft.getRelevantEvents()[indexRelevant])) { + // Relevant event is still operational + return true; + } else { + // Consider next relevant event + ++indexRelevant; + } + } + return false; + } + template bool DFTState::claimNew(size_t spareId, size_t currentlyUses, std::vector>> const& children) { auto it = children.begin(); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 3718e7627..f0429b99d 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -119,6 +119,7 @@ namespace storm { size_t mId; FailableElements failableElements; std::vector mUsedRepresentants; + size_t indexRelevant; bool mPseudoState; bool mValid = true; const DFT& mDft; @@ -330,12 +331,18 @@ namespace storm { */ bool isEventDisabledViaRestriction(size_t id) const; - /** + /*! * Checks whether operational post seq elements are present * @param id * @return */ bool hasOperationalPostSeqElements(size_t id) const; + + /*! + * Check whether at least one relevant event is still operational. + * @return True iff one operational relevant event exists. + */ + bool hasOperationalRelevantEvent(); std::string getCurrentlyFailableString() const { std::stringstream stream;