splitted elements into single headers

Former-commit-id: 6d0774478d

src/storage/dft/DFT.h

@@ -15,6 +15,7 @@
 #include "SymmetricUnits.h"
 #include "../../utility/math.h"
 #include "src/utility/macros.h"
+#include "DFTStateGenerationInfo.h"
 
 namespace storm {
     namespace storage {
@@ -35,96 +36,6 @@ namespace storm {
         template<typename T> class DFTColouring;
 
         
-        class DFTStateGenerationInfo {
-        private:
-            const size_t mUsageInfoBits;
-            std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
-            std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
-            std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
-            std::map<size_t, size_t> mRestrictedItems;
-            std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups)
-
-        public:
-            
-            DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), mIdToStateIndex(nrElements) {
-                assert(maxSpareChildCount < pow(2, mUsageInfoBits));
-            }
-
-            size_t usageInfoBits() const {
-                return mUsageInfoBits;
-            }
-            
-            void addStateIndex(size_t id, size_t index) {
-                assert(id < mIdToStateIndex.size());
-                mIdToStateIndex[id] = index;
-            }
-
-            void addSpareActivationIndex(size_t id, size_t index) {
-                mSpareActivationIndex[id] = index;
-            }
-
-            void addSpareUsageIndex(size_t id, size_t index) {
-                mSpareUsageIndex[id] = index;
-            }
-
-            size_t getStateIndex(size_t id) const {
-                assert(id < mIdToStateIndex.size());
-                return mIdToStateIndex[id];
-            }
-            
-            size_t getSpareUsageIndex(size_t id) const {
-                assert(mSpareUsageIndex.count(id) > 0);
-                return mSpareUsageIndex.at(id);
-            }
-            
-            size_t getSpareActivationIndex(size_t id) const {
-                assert(mSpareActivationIndex.count(id) > 0);
-                return mSpareActivationIndex.at(id);
-            }
-            
-            void addSymmetry(size_t length, std::vector<size_t>& startingIndices) {
-                mSymmetries.push_back(std::make_pair(length, startingIndices));
-            }
-            
-            size_t getSymmetrySize() const {
-                return mSymmetries.size();
-            }
-            
-            size_t getSymmetryLength(size_t pos) const {
-                assert(pos < mSymmetries.size());
-                return mSymmetries[pos].first;
-            }
-            
-            std::vector<size_t> const& getSymmetryIndices(size_t pos) const {
-                assert(pos < mSymmetries.size());
-                return mSymmetries[pos].second;
-            }
-            
-            friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) {
-                os << "Id to state index:" << std::endl;
-                for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) {
-                    os << id << " -> " << info.getStateIndex(id) << std::endl;
-                }
-                os << "Spare usage index with usage InfoBits of size " << info.mUsageInfoBits << ":" << std::endl;
-                for (auto pair : info.mSpareUsageIndex) {
-                    os << pair.first << " -> " << pair.second << std::endl;
-                }
-                os << "Spare activation index:" << std::endl;
-                for (auto pair : info.mSpareActivationIndex) {
-                    os << pair.first << " -> " << pair.second << std::endl;
-                }
-                os << "Symmetries:" << std::endl;
-                for (auto pair : info.mSymmetries) {
-                    os << "Length: " << pair.first << ", starting indices: ";
-                    for (size_t index : pair.second) {
-                        os << index << ", ";
-                    }
-                    os << std::endl;
-                }
-                return os;
-            }
-            
-        };
         
 
         /**

src/storage/dft/DFTStateGenerationInfo.h

@@ -0,0 +1,96 @@
+#pragma once
+
+namespace storm {
+    namespace storage {
+        class DFTStateGenerationInfo {
+        private:
+            const size_t mUsageInfoBits;
+            std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
+            std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
+            std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
+            std::map<size_t, size_t> mRestrictedItems;
+            std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups)
+
+        public:
+
+            DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), mIdToStateIndex(nrElements) {
+                assert(maxSpareChildCount < pow(2, mUsageInfoBits));
+            }
+
+            size_t usageInfoBits() const {
+                return mUsageInfoBits;
+            }
+
+            void addStateIndex(size_t id, size_t index) {
+                assert(id < mIdToStateIndex.size());
+                mIdToStateIndex[id] = index;
+            }
+
+            void addSpareActivationIndex(size_t id, size_t index) {
+                mSpareActivationIndex[id] = index;
+            }
+
+            void addSpareUsageIndex(size_t id, size_t index) {
+                mSpareUsageIndex[id] = index;
+            }
+
+            size_t getStateIndex(size_t id) const {
+                assert(id < mIdToStateIndex.size());
+                return mIdToStateIndex[id];
+            }
+
+            size_t getSpareUsageIndex(size_t id) const {
+                assert(mSpareUsageIndex.count(id) > 0);
+                return mSpareUsageIndex.at(id);
+            }
+
+            size_t getSpareActivationIndex(size_t id) const {
+                assert(mSpareActivationIndex.count(id) > 0);
+                return mSpareActivationIndex.at(id);
+            }
+
+            void addSymmetry(size_t length, std::vector<size_t>& startingIndices) {
+                mSymmetries.push_back(std::make_pair(length, startingIndices));
+            }
+
+            size_t getSymmetrySize() const {
+                return mSymmetries.size();
+            }
+
+            size_t getSymmetryLength(size_t pos) const {
+                assert(pos < mSymmetries.size());
+                return mSymmetries[pos].first;
+            }
+
+            std::vector<size_t> const& getSymmetryIndices(size_t pos) const {
+                assert(pos < mSymmetries.size());
+                return mSymmetries[pos].second;
+            }
+
+            friend std::ostream& operator<<(std::ostream& os, DFTStateGenerationInfo const& info) {
+                os << "Id to state index:" << std::endl;
+                for (size_t id = 0; id < info.mIdToStateIndex.size(); ++id) {
+                    os << id << " -> " << info.getStateIndex(id) << std::endl;
+                }
+                os << "Spare usage index with usage InfoBits of size " << info.mUsageInfoBits << ":" << std::endl;
+                for (auto pair : info.mSpareUsageIndex) {
+                    os << pair.first << " -> " << pair.second << std::endl;
+                }
+                os << "Spare activation index:" << std::endl;
+                for (auto pair : info.mSpareActivationIndex) {
+                    os << pair.first << " -> " << pair.second << std::endl;
+                }
+                os << "Symmetries:" << std::endl;
+                for (auto pair : info.mSymmetries) {
+                    os << "Length: " << pair.first << ", starting indices: ";
+                    for (size_t index : pair.second) {
+                        os << index << ", ";
+                    }
+                    os << std::endl;
+                }
+                return os;
+            }
+
+        };
+    }
+}

src/storage/dft/elements/DFTAnd.h

@@ -0,0 +1,50 @@
+#pragma once 
+#include "DFTGate.h"
+
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        class DFTAnd : public DFTGate<ValueType> {
+            
+        public:
+            DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
+            {}
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(state.isOperational(this->mId)) {
+                    for(auto const& child : this->mChildren)
+                    {
+                        if(!state.hasFailed(child->id())) {
+                            return;
+                        }
+                    }
+                    this->fail(state, queues);
+                }
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                assert(this->hasFailsafeChild(state));
+                if(state.isOperational(this->mId)) {
+                    this->failsafe(state, queues);
+                    this->childrenDontCare(state, queues);
+                }
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::AND;
+            }
+            
+            std::string typestring() const override {
+                return "AND";
+            }
+        };
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTAnd<ValueType> const& gate) {
+            return os << gate.toString();
+        }
+
+              
+    }
+}

src/storage/dft/elements/DFTBE.h

@@ -0,0 +1,104 @@
+#pragma once
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        class DFTBE : public DFTElement<ValueType> {
+            
+            using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
+            using DFTDependencyVector = std::vector<DFTDependencyPointer>;
+
+        protected:
+            ValueType mActiveFailureRate;
+            ValueType mPassiveFailureRate;
+            DFTDependencyVector mIngoingDependencies;
+
+        public:
+            DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) :
+                    DFTElement<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
+            {}
+
+            DFTElementType type() const override {
+                return DFTElementType::BE;
+            }
+
+            virtual size_t nrChildren() const override {
+                return 0;
+            }
+
+            ValueType const& activeFailureRate() const {
+                return mActiveFailureRate;
+            }
+
+            ValueType const& passiveFailureRate() const {
+                return mPassiveFailureRate;
+            }
+            
+            bool addIngoingDependency(DFTDependencyPointer const& e) {
+                assert(e->dependentEvent()->id() == this->id());
+                if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
+                    return false;
+                }
+                else
+                {
+                    mIngoingDependencies.push_back(e);
+                    return true;
+                }
+            }
+            
+            bool hasIngoingDependencies() const {
+                return !mIngoingDependencies.empty();
+            }
+            
+            size_t nrIngoingDependencies() const {
+                return mIngoingDependencies.size();
+            }
+            
+            DFTDependencyVector const& ingoingDependencies() const {
+                return mIngoingDependencies;
+            }
+        
+            std::string toString() const override {
+                std::stringstream stream;
+                stream << *this;
+                return stream.str();
+            }
+            
+            bool isBasicElement() const override{
+                return true;
+            }
+            
+            bool isColdBasicElement() const override{
+                return storm::utility::isZero(mPassiveFailureRate);
+            }
+            
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+                 if(elemsInSubtree.count(this->id())) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                for(auto const& incDep : mIngoingDependencies) {
+                    incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                    if(elemsInSubtree.empty()) {
+                        // Parent in the subdft, ie it is *not* a subdft
+                        return;
+                    }
+                }
+            }
+            
+            bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+                if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+                DFTBE<ValueType> const&  otherBE = static_cast<DFTBE<ValueType> const&>(other);
+                return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate);
+            }
+            
+            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override;
+        };
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTBE<ValueType> const& be) {
+            return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
+        }
+    }
+}

src/storage/dft/elements/DFTConst.h

@@ -0,0 +1,47 @@
+#pragma once
+
+
+#include "DFTElement.h"
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        class DFTConst : public DFTElement<ValueType> {
+
+            bool mFailed;
+
+        public:
+            DFTConst(size_t id, std::string const& name, bool failed) :
+                    DFTElement<ValueType>(id, name), mFailed(failed)
+            {}
+
+            DFTElementType type() const override {
+                if(mFailed) {
+                    return DFTElementType::CONSTF;
+                } else {
+                    return DFTElementType::CONSTS;
+                }
+            }
+
+
+            bool failed() const {
+                return mFailed;
+            }
+            
+            virtual bool isConstant() const {
+                return true;
+            }
+            
+            virtual size_t nrChildren() const override {
+                return 0;
+            }
+            
+            
+            bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+                if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+                DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other);
+                return (mFailed == otherCNST.mFailed);
+            }
+
+        };
+    }
+}

src/storage/dft/elements/DFTDependency.h

@@ -0,0 +1,118 @@
+#pragma once
+
+
+#include "DFTElement.h"
+namespace storm {
+    namespace storage {
+        
+        template<typename ValueType>
+        class DFTDependency : public DFTElement<ValueType> {
+
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
+            
+        protected:
+            std::string mNameTrigger;
+            std::string mNameDependent;
+            ValueType mProbability;
+            DFTGatePointer mTriggerEvent;
+            DFTBEPointer mDependentEvent;
+
+        public:
+            DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) :
+                DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability)
+            {
+            }
+
+            virtual ~DFTDependency() {}
+
+            void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) {
+                assert(triggerEvent->name() == mNameTrigger);
+                assert(dependentEvent->name() == mNameDependent);
+                mTriggerEvent = triggerEvent;
+                mDependentEvent = dependentEvent;
+            }
+
+            std::string nameTrigger() const {
+                return mNameTrigger;
+            }
+
+            std::string nameDependent() const {
+                return mNameDependent;
+            }
+
+            ValueType const& probability() const {
+                return mProbability;
+            }
+
+            DFTGatePointer const& triggerEvent() const {
+                assert(mTriggerEvent);
+                return mTriggerEvent;
+            }
+
+            DFTBEPointer const& dependentEvent() const {
+                assert(mDependentEvent);
+                return mDependentEvent;
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::PDEP;
+            }
+
+            virtual size_t nrChildren() const override {
+                return 1;
+            }
+
+            virtual bool isDependency() const override {
+                return true;
+            }
+            
+            virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+                if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+                DFTDependency<ValueType> const& otherDEP= static_cast<DFTDependency<ValueType> const&>(other);
+                return (mProbability == otherDEP.mProbability);
+            }
+            
+
+            virtual std::vector<size_t> independentUnit() const override {
+                std::set<size_t> unit = {this->mId};
+                mDependentEvent->extendUnit(unit);
+                if(unit.count(mTriggerEvent->id()) != 0) {
+                    return {};
+                }
+                return std::vector<size_t>(unit.begin(), unit.end());
+            }
+
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const override {
+                 if(elemsInSubtree.count(this->id())) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                
+                
+            }
+            
+            virtual std::string toString() const override {
+                std::stringstream stream;
+                bool fdep = storm::utility::isOne(mProbability);
+                stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+                if (!fdep) {
+                    stream << " with probability " << mProbability;
+                }
+                return stream.str();
+            }
+
+        protected:
+
+        };
+
+    }
+}

src/storage/dft/elements/DFTElement.h

@@ -0,0 +1,297 @@
+#pragma once 
+
+#include <string>
+#include <cassert>
+#include <cstdlib>
+#include <iostream>
+#include <functional>
+#include <set>
+#include <vector>
+#include <memory>
+
+
+
+#include "../DFTElementType.h"
+#include "../DFTState.h"
+#include "../DFTStateSpaceGenerationQueues.h"
+#include "src/utility/constants.h"
+#include "src/adapters/CarlAdapter.h"
+
+
+
+
+namespace storm {
+    namespace storage {
+        
+        using std::size_t;
+        template<typename ValueType>
+        class DFTGate;
+        
+        template<typename ValueType>
+        class DFTDependency;
+        template<typename ValueType>
+        class DFTRestriction;
+
+        
+        template<typename ValueType>
+        class DFTElement {
+
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            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:
+            std::size_t mId;
+            std::string mName;
+            std::size_t mRank = -1;
+            DFTGateVector mParents;
+            DFTDependencyVector mOutgoingDependencies;
+            DFTRestrictionVector mRestrictions;
+
+
+        public:
+            DFTElement(size_t id, std::string const& name) :
+                    mId(id), mName(name)
+            {}
+
+            virtual ~DFTElement() {}
+
+            /**
+             * Returns the id
+             */
+            virtual size_t id() const {
+                return mId;
+            }
+
+            virtual DFTElementType type() const = 0;
+
+            virtual void setRank(size_t rank) {
+                mRank = rank;
+            }
+            
+            virtual size_t rank() const {
+                return mRank;
+            }
+            
+            virtual bool isConstant() const {
+                return false;
+            }
+            
+            virtual bool isGate() const {
+                return false;
+            }
+
+            /**
+             *  Returns true if the element is a BE
+             */
+            virtual bool isBasicElement() const {
+                return false;
+            }
+            
+            virtual bool isColdBasicElement() const {
+                return false;
+            }
+
+            /**
+             * Returns true if the element is a spare gate
+             */
+            virtual bool isSpareGate() const {
+                return false;
+            }
+
+            virtual bool isDependency() const {
+                return false;
+            }
+            
+            virtual bool isRestriction() const {
+                return false;
+            }
+
+            virtual void setId(size_t newId) {
+                mId = newId;
+            }
+
+            /**
+             * Returns the name
+             */
+            virtual std::string const& name() const {
+                return mName;
+            }
+            
+            bool addParent(DFTGatePointer const& e) {
+                if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
+                    return false;
+                }
+                else 
+                {
+                    mParents.push_back(e);
+                    return true;
+                }
+            }
+
+            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())) {
+                        return false;
+                    }
+                }
+                return true;
+            }
+
+            
+            bool hasParents() const {
+                return !mParents.empty();
+            }
+            
+            size_t nrParents() const {
+                return mParents.size();
+            }
+
+            DFTGateVector const& parents() const {
+                return mParents;
+            }
+            
+            bool hasRestrictions() const {
+                return !mRestrictions.empty();
+            }
+            
+            size_t nrRestrictions() const {
+                return mRestrictions.size();
+            }
+            
+            DFTRestrictionVector const& restrictions() const {
+                return mRestrictions;
+            }
+
+            std::vector<size_t> parentIds() const {
+                std::vector<size_t> res;
+                for(auto parent : parents()) {
+                    res.push_back(parent->id());
+                }
+                return res;
+            }
+            
+            bool addOutgoingDependency(DFTDependencyPointer const& e) {
+                assert(e->triggerEvent()->id() == this->id());
+                if(std::find(mOutgoingDependencies.begin(), mOutgoingDependencies.end(), e) != mOutgoingDependencies.end()) {
+                    return false;
+                }
+                else
+                {
+                    mOutgoingDependencies.push_back(e);
+                    return true;
+                }
+            }
+            
+            bool hasOutgoingDependencies() const {
+                return !mOutgoingDependencies.empty();
+            }
+            
+            size_t nrOutgoingDependencies() const {
+                return mOutgoingDependencies.size();
+            }
+            
+            std::set<DFTElement<ValueType>> restrictedItems() const {
+                std::set<DFTElement<ValueType>> result;
+                for(auto const& restr : mRestrictions) {
+                    bool foundThis = false;
+                    for(auto const& child : restr->children()) {
+                        if(!foundThis) {
+                            if(child->id() == mId) {
+                                foundThis = true;
+                            }
+                        } else if(result.count(child) == 0) {
+                            result.insert(child);
+                        }
+                    }
+                }
+            }
+            
+            std::set<DFTElement<ValueType>> restrictedItemsTC() const {
+                std::set<DFTElement<ValueType>> result;
+                for(auto const& restr : mRestrictions) {
+                    bool foundThis = false;
+                    for(auto const& child : restr->children()) {
+                        if(!foundThis) {
+                            if(child->id() == mId) {
+                                foundThis = true;
+                            }
+                        } else if(result.count(child) == 0) {
+                            result.insert(child);
+                            std::set<DFTElement<ValueType>> tmpRes = child->restrictedItemsTC();
+                            result.insert(tmpRes.begin(), tmpRes.end());
+                        }
+                    }
+                }
+            }
+            
+            DFTDependencyVector const& outgoingDependencies() const {
+                return mOutgoingDependencies;
+            }
+            
+            virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
+
+           // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
+            
+            virtual std::size_t nrChildren() const = 0;
+
+            virtual std::string toString() const = 0;
+
+            virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const;
+
+            /**
+             *  Computes the independent unit of this element, that is, all elements which are direct or indirect successors of an element.
+             */
+            virtual std::vector<size_t> independentUnit() const;
+
+            /**
+             *  Helper to independent unit computation
+             *  @see independentUnit
+             */
+            virtual void extendUnit(std::set<size_t>& unit) const;
+
+            /**
+             *  Computes independent subtrees starting with this element (this), that is, all elements (x) which are connected to either
+             *  - one of the children of the element,
+             *  - a probabilistic dependency
+             *  such that there exists a  path from x to a child of this does not go through this.
+             */
+            virtual std::vector<size_t> independentSubDft(bool blockParents) const;
+            /**
+             * Helper to the independent subtree computation
+             * @see independentSubDft
+             */
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents) const;
+
+            virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
+                return type() == other.type();
+            }
+
+
+        protected:
+           // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector<std::pair<DFTElement const&, DFTElement const&>>& mapping, std::vector<DFTElement const&> const& order ) const = 0;
+
+        };
+        
+        
+       
+          
+        template<typename ValueType>
+        bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
+            return e1.isTypeEqualTo(e2);
+        }
+    }
+}

