From 2ec921a6835c0a67626eb12b8ad65a73f53391bb Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 7 Aug 2019 18:08:27 +0200 Subject: [PATCH] Added support for constantly failed BEs in the model generation --- .../builder/ExplicitDFTModelBuilder.cpp | 20 +++ .../generator/DftNextStateGenerator.cpp | 135 +++++++++++++----- .../generator/DftNextStateGenerator.h | 20 +++ 3 files changed, 136 insertions(+), 39 deletions(-) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 0f3196516..5275ed7e7 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -167,6 +167,26 @@ namespace storm { STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); + + // DFT may be instantly failed due to a constant failure + // in this case a model only consisting of the uniqueFailedState suffices + if (initialStateIndex == 0 && this->uniqueFailedState) { + modelComponents.markovianStates.resize(1); + modelComponents.deterministicModel = generator.isDeterministicModel(); + + STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); + STORM_LOG_DEBUG("Model has 1 state"); + STORM_LOG_DEBUG( + "Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic")); + + // Build transition matrix + modelComponents.transitionMatrix = matrixBuilder.builder.build(1, 1); + STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix); + + buildLabeling(); + return; + } + // Initialize heuristic values for inital state STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); ExplorationHeuristicPointer heuristic; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index bfbc870ba..d8fcb1072 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -22,11 +22,53 @@ namespace storm { template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); + size_t constFailedBeCounter = 0; + std::shared_ptr const> constFailedBE = nullptr; + for (auto &be : mDft.getBasicElements()) { + if (be->type() == storm::storage::DFTElementType::BE_CONST) { + auto constBe = std::static_pointer_cast const>(be); + if (constBe->failed()) { + constFailedBeCounter++; + STORM_LOG_THROW(constFailedBeCounter < 2, storm::exceptions::NotSupportedException, + "DFTs with more than one constantly failed BE are not supported"); + constFailedBE = constBe; + } + } + } + StateType id; + if (constFailedBeCounter == 0) { + // Register initial state + id = stateToIdCallback(initialState); + } else { + initialState->letNextBEFail(constFailedBE->id(), false); + // Propagate the constant failure to reach the real initial state + storm::storage::DFTStateSpaceGenerationQueues queues; + propagateFailure(initialState, constFailedBE, queues); + + if (initialState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) { + propagateFailsafe(initialState, constFailedBE, queues); + + // Update failable dependencies + initialState->updateFailableDependencies(constFailedBE->id()); + initialState->updateDontCareDependencies(constFailedBE->id()); + initialState->updateFailableInRestrictions(constFailedBE->id()); + + // Unique failed state + id = 0; + } else { + propagateFailsafe(initialState, constFailedBE, queues); - // Register initial state - StateType id = stateToIdCallback(initialState); + // Update failable dependencies + initialState->updateFailableDependencies(constFailedBE->id()); + initialState->updateDontCareDependencies(constFailedBE->id()); + initialState->updateFailableInRestrictions(constFailedBE->id()); + + id = stateToIdCallback(initialState); + } + } initialState->setId(id); + return {id}; } @@ -90,31 +132,7 @@ namespace storm { // Propagate storm::storage::DFTStateSpaceGenerationQueues queues; - // Propagate failure - for (DFTGatePointer parent : nextBE->parents()) { - if (newState->isOperational(parent->id())) { - queues.propagateFailure(parent); - } - } - // Propagate failures - while (!queues.failurePropagationDone()) { - DFTGatePointer next = queues.nextFailurePropagation(); - next->checkFails(*newState, queues); - newState->updateFailableDependencies(next->id()); - newState->updateFailableInRestrictions(next->id()); - } - - // Check restrictions - for (DFTRestrictionPointer restr : nextBE->restrictions()) { - queues.checkRestrictionLater(restr); - } - // Check restrictions - while(!queues.restrictionChecksDone()) { - DFTRestrictionPointer next = queues.nextRestrictionCheck(); - next->checkFails(*newState, queues); - newState->updateFailableDependencies(next->id()); - newState->updateFailableInRestrictions(next->id()); - } + propagateFailure(newState, nextBE, queues); newState->updateRemainingRelevantEvents(); @@ -137,18 +155,7 @@ namespace storm { // Use unique failed state newStateId = 0; } else { - // Propagate failsafe - while (!queues.failsafePropagationDone()) { - DFTGatePointer next = queues.nextFailsafePropagation(); - next->checkFailsafe(*newState, queues); - } - - // Propagate dont cares - // Relevance is considered for each element independently - while (!queues.dontCarePropagationDone()) { - DFTElementPointer next = queues.nextDontCarePropagation(); - next->checkDontCareAnymore(*newState, queues); - } + propagateFailsafe(newState, nextBE, queues); // Update failable dependencies newState->updateFailableDependencies(nextBE->id()); @@ -222,6 +229,56 @@ namespace storm { return result; } + template + void DftNextStateGenerator::propagateFailure(DFTStatePointer newState, + std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues) { + // Propagate failure + for (DFTGatePointer parent : nextBE->parents()) { + if (newState->isOperational(parent->id())) { + queues.propagateFailure(parent); + } + } + // Propagate failures + while (!queues.failurePropagationDone()) { + DFTGatePointer next = queues.nextFailurePropagation(); + next->checkFails(*newState, queues); + newState->updateFailableDependencies(next->id()); + newState->updateFailableInRestrictions(next->id()); + } + + // Check restrictions + for (DFTRestrictionPointer restr : nextBE->restrictions()) { + queues.checkRestrictionLater(restr); + } + // Check restrictions + while (!queues.restrictionChecksDone()) { + DFTRestrictionPointer next = queues.nextRestrictionCheck(); + next->checkFails(*newState, queues); + newState->updateFailableDependencies(next->id()); + newState->updateFailableInRestrictions(next->id()); + } + + } + + template + void DftNextStateGenerator::propagateFailsafe(DFTStatePointer newState, + std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues) { + // Propagate failsafe + while (!queues.failsafePropagationDone()) { + DFTGatePointer next = queues.nextFailsafePropagation(); + next->checkFailsafe(*newState, queues); + } + + // Propagate dont cares + // Relevance is considered for each element independently + while (!queues.dontCarePropagationDone()) { + DFTElementPointer next = queues.nextDontCarePropagation(); + next->checkDontCareAnymore(*newState, queues); + } + } + template StateBehavior DftNextStateGenerator::createMergeFailedState(StateToIdCallback const& stateToIdCallback) { this->uniqueFailedState = true; diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 9fab2ee1f..4a1e45308 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -42,6 +42,26 @@ namespace storm { */ StateBehavior createMergeFailedState(StateToIdCallback const& stateToIdCallback); + /** + * Propagate the failures in a given state if the given BE fails + * + * @param newState starting state of the propagation + * @param nextBE BE whose failure is propagated + */ + void + propagateFailure(DFTStatePointer newState, std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues); + + /** + * Propagate the failsafe state in a given state if the given BE fails + * + * @param newState starting state of the propagation + * @param nextBE BE whose failure is propagated + */ + void + propagateFailsafe(DFTStatePointer newState, std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues); + private: StateBehavior exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies);