From 2a2eefa95645e13f2254497c3a58d332dae06076 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 21 Feb 2016 19:25:38 +0100 Subject: [PATCH] towards restrictions Former-commit-id: e3baec90ea5ea4bf82e91892fd722cc2583a94e0 --- src/storage/dft/DFTBuilder.cpp | 52 +++++- src/storage/dft/DFTBuilder.h | 19 ++- src/storage/dft/DFTElements.h | 20 +++ src/storage/dft/elements/DFTRestriction.h | 195 +++++++++++++++++++++- 4 files changed, 281 insertions(+), 5 deletions(-) diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 1979aea3b..62b022635 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -27,6 +27,7 @@ namespace storm { childElement->addParent(gate); } else { // Child not found -> find first dependent event to assure that child is dependency + // TODO: Not sure whether this is the intended behaviour? auto itFind = mElements.find(child + "_1"); assert(itFind != mElements.end()); assert(itFind->second->isDependency()); @@ -34,6 +35,17 @@ namespace storm { } } } + + for(auto& elem : mRestrictionChildNames) { + for(auto const& childName : elem.second) { + auto itFind = mElements.find(childName); + assert(itFind != mElements.end()); + DFTElementPointer childElement = itFind->second; + assert(!childElement->isDependency() && !childElement->isRestriction()); + elem.first->pushBackChild(childElement); + childElement->addRestriction(elem.first); + } + } // Initialize dependencies for (auto& dependency : mDependencies) { @@ -45,6 +57,17 @@ namespace storm { dependentEvent->addIngoingDependency(dependency); } +// for (auto& restriction : mRestrictions) { +// std::set parentsOfRestrictedElements; +// for (auto& child : restriction->children()) { +// for(DFTGatePointer& parent : child->parents()) { +// parentsOfRestrictedElements.insert(parent); +// } +// } +// +// +// } + // Sort elements topologically // compute rank for (auto& elem : mElements) { @@ -82,6 +105,33 @@ namespace storm { return elem->rank(); } + template + bool DFTBuilder::addRestriction(std::string const& name, std::vector const& children, DFTElementType tp) { + if (children.size() <= 1) { + STORM_LOG_ERROR("Sequence enforcers require at least two children"); + } + if (mElements.count(name) != 0) { + return false; + } + DFTRestrictionPointer restr; + switch (tp) { + case DFTElementType::SEQ: + restr = std::make_shared> + (mNextId++, name); + break; + case DFTElementType::MUTEX: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); + break; + } + + mElements[name] = restr; + mRestrictionChildNames[restr] = children; + mRestrictions.push_back(restr); + } + template bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp) { assert(children.size() > 0); @@ -108,11 +158,11 @@ namespace storm { break; case DFTElementType::BE: case DFTElementType::VOT: + case DFTElementType::PDEP: // Handled separately STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); case DFTElementType::CONSTF: case DFTElementType::CONSTS: - case DFTElementType::PDEP: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 17a16cb49..8ef0d6cf1 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -3,6 +3,7 @@ #define DFTBUILDER_H #include "DFTElements.h" +#include "elements/DFTRestriction.h" #include #include #include @@ -21,13 +22,16 @@ namespace storm { using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; using DFTDependencyPointer = std::shared_ptr>; + using DFTRestrictionPointer = std::shared_ptr>; private: std::size_t mNextId = 0; std::string topLevelIdentifier; std::unordered_map mElements; std::unordered_map> mChildNames; + std::unordered_map> mRestrictionChildNames; std::vector mDependencies; + std::vector mRestrictions; public: DFTBuilder() { @@ -53,9 +57,19 @@ namespace storm { bool addSpareElement(std::string const& name, std::vector const& children) { return addStandardGate(name, children, DFTElementType::SPARE); } + + bool addSequenceEnforcer(std::string const& name, std::vector const& children) { + return addRestriction(name, children, DFTElementType::SEQ); + } + + bool addMutex(std::string const& name, std::vector const& children) { + return addRestriction(name, children, DFTElementType::MUTEX); + } bool addDepElement(std::string const& name, std::vector const& children, ValueType probability) { - assert(children.size() > 1); + if(children.size() <= 1) { + STORM_LOG_ERROR("Dependencies require at least two children"); + } if(mElements.count(name) != 0) { // Element with that name already exists. return false; @@ -138,7 +152,8 @@ namespace storm { unsigned computeRank(DFTElementPointer const& elem); bool addStandardGate(std::string const& name, std::vector const& children, DFTElementType tp); - + bool addRestriction(std::string const& name, std::vector const& children, DFTElementType tp); + enum class topoSortColour {WHITE, BLACK, GREY}; void topoVisit(DFTElementPointer const& n, std::map>& visited, DFTElementVector& L); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index c51e180c7..66e8b3e8a 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -26,6 +26,8 @@ namespace storm { template class DFTDependency; + template + class DFTRestriction; template class DFTElement { @@ -34,6 +36,9 @@ namespace storm { using DFTGateVector = std::vector; using DFTDependencyPointer = std::shared_ptr>; using DFTDependencyVector = std::vector; + using DFTRestrictionPointer = std::shared_ptr>; + using DFTRestrictionVector = std::vector; + protected: size_t mId; @@ -41,6 +46,8 @@ namespace storm { size_t mRank = -1; DFTGateVector mParents; DFTDependencyVector mOutgoingDependencies; + DFTRestrictionVector mRestrictions; + public: DFTElement(size_t id, std::string const& name) : @@ -95,6 +102,10 @@ namespace storm { virtual bool isDependency() const { return false; } + + virtual bool isRestriction() const { + return false; + } virtual void setId(size_t newId) { mId = newId; @@ -118,6 +129,15 @@ namespace storm { } } + bool addRestriction(DFTRestrictionPointer const& e) { + if (std::find(mRestrictions.begin(), mRestrictions.end(), e) != mRestrictions.end()) { + return false; + } else { + mRestrictions.push_back(e); + return true; + } + } + bool hasOnlyStaticParents() const { for(auto const& parent : mParents) { if(!isStaticGateType(parent->type())) { diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h index 8bd586deb..464c49db2 100644 --- a/src/storage/dft/elements/DFTRestriction.h +++ b/src/storage/dft/elements/DFTRestriction.h @@ -6,8 +6,199 @@ namespace storm { namespace storage { template class DFTRestriction : public DFTElement { - + using DFTElementPointer = std::shared_ptr>; + using DFTElementVector = std::vector; + protected: + DFTElementVector mChildren; + + public: + DFTRestriction(size_t id, std::string const& name, DFTElementVector const& children) : + DFTElement(id, name), mChildren(children) + {} + + virtual ~DFTRestriction() {} + + void pushBackChild(DFTElementPointer elem) { + return mChildren.push_back(elem); + } + + size_t nrChildren() const override { + return mChildren.size(); + } + + DFTElementVector const& children() const { + return mChildren; + } + + virtual bool isRestriction() const override { + return true; + } + + + virtual std::string typestring() const = 0; + + virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; + + virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0; + + virtual void extendSpareModule(std::set& elementsInSpareModule) const override { + DFTElement::extendSpareModule(elementsInSpareModule); + for(auto const& child : mChildren) { + if(elementsInSpareModule.count(child->id()) == 0) { + elementsInSpareModule.insert(child->id()); + child->extendSpareModule(elementsInSpareModule); + } + } + } + + virtual std::vector independentUnit() const override { + std::set unit = {this->mId}; + for(auto const& child : mChildren) { + child->extendUnit(unit); + } + return std::vector(unit.begin(), unit.end()); + } + + virtual void extendUnit(std::set& unit) const override { + DFTElement::extendUnit(unit); + for(auto const& child : mChildren) { + child->extendUnit(unit); + } + } + + virtual std::vector independentSubDft() const override { + auto prelRes = DFTElement::independentSubDft(); + if(prelRes.empty()) { + // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft. + return prelRes; + } + std::set unit(prelRes.begin(), prelRes.end()); + std::vector pids = this->parentIds(); + for(auto const& child : mChildren) { + child->extendSubDft(unit, pids); + if(unit.empty()) { + // Parent in the subdft, ie it is *not* a subdft + break; + } + } + return std::vector(unit.begin(), unit.end()); + } + + virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot) const override { + if(elemsInSubtree.count(this->id()) > 0) return; + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + for(auto const& child : mChildren) { + child->extendSubDft(elemsInSubtree, parentsOfSubRoot); + if(elemsInSubtree.empty()) { + // Parent in the subdft, ie it is *not* a subdft + return; + } + } + } + + + virtual std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} " << typestring() << "( "; + typename DFTElementVector::const_iterator it = mChildren.begin(); + stream << (*it)->name(); + ++it; + while(it != mChildren.end()) { + stream << ", " << (*it)->name(); + ++it; + } + stream << ")"; + return stream.str(); + } + + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + if(DFTElement::checkDontCareAnymore(state, queues)) { + childrenDontCare(state, queues); + return true; + } + return false; + } + + + protected: + + void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + //state.restrictionViolated(this->mId); + } + + void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + + } + + void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + queues.propagateDontCare(mChildren); + } + + bool hasFailsafeChild(DFTState& state) const { + for(auto const& child : mChildren) { + if(state.isFailsafe(child->id())) + { + return true; + } + } + return false; + } + + bool hasFailedChild(DFTState& state) const { + for(auto const& child : mChildren) { + if(state.hasFailed(child->id())) { + return true; + } + } + return false; + } + + + + }; - + + template + class DFTSeq : public DFTRestriction { + + + public: + DFTSeq(size_t id, std::string const& name, std::vector>> const& children = {}) : + DFTRestriction(id, name, children) + {} + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + assert(queues.failurePropagationDone()); + bool childOperationalBefore = false; + for(auto const& child : this->mChildren) + { + if(!state.hasFailed(child->id())) { + childOperationalBefore = true; + } else if(childOperationalBefore && state.hasFailed(child->id())){ + this->fail(state, queues); + return; + } + } + + } + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + assert(this->hasFailsafeChild(state)); + + } + + virtual DFTElementType type() const override { + return DFTElementType::SEQ; + } + + std::string typestring() const override { + return "SEQ"; + } + }; + } } \ No newline at end of file