src/storage/dft/elements/DFTGate.h

@@ -0,0 +1,180 @@
+#pragma once
+
+#include "DFTElement.h"
+namespace storm {
+    namespace storage {
+    template<typename ValueType>
+        class DFTGate : public DFTElement<ValueType> {
+
+            using DFTElementPointer = std::shared_ptr<DFTElement<ValueType>>;
+            using DFTElementVector = std::vector<DFTElementPointer>;
+
+        protected:
+            DFTElementVector mChildren;
+
+        public:
+            DFTGate(size_t id, std::string const& name, DFTElementVector const& children) :
+                    DFTElement<ValueType>(id, name), mChildren(children)
+            {}
+            
+            virtual ~DFTGate() {}
+            
+            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 isGate() 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 {
+                if (!this->isSpareGate()) {
+                    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(bool blockParents) const override {
+                auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
+                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, blockParents);
+                    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, bool blockParents) const override {
+                if(elemsInSubtree.count(this->id()) > 0) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                for(auto const& child : mChildren) {
+                    child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents);
+                    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 {
+                for(std::shared_ptr<DFTGate> parent : this->mParents) {
+                    if(state.isOperational(parent->id())) {
+                        queues.propagateFailure(parent);
+                    }
+                }
+                for(std::shared_ptr<DFTRestriction<ValueType>> restr : this->mRestrictions) {
+                    queues.checkRestrictionLater(restr);
+                }
+                state.setFailed(this->mId);
+                this->childrenDontCare(state, queues);
+            }
+
+            void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                for(std::shared_ptr<DFTGate> parent : this->mParents) {
+                    if(state.isOperational(parent->id())) {
+                        queues.propagateFailsafe(parent);
+                    }
+                }
+                state.setFailsafe(this->mId);
+                this->childrenDontCare(state, queues);
+            }
+            
+            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;
+            }
+            
+        };
+    }
+}

