diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 4dd2e8402..4edd26b4b 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -59,8 +59,10 @@ namespace storm { //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); //size_t currentFailable = 0; state->getFailableElements().init(exploreDependencies); - // Check for absorbing state - if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->getFailableElements().isEnd()) { + // Check for absorbing state: + // - either no relevant event remains (i.e., all relevant events have failed already), or + // - no BE can fail + if (!state->getFailableElements().hasRemainingRelevantEvent() || state->getFailableElements().isEnd()) { Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); @@ -80,7 +82,6 @@ namespace storm { // We discard further exploration as we already chose one dependent event break; } - STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed."); isFirst = false; // Construct new state as copy from original one @@ -120,6 +121,8 @@ namespace storm { newState->updateFailableInRestrictions(next->id()); } + newState->updateRemainingRelevantEvents(); + bool transient = false; if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) { auto beExp = std::static_pointer_cast const>(nextBE); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 39b57773f..28b7d29d0 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -874,6 +874,18 @@ namespace storm { } } + template + std::set DFT::getRelevantEvents() const { + std::set relevantEvents; + for (auto const& elem : mElements) { + if (elem->isRelevant()) { + relevantEvents.insert(elem->id()); + } + } + return relevantEvents; + } + + template std::string DFT::getRelevantEventsString() const { std::stringstream stream; diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 9c6b31020..5c885ef59 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -318,6 +318,12 @@ namespace storm { */ size_t getIndex(std::string const& name) const; + /*! + * Get all relevant events. + * @return List of all relevant events. + */ + std::set getRelevantEvents() const; + /*! * Set the relevance flag for all elements according to the given relevant events. * @param relevantEvents All elements which should be to relevant. All elements not occuring are set to irrelevant. diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index a3c57f2e3..be66bc2a0 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(), dft.getRelevantEvents()), 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(), dft.getRelevantEvents()), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // Intentionally left empty } @@ -86,6 +86,11 @@ namespace storm { STORM_LOG_TRACE("New dependency failure: " << *dependency); } } + + // Initialize remaining relevant events + failableElements.remainingRelevantEvents = mDft.getRelevantEvents(); + this->updateRemainingRelevantEvents(); + mPseudoState = false; } @@ -311,6 +316,18 @@ namespace storm { } } + template + void DFTState::updateRemainingRelevantEvents() { + for (auto it = failableElements.remainingRelevantEvents.begin(); it != failableElements.remainingRelevantEvents.end(); ) { + if (isOperational(*it)) { + ++it; + } else { + // Element is not relevant anymore + it = failableElements.remainingRelevantEvents.erase(it); + } + } + } + template ValueType DFTState::getBERate(size_t id) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 3718e7627..fd911b355 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -25,7 +25,7 @@ namespace storm { struct FailableElements { - FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) { + FailableElements(size_t nrElements, std::set relevantEvents) : currentlyFailableBE(nrElements), remainingRelevantEvents(relevantEvents), it(currentlyFailableBE.begin()) { // Intentionally left empty } @@ -103,10 +103,19 @@ namespace storm { return !currentlyFailableBE.empty(); } + /*! + * Check whether at least one relevant event has not failed yet. + * @return True iff one relevant event is still operational. + */ + bool hasRemainingRelevantEvent() const { + return !remainingRelevantEvents.empty(); + } + mutable bool dependency; storm::storage::BitVector currentlyFailableBE; std::vector mFailableDependencies; + std::set remainingRelevantEvents; mutable storm::storage::BitVector::const_iterator it; mutable std::vector::const_iterator itDep; @@ -303,6 +312,11 @@ namespace storm { */ void updateDontCareDependencies(size_t id); + /*! + * Update remaining relevant events. + */ + void updateRemainingRelevantEvents(); + /** * Sets the next BE as failed * @param index Index in currentlyFailableBE of BE to fail diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index 46cab4f61..a934ea1e2 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -32,8 +32,8 @@ namespace { storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries, relevantEvents, false); builder2.buildModel(0, 0.0); model = builder2.getModel(); - EXPECT_EQ(448ul, model->getNumberOfStates()); - EXPECT_EQ(1260ul, model->getNumberOfTransitions()); + EXPECT_EQ(512ul, model->getNumberOfStates()); + EXPECT_EQ(2305ul, model->getNumberOfTransitions()); // Set relevant events (H) relevantEvents.clear();