From c78d9ff80222c373589b4b7af5ce4d77b1a61465 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 17 Feb 2016 11:21:46 +0100 Subject: [PATCH] Fixed problems with pdeps Former-commit-id: c46c88b1779b51b6d052fe9cb462d37dc8973e31 --- benchmark_dft.py | 3 +- examples/dft/pdep3.dft | 5 +++ src/builder/ExplicitDFTModelBuilder.cpp | 42 ++++++++++++++++++--- src/storage/dft/DFT.cpp | 32 ++++++++++------ src/storage/dft/DFTBuilder.cpp | 1 + src/storage/dft/DFTElementState.h | 50 ++++++++++++++++++++++++- src/storage/dft/DFTElements.cpp | 2 +- src/storage/dft/DFTElements.h | 32 +++++++++++++++- src/storage/dft/DFTState.cpp | 42 ++++++++++++++++++++- src/storage/dft/DFTState.h | 23 +++++++++++- 10 files changed, 207 insertions(+), 25 deletions(-) create mode 100644 examples/dft/pdep3.dft diff --git a/benchmark_dft.py b/benchmark_dft.py index dfcecd15f..77880d951 100644 --- a/benchmark_dft.py +++ b/benchmark_dft.py @@ -31,8 +31,9 @@ benchmarks = [ ("or", False, [1, 1]), ("pand", False, ["inf", 0.666667]), ("pand_param", True, ["-1", "(x)/(y+x)"]), - ("pdep", False, [0, 1]), #Compute + ("pdep", False, [2.66667, 1]), ("pdep2", False, [0, 1]), #Compute + ("pdep3", False, [2.79167, 1]), ("spare", False, [3.53846, 1]), ("spare2", False, [1.86957, 1]), ("spare3", False, [1.27273, 1]), diff --git a/examples/dft/pdep3.dft b/examples/dft/pdep3.dft new file mode 100644 index 000000000..a9a73f472 --- /dev/null +++ b/examples/dft/pdep3.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" and "B" "C" "F"; +"F" pdep=0.3 "B" "C"; +"B" lambda=0.4 dorm=0; +"C" lambda=0.8 dorm=0; diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index aa4d46f15..160535443 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -77,17 +77,20 @@ namespace storm { // TODO Matthias: avoid transforming back and forth storm::storage::SparseMatrix rateMatrix(modelComponents.transitionMatrix); for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { + assert(row < modelComponents.markovianStates.size()); if (modelComponents.markovianStates.get(row)) { for (auto& entry : rateMatrix.getRow(row)) { entry.setValue(entry.getValue() * modelComponents.exitRates[row]); } } } + if (deterministic) { model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling)); } else { model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); } + model->printModelInformationToStream(std::cout); return model; } @@ -143,9 +146,6 @@ namespace storm { 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; @@ -169,6 +169,9 @@ namespace storm { DFTElementPointer next = queues.nextDontCarePropagation(); next->checkDontCareAnymore(*newState, queues); } + + // Update failable dependencies + newState->updateFailableDependencies(nextBE->id()); if (mStates.contains(newState->status())) { // State already exists @@ -180,7 +183,7 @@ namespace storm { mStates.findOrAdd(newState->status(), newState); STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); - // Add state to search + // Add state to search queue stateQueue.push(newState); } @@ -188,8 +191,37 @@ namespace storm { if (hasDependencies) { // Failure is due to dependency -> add non-deterministic choice std::shared_ptr const> dependency = mDft.getDependency(state->getDependencyId(smallest-1)); - transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), dependency->probability()); + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, newState->getId(), dependency->probability()); STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with probability " << dependency->probability()); + + if (!storm::utility::isOne(dependency->probability())) { + // Add transition to state where dependency was unsuccessful + DFTStatePointer unsuccessfulState = std::make_shared>(*state); + unsuccessfulState->letDependencyBeUnsuccessful(smallest-1); + + if (mStates.contains(unsuccessfulState->status())) { + // Unsuccessful state already exists + unsuccessfulState = mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState); + STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists"); + } else { + // New unsuccessful state + unsuccessfulState->setId(newIndex++); + mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState); + STORM_LOG_TRACE("New state " << mDft.getStateString(unsuccessfulState)); + + // Add unsuccessful state to search queue + stateQueue.push(unsuccessfulState); + } + + ValueType remainingProbability = storm::utility::one() - dependency->probability(); + transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, unsuccessfulState->getId(), remainingProbability); + STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << unsuccessfulState->getId() << " with probability " << remainingProbability); + } else { + // Self-loop with probability one cannot be eliminated later one. + assert(state->getId() != newState->getId()); + } + ++rowOffset; + } else { // Set failure rate according to usage bool isUsed = true; diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index b3f0dce7a..83e287b3b 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -118,13 +118,17 @@ namespace storm { for (auto const& elem : mElements) { stream << "[" << elem->id() << "]"; stream << elem->toString(); - stream << "\t** " << state->getElementState(elem->id()); - if(elem->isSpareGate()) { - if(state->isActiveSpare(elem->id())) { - stream << " actively"; + if (elem->isDependency()) { + stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id())); + } else { + stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id())); + if(elem->isSpareGate()) { + if(state->isActiveSpare(elem->id())) { + stream << " actively"; + } + stream << " using " << state->uses(elem->id()); } - stream << " using " << state->uses(elem->id()); - } + } stream << std::endl; } return stream.str(); @@ -135,13 +139,17 @@ namespace storm { std::stringstream stream; stream << "(" << state->getId() << ") "; for (auto const& elem : mElements) { - stream << state->getElementStateInt(elem->id()); - if(elem->isSpareGate()) { - stream << "["; - if(state->isActiveSpare(elem->id())) { - stream << "actively "; + if (elem->isDependency()) { + stream << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]"; + } else { + stream << storm::storage::toChar(state->getElementState(elem->id())); + if(elem->isSpareGate()) { + stream << "["; + if(state->isActiveSpare(elem->id())) { + stream << "actively "; + } + stream << "using " << state->uses(elem->id()) << "]"; } - stream << "using " << state->uses(elem->id()) << "]"; } } return stream.str(); diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 00e416d54..13ed7d7b0 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -40,6 +40,7 @@ namespace storm { DFTGatePointer triggerEvent = std::static_pointer_cast>(mElements[dependency->nameTrigger()]); std::shared_ptr> dependentEvent = std::static_pointer_cast>(mElements[dependency->nameDependent()]); dependency->initialize(triggerEvent, dependentEvent); + triggerEvent->addDependency(dependency); } // Sort elements topologically diff --git a/src/storage/dft/DFTElementState.h b/src/storage/dft/DFTElementState.h index 1926745bf..d191cc2d9 100644 --- a/src/storage/dft/DFTElementState.h +++ b/src/storage/dft/DFTElementState.h @@ -2,9 +2,11 @@ #ifndef DFTELEMENTSTATE_H #define DFTELEMENTSTATE_H +#include + namespace storm { namespace storage { - enum class DFTElementState {Operational = 0, Failed = 2, Failsafe = 1, DontCare = 3}; + enum class DFTElementState {Operational = 0, Failed = 2, Failsafe = 1, DontCare = 3}; inline std::ostream& operator<<(std::ostream& os, DFTElementState st) { switch(st) { @@ -17,7 +19,53 @@ namespace storm { case DFTElementState::DontCare: return os << "Don't Care"; } + assert(false); + } + + inline char toChar(DFTElementState st) { + switch(st) { + case DFTElementState::Operational: + return 'O'; + case DFTElementState::Failed: + return 'F'; + case DFTElementState::Failsafe: + return 'S'; + case DFTElementState::DontCare: + return '-'; + } + assert(false); + } + + enum class DFTDependencyState {Passive = 0, Unsuccessful = 1, Successful = 2, DontCare = 3}; + + inline std::ostream& operator<<(std::ostream& os, DFTDependencyState st) { + switch(st) { + case DFTDependencyState::Passive: + return os << "Passive"; + case DFTDependencyState::Successful: + return os << "Successful"; + case DFTDependencyState::Unsuccessful: + return os << "Unsuccessful"; + case DFTDependencyState::DontCare: + return os << "Don't Care"; + } + assert(false); } + + inline char toChar(DFTDependencyState st) { + switch(st) { + case DFTDependencyState::Passive: + return 'P'; + case DFTDependencyState::Successful: + return 'S'; + case DFTDependencyState::Unsuccessful: + return 'U'; + case DFTDependencyState::DontCare: + return '-'; + } + assert(false); + } + } } diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp index d5b089c84..5597f1c5e 100644 --- a/src/storage/dft/DFTElements.cpp +++ b/src/storage/dft/DFTElements.cpp @@ -7,7 +7,7 @@ namespace storm { template bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { - if(!state.dontCare(mId)) + if(!state.dontCare(mId) && !hasDependencies()) { for(DFTGatePointer const& parent : mParents) { if(state.isOperational(parent->id())) { diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 9778d9146..e49b91901 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -23,12 +23,17 @@ namespace storm { template class DFTGate; + + template + class DFTDependency; template class DFTElement { using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; + using DFTDependencyPointer = std::shared_ptr>; + using DFTDependencyVector = std::vector; protected: @@ -36,6 +41,7 @@ namespace storm { std::string mName; size_t mRank = -1; DFTGateVector mParents; + DFTDependencyVector dependencies; public: DFTElement(size_t id, std::string const& name) : @@ -132,6 +138,29 @@ namespace storm { } return res; } + + bool addDependency(DFTDependencyPointer const& e) { + if(std::find(dependencies.begin(), dependencies.end(), e) != dependencies.end()) { + return false; + } + else + { + dependencies.push_back(e); + return true; + } + } + + bool hasDependencies() const { + return !dependencies.empty(); + } + + size_t nrDependencies() const { + return dependencies.size(); + } + + DFTDependencyVector const& getDependencies() const { + return dependencies; + } virtual void extendSpareModule(std::set& elementsInModule) const; @@ -433,8 +462,7 @@ namespace storm { using DFTGatePointer = std::shared_ptr>; using DFTBEPointer = std::shared_ptr>; - using DFTBEVector = std::vector; - + protected: std::string mNameTrigger; std::string mNameDependent; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 8714f0130..53d0f8761 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -19,6 +19,11 @@ namespace storm { DFTElementState DFTState::getElementState(size_t id) const { return static_cast(getElementStateInt(id)); } + + template + DFTDependencyState DFTState::getDependencyState(size_t id) const { + return static_cast(getElementStateInt(id)); + } template int DFTState::getElementStateInt(size_t id) const { @@ -54,6 +59,20 @@ namespace storm { bool DFTState::dontCare(size_t id) const { return getElementState(id) == DFTElementState::DontCare; } + + template + bool DFTState::dependencyTriggered(size_t id) const { + return getElementStateInt(id) > 0; + } + + template + bool DFTState::dependencySuccessful(size_t id) const { + return mStatus[mDft.failureIndex(id)]; + } + template + bool DFTState::dependencyUnsuccessful(size_t id) const { + return mStatus[mDft.failureIndex(id)+1]; + } template void DFTState::setFailed(size_t id) { @@ -69,6 +88,16 @@ namespace storm { void DFTState::setDontCare(size_t id) { mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast(DFTElementState::DontCare) ); } + + template + void DFTState::setDependencySuccessful(size_t id) { + mStatus.set(mDft.failureIndex(id)); + } + + template + void DFTState::setDependencyUnsuccessful(size_t id) { + mStatus.set(mDft.failureIndex(id)+1); + } template void DFTState::beNoLongerFailable(size_t id) { @@ -84,7 +113,8 @@ namespace storm { for (size_t i = 0; i < mDft.getDependencies().size(); ++i) { std::shared_ptr const> dependency = mDft.getDependency(mDft.getDependencies()[i]); if (dependency->triggerEvent()->id() == id) { - if (!hasFailed(dependency->dependentEvent()->id())) { + if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) { + assert(!isFailsafe(dependency->dependentEvent()->id())); mFailableDependencies.push_back(dependency->id()); STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); } @@ -99,10 +129,12 @@ namespace storm { STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); if (nrFailableDependencies() > 0) { // Consider failure due to dependency + assert(index < nrFailableDependencies()); std::shared_ptr const> dependency = mDft.getDependency(getDependencyId(index)); std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true); mFailableDependencies.erase(mFailableDependencies.begin() + index); setFailed(res.first->id()); + setDependencySuccessful(dependency->id()); return res; } else { // Consider "normal" failure @@ -113,6 +145,14 @@ namespace storm { return res; } } + + template + void DFTState::letDependencyBeUnsuccessful(size_t index) { + assert(nrFailableDependencies() > 0 && index < nrFailableDependencies()); + std::shared_ptr const> dependency = mDft.getDependency(getDependencyId(index)); + mFailableDependencies.erase(mFailableDependencies.begin() + index); + setDependencyUnsuccessful(dependency->id()); + } template void DFTState::activate(size_t repr) { diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 520587a42..450953bd7 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -22,6 +22,7 @@ namespace storm { class DFTState { friend struct std::hash; private: + // Status is bitvector where each element has two bits with the meaning according to DFTElementState storm::storage::BitVector mStatus; size_t mId; std::vector mInactiveSpares; @@ -35,6 +36,8 @@ namespace storm { DFTState(DFT const& dft, size_t id); DFTElementState getElementState(size_t id) const; + + DFTDependencyState getDependencyState(size_t id) const; int getElementStateInt(size_t id) const; @@ -50,12 +53,22 @@ namespace storm { bool dontCare(size_t id) const; + bool dependencyTriggered(size_t id) const; + + bool dependencySuccessful(size_t id) const; + + bool dependencyUnsuccessful(size_t id) const; + void setFailed(size_t id); void setFailsafe(size_t id); void setDontCare(size_t id); + void setDependencySuccessful(size_t id); + + void setDependencyUnsuccessful(size_t id); + void beNoLongerFailable(size_t id); void activate(size_t repr); @@ -135,10 +148,16 @@ namespace storm { /** * Sets the next BE as failed - * @param smallestIndex Index in currentlyFailableBE of BE to fail + * @param index Index in currentlyFailableBE of BE to fail * @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies */ - std::pair const>, bool> letNextBEFail(size_t smallestIndex = 0); + std::pair const>, bool> letNextBEFail(size_t index = 0); + + /** + * Sets the dependency as unsuccesful meaning no BE will fail. + * @param index Index of dependency to fail. + */ + void letDependencyBeUnsuccessful(size_t index = 0); std::string getCurrentlyFailableString() const { std::stringstream stream;