src/storage/dft/elements/DFTOr.h

@@ -0,0 +1,45 @@
+#pragma once 
+
+#include "DFTGate.h"
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        class DFTOr : public DFTGate<ValueType> {
+
+        public:
+            DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
+            {}
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                assert(this->hasFailedChild(state));
+                if(state.isOperational(this->mId)) {
+                    this->fail(state, queues);
+                }
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                 for(auto const& child : this->mChildren) {
+                     if(!state.isFailsafe(child->id())) {
+                         return;
+                     }
+                 }
+                 this->failsafe(state, queues);
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::OR;
+            }
+            
+            std::string typestring() const override {
+                return "OR";
+            }
+        };
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTOr<ValueType> const& gate) {
+            return os << gate.toString();
+        }
+    }
+}
+       

src/storage/dft/elements/DFTPand.h

@@ -0,0 +1,56 @@
+#pragma once 
+
+#include "DFTGate.h"
+namespace storm {
+    namespace storage {
+          template<typename ValueType>
+        class DFTPand : public DFTGate<ValueType> {
+
+        public:
+            DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
+            {}
+
+            void checkFails(storm::storage::DFTState<ValueType>& state,  DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(state.isOperational(this->mId)) {
+                    bool childOperationalBefore = false;
+                    for(auto const& child : this->mChildren)
+                    {
+                        if(!state.hasFailed(child->id())) {
+                            childOperationalBefore = true;
+                        } else if(childOperationalBefore && state.hasFailed(child->id())){
+                            this->failsafe(state, queues);
+                            this->childrenDontCare(state, queues);
+                            return;
+                        }
+                    }
+                    if(!childOperationalBefore) {
+                        this->fail(state, queues);
+                    }
+                }
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                assert(this->hasFailsafeChild(state));
+                if(state.isOperational(this->mId)) {
+                    this->failsafe(state, queues);
+                    this->childrenDontCare(state, queues);
+                }
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::PAND;
+            }
+            
+            std::string typestring() const override {
+                return "PAND";
+            }
+        };
+        
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTPand<ValueType> const& gate) {
+             return os << gate.toString();
+        }
+
+    }
+}

