diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 0bd92b069..817295346 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -40,7 +40,7 @@ namespace storm { STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix); STORM_LOG_DEBUG("Exit rates: " << modelComponents.exitRates); STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates); - assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); + assert(!deterministic || modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount()); // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size()); @@ -100,24 +100,26 @@ namespace storm { // TODO Matthias: set Markovian states directly as bitvector? std::map outgoingTransitions; size_t rowOffset = 0; // Captures number of non-deterministic choices - ValueType exitRate; bool deterministic = true; - //TODO Matthias: Handle dependencies! while (!stateQueue.empty()) { // Initialization outgoingTransitions.clear(); - exitRate = storm::utility::zero(); + ValueType exitRate = storm::utility::zero(); // Consider next state DFTStatePointer state = stateQueue.front(); stateQueue.pop(); + bool hasDependencies = state->nrFailableDependencies() > 0; + deterministic &= !hasDependencies; + size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); size_t smallest = 0; + transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); + // Add self loop for target states if (mDft.hasFailed(state) || mDft.isFailsafe(state)) { - transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, state->getId(), storm::utility::one()); STORM_LOG_TRACE("Added self loop for " << state->getId()); exitRates.push_back(storm::utility::one()); @@ -130,18 +132,21 @@ namespace storm { } // Let BE fail - while (smallest < state->nrFailableBEs()) { + while (smallest < failableCount) { STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state)); // Construct new state as copy from original one DFTStatePointer newState = std::make_shared>(*state); std::pair>, bool> nextBEPair = newState->letNextBEFail(smallest++); std::shared_ptr> nextBE = nextBEPair.first; - if (nextBE == nullptr) { - break; - } + assert(nextBE); + assert(nextBEPair.second == hasDependencies); STORM_LOG_TRACE("with the failure of: " << nextBE->name() << " [" << nextBE->id() << "]"); + // Update failable dependencies + newState->updateFailableDependencies(nextBE->id()); + + // Propagate failures storm::storage::DFTStateSpaceGenerationQueues queues; for (DFTGatePointer parent : nextBE->parents()) { @@ -179,42 +184,53 @@ namespace storm { stateQueue.push(newState); } - // Set failure rate according to usage - bool isUsed = true; - if (mDft.hasRepresentant(nextBE->id())) { - DFTElementPointer representant = mDft.getRepresentant(nextBE->id()); - // Used 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()); - } - STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); - ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); - auto resultFind = outgoingTransitions.find(newState->getId()); - if (resultFind != outgoingTransitions.end()) { - // Add to existing transition - resultFind->second += rate; - STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second); + // Set transitions + if (hasDependencies) { + // Failure is due to dependency -> add non-deterministic choice + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), storm::utility::one()); } else { - // Insert new transition - outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); - STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate); + // Set failure rate according to usage + bool isUsed = true; + if (mDft.hasRepresentant(nextBE->id())) { + DFTElementPointer representant = mDft.getRepresentant(nextBE->id()); + // Used 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()); + } + STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used")); + ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); + auto resultFind = outgoingTransitions.find(newState->getId()); + if (resultFind != outgoingTransitions.end()) { + // Add to existing transition + resultFind->second += rate; + STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second); + } else { + // Insert new transition + outgoingTransitions.insert(std::make_pair(newState->getId(), rate)); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate); + } + exitRate += rate; } - exitRate += rate; } // end while failing BE - // Add all transitions - transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset); - for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) - { - ValueType probability = it->second / exitRate; // Transform rate to probability - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability); + if (hasDependencies) { + rowOffset--; // One increment to many + } else { + // Add all probability transitions + for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it) + { + ValueType probability = it->second / exitRate; // Transform rate to probability + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability); + } + + markovianStates.push_back(state->getId()); } exitRates.push_back(exitRate); assert(exitRates.size()-1 == state->getId()); - markovianStates.push_back(state->getId()); } // end while queue + assert(!deterministic || rowOffset == 0); return deterministic; } diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 112a9273b..1329cab38 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -11,13 +11,13 @@ namespace storm { size_t stateIndex = 0; mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1; - for(auto& elem : mElements) { + for (auto& elem : mElements) { mIdToFailureIndex.push_back(stateIndex); stateIndex += 2; if(elem->isBasicElement()) { ++mNrOfBEs; } - else if(elem->isSpareGate()) { + else if (elem->isSpareGate()) { ++mNrOfSpares; for(auto const& spareReprs : std::static_pointer_cast>(elem)->children()) { if(mActivationIndex.count(spareReprs->id()) == 0) { @@ -39,6 +39,8 @@ namespace storm { mUsageIndex.insert(std::make_pair(elem->id(), stateIndex)); stateIndex += mUsageInfoBits; + } else if (elem->isDependency()) { + mDependencies.push_back(elem->id()); } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 2cfbf6422..cff6db0cb 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -51,6 +51,7 @@ namespace storm { size_t mStateSize; std::map mActivationIndex; std::map> mSpareModules; + std::vector mDependencies; std::vector mTopModule; std::vector mIdToFailureIndex; std::map mUsageIndex; @@ -120,6 +121,10 @@ namespace storm { } } + std::vector const& getDependencies() const { + return mDependencies; + } + void propagateActivation(DFTState& state, size_t representativeId) const { state.activate(representativeId); for(size_t id : module(representativeId)) { diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index d760129e0..17bb4aee8 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -78,17 +78,41 @@ namespace storm { } } + template + bool DFTState::updateFailableDependencies(size_t id) { + assert(hasFailed(id)); + for (size_t i = 0; i < mDft.getDependencies().size(); ++i) { + std::shared_ptr> dependency = std::static_pointer_cast>(mDft.getElement(mDft.getDependencies()[i])); + if (dependency->triggerEvent()->id() == id) { + if (!hasFailed(dependency->dependentEvent()->id())) { + mFailableDependencies.push_back(dependency->id()); + STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); + } + } + } + return nrFailableDependencies() > 0; + } + template std::pair>, bool> DFTState::letNextBEFail(size_t index) { - assert(index < mIsCurrentlyFailableBE.size()); STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - // TODO set when implementing functional dependencies - bool dueToFdep = false; - std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), dueToFdep); - mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); - setFailed(res.first->id()); - return res; + if (nrFailableDependencies() > 0) { + // Consider failure due to dependency + assert(index < nrFailableDependencies()); + std::shared_ptr> dependency = std::static_pointer_cast>(mDft.getElement(mFailableDependencies[index])); + std::pair>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true); + mFailableDependencies.erase(mFailableDependencies.begin() + index); + setFailed(res.first->id()); + return res; + } else { + // Consider "normal" failure + assert(index < nrFailableBEs()); + std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); + mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); + setFailed(res.first->id()); + return res; + } } template diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index fed33eee3..a1bab2583 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -25,6 +25,7 @@ namespace storm { size_t mId; std::vector mInactiveSpares; std::vector mIsCurrentlyFailableBE; + std::vector mFailableDependencies; std::vector mUsedRepresentants; bool mValid = true; const DFT& mDft; @@ -110,6 +111,17 @@ namespace storm { return mIsCurrentlyFailableBE.size(); } + size_t nrFailableDependencies() const { + return mFailableDependencies.size(); + } + + /** + * Sets all failable BEs due to dependencies from newly failed element + * @param id Id of the newly failed element + * @return true if failable dependent events exist + */ + bool updateFailableDependencies(size_t id); + /** * Sets the next BE as failed * @param smallestIndex Index in currentlyFailableBE of BE to fail @@ -119,17 +131,31 @@ namespace storm { std::string getCurrentlyFailableString() const { std::stringstream stream; - auto it = mIsCurrentlyFailableBE.begin(); - stream << "{"; - if(it != mIsCurrentlyFailableBE.end()) { - stream << *it; - } - ++it; - while(it != mIsCurrentlyFailableBE.end()) { - stream << ", " << *it; + if (nrFailableDependencies() > 0) { + auto it = mFailableDependencies.begin(); + stream << "{Dependencies: "; + if (it != mFailableDependencies.end()) { + stream << *it; + } + ++it; + while(it != mFailableDependencies.end()) { + stream << ", " << *it; + ++it; + } + stream << "} "; + } else { + auto it = mIsCurrentlyFailableBE.begin(); + stream << "{"; + if(it != mIsCurrentlyFailableBE.end()) { + stream << *it; + } ++it; + while(it != mIsCurrentlyFailableBE.end()) { + stream << ", " << *it; + ++it; + } + stream << "}"; } - stream << "}"; return stream.str(); }