diff --git a/examples/dft/pdep_symmetry.dft b/examples/dft/pdep_symmetry.dft index 43224d790..5c9254aa5 100644 --- a/examples/dft/pdep_symmetry.dft +++ b/examples/dft/pdep_symmetry.dft @@ -2,8 +2,8 @@ toplevel "A"; "A" and "B" "B'"; "B" and "C" "D" "PDEP"; "B'" and "C'" "D'" "PDEP'"; -"PDEP" pdep=0.6 "B" "C"; -"PDEP'" pdep=0.6 "B'" "C'"; +"PDEP" pdep=0.6 "C" "D"; +"PDEP'" pdep=0.6 "C'" "D'"; "C" lambda=0.5 dorm=0; "D" lambda=0.5 dorm=0; "C'" lambda=0.5 dorm=0; diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 09fde00ef..103e87af3 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -227,6 +227,7 @@ namespace storm { // Update failable dependencies if (!dftFailed) { newState->updateFailableDependencies(nextBE->id()); + newState->updateDontCareDependencies(nextBE->id()); } uint_fast64_t newStateId; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 24291b446..1468a36ff 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -142,14 +142,21 @@ namespace storm { template void DFTState::setDependencySuccessful(size_t id) { - // No distinction between successful dependency and no dependency at all - // => we do not set bit - //mStatus.set(mStateGenerationInfo.mIdToStateIndex(id)); + // Only distinguish between passive and dont care dependencies + //mStatus.set(mStateGenerationInfo.getStateIndex(id)); + setDependencyDontCare(id); } template void DFTState::setDependencyUnsuccessful(size_t id) { - mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); + // Only distinguish between passive and dont care dependencies + //mStatus.set(mStateGenerationInfo.getStateIndex(id)+1); + setDependencyDontCare(id); + } + + template + void DFTState::setDependencyDontCare(size_t id) { + mStatus.setFromInt(mStateGenerationInfo.getStateIndex(id), 2, static_cast(DFTDependencyState::DontCare)); } template @@ -176,6 +183,17 @@ namespace storm { } return nrFailableDependencies() > 0; } + + template + void DFTState::updateDontCareDependencies(size_t id) { + assert(mDft.isBasicElement(id)); + assert(hasFailed(id)); + + for (auto dependency : mDft.getBasicElement(id)->ingoingDependencies()) { + assert(dependency->dependentEvent()->id() == id); + setDependencyDontCare(dependency->id()); + } + } template std::pair const>, bool> DFTState::letNextBEFail(size_t index) diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index faf183411..1311d74ae 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -79,6 +79,8 @@ namespace storm { void setDependencyUnsuccessful(size_t id); + void setDependencyDontCare(size_t id); + void beNoLongerFailable(size_t id); void activate(size_t repr); @@ -162,6 +164,12 @@ namespace storm { * @return true if failable dependent events exist */ bool updateFailableDependencies(size_t id); + + /** + * Sets all dependencies dont care whose dependent event is the newly failed BE. + * @param id Id of the newly failed element + */ + void updateDontCareDependencies(size_t id); /** * Sets the next BE as failed