src/storage/dft/elements/DFTPor.h

@@ -0,0 +1,36 @@
+#pragma once 
+
+#include "DFTGate.h"
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        class DFTPor : public DFTGate<ValueType> {
+        public:
+            DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
+            {}
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                 assert(false);
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                assert(false);
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::POR;
+            }
+            
+            std::string  typestring() const override {
+                return "POR";
+            }
+        };
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTPor<ValueType> const& gate) {
+             return os << gate.toString();
+        }
+
+    }
+}

src/storage/dft/elements/DFTRestriction.h

@@ -1,7 +1,6 @@
 #pragma once
 
-#include "../DFTElements.h"
-
+#include "DFTElement.h"
 namespace storm {
     namespace storage {
         template<typename ValueType>

src/storage/dft/elements/DFTSpare.h

@@ -0,0 +1,70 @@
+#pragma once 
+
+
+#include "DFTGate.h"
+namespace storm {
+    namespace storage {
+        
+
+        template<typename ValueType>
+        class DFTSpare : public DFTGate<ValueType> {
+
+        public:
+            DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children)
+            {}
+            
+            std::string typestring() const override {
+                return "SPARE";
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::SPARE;
+            }
+
+            bool isSpareGate() const override {
+                return true;
+            }
+            
+            void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                DFTGate<ValueType>::fail(state, queues);
+                state.finalizeUses(this->mId);
+            }
+            
+            void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+                DFTGate<ValueType>::failsafe(state, queues);
+                state.finalizeUses(this->mId);
+            }
+            
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if (DFTGate<ValueType>::checkDontCareAnymore(state, queues)) {
+                    state.finalizeUses(this->mId);
+                    return true;
+                }
+                return false;
+            }
+            
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(state.isOperational(this->mId)) {
+                    size_t uses = state.uses(this->mId);
+                    if(!state.isOperational(uses)) {
+                        bool claimingSuccessful = state.claimNew(this->mId, uses, this->mChildren);
+                        if(!claimingSuccessful) {
+                            this->fail(state, queues);
+                        }
+                    }                  
+                } 
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(state.isOperational(this->mId)) {
+                    if(state.isFailsafe(state.uses(this->mId))) {
+                        this->failsafe(state, queues);
+                        this->childrenDontCare(state, queues);
+                    }
+                }
+            }
+
+        };
+    }
+}

