From 8755e75a60f12bc9e9cf91fd9ccbfe2367bc623c Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 19 Feb 2016 18:13:05 +0100 Subject: [PATCH 1/4] towards a new element (and actually added a folder) Former-commit-id: 0bca77dfa7b9800ef60225ca2fcc3e01d5e1e157 --- src/CMakeLists.txt | 2 + src/storage/dft/DFTElementType.h | 7 ++- src/storage/dft/DFTElements.h | 54 ----------------------- src/storage/dft/elements/DFTRestriction.h | 13 ++++++ 4 files changed, 18 insertions(+), 58 deletions(-) create mode 100644 src/storage/dft/elements/DFTRestriction.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3aa121a0a..60fbadab9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -38,6 +38,7 @@ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SO file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp) +file(GLOB STORM_STORAGE_DFT_ELEMENTS_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) @@ -94,6 +95,7 @@ source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) source_group(storage\\dft FILES ${STORM_STORAGE_DFT_FILES}) +source_group(storage\\dft\\elements FILES ${STORM_STORAGE_DFT_ELEMENTS_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) # Add custom additional include or link directories diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h index a32745cdf..d4bf3bfc2 100644 --- a/src/storage/dft/DFTElementType.h +++ b/src/storage/dft/DFTElementType.h @@ -4,20 +4,20 @@ namespace storm { namespace storage { - enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQAND = 11}; + enum class DFTElementType : int {AND = 0, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQ = 11, MUTEX=12}; inline bool isGateType(DFTElementType const& tp) { switch(tp) { case DFTElementType::AND: - case DFTElementType::COUNTING: case DFTElementType::OR: case DFTElementType::VOT: case DFTElementType::PAND: case DFTElementType::SPARE: case DFTElementType::POR: - case DFTElementType::SEQAND: return true; + case DFTElementType::SEQ: + case DFTElementType::MUTEX: case DFTElementType::BE: case DFTElementType::CONSTF: case DFTElementType::CONSTS: @@ -40,7 +40,6 @@ namespace storm { case DFTElementType::POR: case DFTElementType::SPARE: case DFTElementType::PAND: - case DFTElementType::SEQAND: return false; default: assert(false); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 11fc31948..c51e180c7 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -726,60 +726,6 @@ namespace storm { - template - class DFTSeqAnd : public DFTGate { - - public: - DFTSeqAnd(size_t id, std::string const& name, std::vector>> const& children = {}) : - DFTGate(id, name, children) - {} - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(!state.hasFailed(this->mId)) { - bool childOperationalBefore = false; - for(auto const& child : this->mChildren) - { - if(!state.hasFailed(child->id())) { - childOperationalBefore = true; - } - else { - if(childOperationalBefore) { - state.markAsInvalid(); - return; - } - } - } - if(!childOperationalBefore) { - fail(state, queues); - } - - } - } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ - assert(hasFailsafeChild(state)); - if(state.isOperational(this->mId)) { - failsafe(state, queues); - //return true; - } - //return false; - } - - virtual DFTElementType type() const override { - return DFTElementType::SEQAND; - } - - std::string typestring() const override { - return "SEQAND"; - } - }; - - template - inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) { - return os << gate.toString(); - } - - template class DFTPand : public DFTGate { diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h new file mode 100644 index 000000000..8bd586deb --- /dev/null +++ b/src/storage/dft/elements/DFTRestriction.h @@ -0,0 +1,13 @@ +#pragma once + +#include "../DFTElements.h" + +namespace storm { + namespace storage { + template + class DFTRestriction : public DFTElement { + + }; + + } +} \ No newline at end of file From 7bcbbe75faf5ea592b3253cad345517b1b3b8bc8 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sun, 21 Feb 2016 15:53:14 +0100 Subject: [PATCH 2/4] Set dont care for children if parent gate fails Former-commit-id: c70852b7e85804cea30d6a27090baaa8457e4cb8 --- src/storage/dft/DFTElements.cpp | 26 ++++++++++++++++---------- src/storage/dft/DFTElements.h | 2 ++ 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index 26f5f9cbe..e06b3fe7d 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -7,18 +7,24 @@ namespace storm { template bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(!state.dontCare(mId) && !hasOutgoingDependencies()) - { - for(DFTGatePointer const& parent : mParents) { - if(state.isOperational(parent->id())) { - return false; - } + if (state.dontCare(mId)) { + return false; + } + // Check that no outgoing dependencies can be triggered anymore + for (DFTDependencyPointer dependency : mOutgoingDependencies) { + if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) { + return false; } - state.setDontCare(mId); - return true; - } - return false; + // Check that no parent can fail anymore + for(DFTGatePointer const& parent : mParents) { + if(state.isOperational(parent->id())) { + return false; + } + } + + state.setDontCare(mId); + return true; } template diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 11fc31948..d5620717f 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -350,6 +350,7 @@ namespace storm { } } state.setFailed(this->mId); + this->childrenDontCare(state, queues); } void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { @@ -359,6 +360,7 @@ namespace storm { } } state.setFailsafe(this->mId); + this->childrenDontCare(state, queues); } void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { From 74b512a76ef62c727a453a50590c12eded00c234 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sun, 21 Feb 2016 16:05:03 +0100 Subject: [PATCH 3/4] Consider dependencies in DFS for state generation info Former-commit-id: c61210cbd548a265778bc636caedab123107d355 --- src/storage/dft/DFT.cpp | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 519036fff..92e780872 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -80,23 +80,17 @@ namespace storm { std::queue visitQueue; std::set visited; visitQueue.push(subTreeRoots[0]); - bool consideredDependencies = false; - while (true) { - if (consideredDependencies) { - break; - } - - stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); - - // 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; + stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); + + // 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()); } + stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex); + assert(stateIndex = mStateVectorSize); STORM_LOG_TRACE(generationInfo); From 371ba87f1c08223f0708e8ceee015d1b5d843466 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sun, 21 Feb 2016 19:35:20 +0100 Subject: [PATCH 4/4] Fixed activation of spares Former-commit-id: f62ccdc79a984cad432d00d8c06a855e52debdb1 --- examples/dft/spare8.dft | 7 +++++ src/builder/ExplicitDFTModelBuilder.cpp | 15 +++++----- src/storage/dft/DFT.cpp | 14 +++++---- src/storage/dft/DFTElements.h | 32 ++++++++++++++++---- src/storage/dft/DFTState.cpp | 40 ++++++++++--------------- src/storage/dft/DFTState.h | 9 +++--- 6 files changed, 69 insertions(+), 48 deletions(-) create mode 100644 examples/dft/spare8.dft diff --git a/examples/dft/spare8.dft b/examples/dft/spare8.dft new file mode 100644 index 000000000..c67eaf022 --- /dev/null +++ b/examples/dft/spare8.dft @@ -0,0 +1,7 @@ +toplevel "A"; +"A" wsp "I" "B"; +"B" wsp "J" "K"; +"I" lambda=0.5 dorm=0.3; +"J" lambda=0.5 dorm=0.3; +"K" lambda=0.5 dorm=0.3; + diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index cbb9b69d0..4900845a5 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -256,7 +256,7 @@ namespace storm { if (mStates.contains(unsuccessfulState->status())) { // Unsuccessful state already exists unsuccessfulStateId = mStates.getValue(unsuccessfulState->status()); - STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists"); + STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " with id " << unsuccessfulStateId << " already exists"); } else { // New unsuccessful state unsuccessfulState->setId(newIndex++); @@ -277,16 +277,15 @@ namespace storm { ++rowOffset; } else { - // Set failure rate according to usage - bool isUsed = true; + // Set failure rate according to activation + bool isActive = true; if (mDft.hasRepresentant(nextBE->id())) { - DFTElementCPointer representant = mDft.getRepresentant(nextBE->id()); - // Used must be checked for the state we are coming from as this state is responsible for the + // Active must be checked for the state we are coming from as this state is responsible for the // rate and not the new state we are going to - isUsed = state->isUsed(representant->id()); + isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id()); } - STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); - ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); + STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isActive ? "active" : "not active")); + ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); auto resultFind = outgoingTransitions.find(newStateId); if (resultFind != outgoingTransitions.end()) { // Add to existing transition diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 92e780872..3fbcd5ee1 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -191,10 +191,11 @@ namespace storm { } else { stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id())); if(elem->isSpareGate()) { - if(state->isActiveSpare(elem->id())) { - stream << " actively"; + size_t useId = state->uses(elem->id()); + if(state->isActive(useId)) { + stream << " actively "; } - stream << " using " << state->uses(elem->id()); + stream << " using " << useId; } } stream << std::endl; @@ -214,10 +215,11 @@ namespace storm { stream << storm::storage::toChar(state->getElementState(elem->id())); if(elem->isSpareGate()) { stream << "["; - if(state->isActiveSpare(elem->id())) { - stream << "actively "; + size_t useId = state->uses(elem->id()); + if(state->isActive(useId)) { + stream << " actively "; } - stream << "using " << state->uses(elem->id()) << "]"; + stream << "using " << useId << "]"; } } } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index eaee1d54a..22c819f84 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -259,11 +259,13 @@ namespace storm { virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; virtual void extendSpareModule(std::set& elementsInSpareModule) const override { - DFTElement::extendSpareModule(elementsInSpareModule); - for(auto const& child : mChildren) { - if(elementsInSpareModule.count(child->id()) == 0) { - elementsInSpareModule.insert(child->id()); - child->extendSpareModule(elementsInSpareModule); + if (!this->isSpareGate()) { + DFTElement::extendSpareModule(elementsInSpareModule); + for( auto const& child : mChildren) { + if(elementsInSpareModule.count(child->id()) == 0) { + elementsInSpareModule.insert(child->id()); + child->extendSpareModule(elementsInSpareModule); + } } } } @@ -350,6 +352,9 @@ namespace storm { } } state.setFailed(this->mId); + if (this->isSpareGate()) { + this->finalizeSpare(state); + } this->childrenDontCare(state, queues); } @@ -360,6 +365,9 @@ namespace storm { } } state.setFailsafe(this->mId); + if (this->isSpareGate()) { + this->finalizeSpare(state); + } this->childrenDontCare(state, queues); } @@ -367,6 +375,20 @@ namespace storm { queues.propagateDontCare(mChildren); } + /** + * Finish failed/failsafe spare gate by activating the children and setting the useIndex to zero. + * This prevents multiple fail states with different usages or activations. + * @param state The current state. + */ + void finalizeSpare(DFTState& state) const { + state.setUses(this->mId, 0); + for (auto child : this->children()) { + if (!state.isActive(child->id())) { + state.activate(child->id()); + } + } + } + bool hasFailsafeChild(DFTState& state) const { for(auto const& child : mChildren) { if(state.isFailsafe(child->id())) diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 0bad03f78..7f34e03ef 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -7,7 +7,6 @@ namespace storm { template DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { - mInactiveSpares = dft.getSpareIndices(); // Initialize uses for(size_t id : mDft.getSpareIndices()) { @@ -18,12 +17,7 @@ namespace storm { } // Initialize activation - this->activate(mDft.getTopLevelIndex()); - for(auto const& id : mDft.module(mDft.getTopLevelIndex())) { - if(mDft.getElement(id)->isSpareGate()) { - propagateActivation(uses(id)); - } - } + propagateActivation(mDft.getTopLevelIndex()); std::vector alwaysActiveBEs = dft.nonColdBEs(); mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); @@ -182,29 +176,25 @@ namespace storm { template void DFTState::activate(size_t repr) { - for(size_t elem : mDft.module(repr)) { - if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { - mIsCurrentlyFailableBE.push_back(elem); - } - else if(mDft.getElement(elem)->isSpareGate()) { - assert(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem) != mInactiveSpares.end()); - mInactiveSpares.erase(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem)); - } - } + size_t activationIndex = mStateGenerationInfo.getSpareActivationIndex(repr); + assert(!mStatus[activationIndex]); + mStatus.set(activationIndex); + propagateActivation(repr); } template - bool DFTState::isActiveSpare(size_t id) const { - assert(mDft.getElement(id)->isSpareGate()); - return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end()); + bool DFTState::isActive(size_t id) const { + assert(mDft.isRepresentative(id)); + return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)]; } template void DFTState::propagateActivation(size_t representativeId) { - activate(representativeId); - for(size_t id : mDft.module(representativeId)) { - if(mDft.getElement(id)->isSpareGate()) { - propagateActivation(uses(id)); + for(size_t elem : mDft.module(representativeId)) { + if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) { + mIsCurrentlyFailableBE.push_back(elem); + } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { + activate(uses(elem)); } } } @@ -243,8 +233,8 @@ namespace storm { size_t childId = (*it)->id(); if(!hasFailed(childId) && !isUsed(childId)) { setUses(spareId, childId); - if(isActiveSpare(spareId)) { - propagateActivation(childId); + if(isActive(currentlyUses)) { + activate(childId); } return true; } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 821aa2fcb..7a26e10ab 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -26,7 +26,6 @@ namespace storm { // Status is bitvector where each element has two bits with the meaning according to DFTElementState storm::storage::BitVector mStatus; size_t mId; - std::vector mInactiveSpares; std::vector mIsCurrentlyFailableBE; std::vector mFailableDependencies; std::vector mUsedRepresentants; @@ -79,9 +78,7 @@ namespace storm { void activate(size_t repr); - bool isActiveSpare(size_t id) const; - - void propagateActivation(size_t representativeId); + bool isActive(size_t id) const; void markAsInvalid() { mValid = false; @@ -200,6 +197,10 @@ namespace storm { friend bool operator==(DFTState const& a, DFTState const& b) { return a.mStatus == b.mStatus; } + + private: + void propagateActivation(size_t representativeId); + }; }