From 87180e1000dec45452b5b35b89bc54909cfcecf6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 24 Mar 2019 18:05:21 +0100 Subject: [PATCH] Correct initialization of priority queue --- .../generator/DftNextStateGenerator.cpp | 32 ++++++++++++------- .../generator/DftNextStateGenerator.h | 4 ++- src/storm-dft/storage/dft/DFTState.cpp | 10 +++--- src/storm-dft/storage/dft/DFTState.h | 3 +- 4 files changed, 32 insertions(+), 17 deletions(-) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 2a3502c5e..69751ea62 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -46,16 +46,19 @@ namespace storm { template StateBehavior DftNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state)); + // Initialization + bool hasDependencies = state->getFailableElements().hasDependencies(); + return exploreState(stateToIdCallback, hasDependencies); + } + template + StateBehavior DftNextStateGenerator::exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies) { // Prepare the result, in case we return early. StateBehavior result; - // Initialization - bool hasDependencies = state->getFailableElements().hasDependencies(); //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); //size_t currentFailable = 0; - state->getFailableElements().init(hasDependencies); - + state->getFailableElements().init(exploreDependencies); // Check for absorbing state if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->getFailableElements().isEnd()) { Choice choice(0, true); @@ -68,12 +71,12 @@ namespace storm { return result; } - Choice choice(0, !hasDependencies); + Choice choice(0, !exploreDependencies); // Let BE fail bool isFirst = true; while (!state->getFailableElements().isEnd()) { - if (storm::settings::getModule().isTakeFirstDependency() && hasDependencies && !isFirst) { + if (storm::settings::getModule().isTakeFirstDependency() && exploreDependencies && !isFirst) { // We discard further exploration as we already chose one dependent event break; } @@ -82,10 +85,10 @@ namespace storm { // Construct new state as copy from original one DFTStatePointer newState = state->copy(); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get()); + std::pair const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get(), exploreDependencies); std::shared_ptr const>& nextBE = nextBEPair.first; STORM_LOG_ASSERT(nextBE, "NextBE is null."); - STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match."); + STORM_LOG_ASSERT(nextBEPair.second == exploreDependencies, "Failure due to dependencies does not match."); STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state)); // Propagate @@ -149,7 +152,7 @@ namespace storm { } // Set transitions - if (hasDependencies) { + if (exploreDependencies) { // Failure is due to dependency -> add non-deterministic choice ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability(); choice.addProbability(newStateId, probability); @@ -184,8 +187,15 @@ namespace storm { state->getFailableElements().next(); } // end while failing BE - - if (!hasDependencies) { + + if (exploreDependencies) { + if (result.empty()) { + // Dependencies might have been prevented from sequence enforcer + // -> explore BEs now + return exploreState(stateToIdCallback, false); + } + } else { + STORM_LOG_ASSERT(choice.size() > 0, "No transitions were generated"); // Add all rates as one choice result.addChoice(std::move(choice)); } diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 2f614afe6..08aa3739e 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -43,7 +43,9 @@ namespace storm { StateBehavior createMergeFailedState(StateToIdCallback const& stateToIdCallback); private: - + + StateBehavior exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies); + // The dft used for the generation of next states. storm::storage::DFT const& mDft; diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 2bbc2dfed..18b0559a0 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -195,7 +195,8 @@ namespace storm { if (!hasFailed(id)) { return false; } - + + bool addedFailableDependency = false; for (auto dependency : mDft.getElement(id)->outgoingDependencies()) { STORM_LOG_ASSERT(dependency->triggerEvent()->id() == id, "Ids do not match."); assert(dependency->dependentEvents().size() == 1); @@ -203,9 +204,10 @@ namespace storm { STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe."); failableElements.addDependency(dependency->id()); STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); + addedFailableDependency = true; } } - return failableElements.hasDependencies(); + return addedFailableDependency; } template @@ -235,9 +237,9 @@ namespace storm { } template - std::pair const>, bool> DFTState::letNextBEFail(size_t id) { + std::pair const>, bool> DFTState::letNextBEFail(size_t id, bool dueToDependency) { STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - if (failableElements.hasDependencies()) { + if (dueToDependency) { // Consider failure due to dependency std::shared_ptr const> dependency = mDft.getDependency(id); STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 427115de4..e569e8d49 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -299,9 +299,10 @@ namespace storm { /** * Sets the next BE as failed * @param index Index in currentlyFailableBE of BE to fail + * @param dueToDependency Whether the failure is due to a dependency. * @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies */ - std::pair const>, bool> letNextBEFail(size_t index = 0); + std::pair const>, bool> letNextBEFail(size_t index, bool dueToDependency); /** * Sets the dependency as unsuccesful meaning no BE will fail.