src/storage/dft/elements/DFTVot.h

@@ -0,0 +1,75 @@
+#pragma once 
+namespace storm {
+    namespace storage {
+        
+
+        template<typename ValueType>
+        class DFTVot : public DFTGate<ValueType> {
+
+        private:
+            unsigned mThreshold;
+
+        public:
+            DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+                    DFTGate<ValueType>(id, name, children), mThreshold(threshold)
+            {}
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                if(state.isOperational(this->mId)) {
+                    unsigned nrFailedChildren = 0;
+                    for(auto const& child : this->mChildren)
+                    {
+                        if(state.hasFailed(child->id())) {
+                            ++nrFailedChildren;
+                            if(nrFailedChildren >= mThreshold) 
+                            {
+                                this->fail(state, queues);
+                                return;
+                            }
+                        }
+                    }
+                  
+                } 
+            }
+
+            void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                assert(this->hasFailsafeChild(state));
+                if(state.isOperational(this->mId)) {
+                    unsigned nrFailsafeChildren = 0;
+                    for(auto const& child : this->mChildren)
+                    {
+                        if(state.isFailsafe(child->id())) {
+                            ++nrFailsafeChildren;
+                            if(nrFailsafeChildren > this->nrChildren() - mThreshold)
+                            {
+                                this->failsafe(state, queues);
+                                this->childrenDontCare(state, queues);
+                                return;
+                            }
+                        }
+                    }
+                }
+            }
+
+            virtual DFTElementType type() const override {
+                return DFTElementType::VOT;
+            }
+            
+            std::string typestring() const override{
+                return "VOT (" + std::to_string(mThreshold) + ")";
+            }
+            
+            virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+                if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+                DFTVot<ValueType> const& otherVOT = static_cast<DFTVot<ValueType> const&>(other);
+                return (mThreshold == otherVOT.mThreshold);
+            }
+        };
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTVot<ValueType> const& gate) {
+            return os << gate.toString();
+        }
+
+    }
+}