towards restrictions

Former-commit-id: e3baec90ea

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<DFTGatePointer> 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<typename ValueType>
+        bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> 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<DFTSeq < ValueType>>
+                    (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<typename ValueType>
         bool DFTBuilder<ValueType>::addStandardGate(std::string const& name, std::vector<std::string> 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.");

src/storage/dft/DFTBuilder.h

@@ -3,6 +3,7 @@
 #define	DFTBUILDER_H
 
 #include "DFTElements.h"
+#include "elements/DFTRestriction.h"
 #include <iostream>
 #include <unordered_map>
 #include <map>
@@ -21,13 +22,16 @@ namespace storm {
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
             using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
+            using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
 
         private:
             std::size_t mNextId = 0;
             std::string topLevelIdentifier;
             std::unordered_map<std::string, DFTElementPointer> mElements;
             std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
+            std::unordered_map<DFTRestrictionPointer, std::vector<std::string>> mRestrictionChildNames;
             std::vector<DFTDependencyPointer> mDependencies;
+            std::vector<DFTRestrictionPointer> mRestrictions;
             
         public:
             DFTBuilder() {
@@ -53,9 +57,19 @@ namespace storm {
             bool addSpareElement(std::string const& name, std::vector<std::string> const& children) {
                 return addStandardGate(name, children, DFTElementType::SPARE);
             }
+
+            bool addSequenceEnforcer(std::string const& name, std::vector<std::string> const& children) {
+                return addRestriction(name, children, DFTElementType::SEQ);
+            }
+
+            bool addMutex(std::string const& name, std::vector<std::string> const& children) {
+                return addRestriction(name, children, DFTElementType::MUTEX);
+            }
             
             bool addDepElement(std::string const& name, std::vector<std::string> 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<std::string> const& children, DFTElementType tp);
-            
+            bool addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
+
             enum class topoSortColour {WHITE, BLACK, GREY}; 
             
             void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L);

src/storage/dft/DFTElements.h

@@ -26,6 +26,8 @@ namespace storm {
         
         template<typename ValueType>
         class DFTDependency;
+        template<typename ValueType>
+        class DFTRestriction;
 
         template<typename ValueType>
         class DFTElement {
@@ -34,6 +36,9 @@ namespace storm {
             using DFTGateVector = std::vector<DFTGatePointer>;
             using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
             using DFTDependencyVector = std::vector<DFTDependencyPointer>;
+            using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
+            using DFTRestrictionVector = std::vector<DFTRestrictionPointer>;
+
 
         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())) {

src/storage/dft/elements/DFTRestriction.h

@@ -6,8 +6,199 @@ namespace storm {
     namespace storage {
         template<typename ValueType>
         class DFTRestriction : public DFTElement<ValueType> {
-            
+            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementVector = std::vector<DFTElementPointer>;
+        protected:
+            DFTElementVector mChildren;
+
+        public:
+            DFTRestriction(size_t id, std::string const& name, DFTElementVector const& children) :
+            DFTElement<ValueType>(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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+            virtual void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
+
+            virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+                DFTElement<ValueType>::extendSpareModule(elementsInSpareModule);
+                for(auto const& child : mChildren) {
+                    if(elementsInSpareModule.count(child->id()) == 0) {
+                        elementsInSpareModule.insert(child->id());
+                        child->extendSpareModule(elementsInSpareModule);
+                    }
+                }
+            }
+
+            virtual std::vector<size_t> independentUnit() const override {
+                std::set<size_t> unit = {this->mId};
+                for(auto const& child : mChildren) {
+                    child->extendUnit(unit);
+                }
+                return std::vector<size_t>(unit.begin(), unit.end());
+            }
+
+            virtual void extendUnit(std::set<size_t>& unit) const override {
+                DFTElement<ValueType>::extendUnit(unit);
+                for(auto const& child : mChildren) {
+                    child->extendUnit(unit);
+                }
+            }
+
+            virtual std::vector<size_t> independentSubDft() const override {
+                auto prelRes = DFTElement<ValueType>::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<size_t> unit(prelRes.begin(), prelRes.end());
+                std::vector<size_t> 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<size_t>(unit.begin(), unit.end());
+            }
+
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const override {
+                if(elemsInSubtree.count(this->id()) > 0) return;
+                DFTElement<ValueType>::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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
+                    childrenDontCare(state, queues);
+                    return true;
+                }
+                return false;
+            }
+
+
+        protected:
+
+            void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                //state.restrictionViolated(this->mId);
+            }
+
+            void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+
+            }
+
+            void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                queues.propagateDontCare(mChildren);
+            }
+
+            bool hasFailsafeChild(DFTState<ValueType>& state) const {
+                for(auto const& child : mChildren) {
+                    if(state.isFailsafe(child->id()))
+                    {
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+            bool hasFailedChild(DFTState<ValueType>& state) const {
+                for(auto const& child : mChildren) {
+                    if(state.hasFailed(child->id())) {
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+
+
+
         };
-        
+
+        template<typename ValueType>
+        class DFTSeq : public DFTRestriction<ValueType> {
+
+
+        public:
+            DFTSeq(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTRestriction<ValueType>(id, name, children)
+            {}
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& 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<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                assert(this->hasFailsafeChild(state));
+
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::SEQ;
+            }
+
+            std::string typestring() const override {
+                return "SEQ";
+            }
+        };
+
     }
 }