Refactoring DFT elements

src/storm-dft/builder/DFTBuilder.cpp

@@ -74,12 +74,10 @@ namespace storm {
                         childElement->addOutgoingDependency(elem.first);
                     }
                 }
-                if (binaryDependencies) {
-                    STORM_LOG_ASSERT(dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element.");
-                }
-                elem.first->setDependentEvents(dependencies);
-                for (auto& dependency : dependencies) {
-                    dependency->addIngoingDependency(elem.first);
+                STORM_LOG_ASSERT(!binaryDependencies || dependencies.size() == 1, "Dependency '" << elem.first->name() << "' should only have one dependent element.");
+                for (auto& be : dependencies) {
+                    elem.first->addDependentEvent(be);
+                    be->addIngoingDependency(elem.first);
                 }
                 
             }

src/storm-dft/storage/dft/DFT.cpp

@@ -621,6 +621,7 @@ namespace storm {
                     }
                 }
             }
+            // TODO check VOT gates
             return wellformed;
         }
 

src/storm-dft/storage/dft/elements/BEConst.h

@@ -7,6 +7,7 @@ namespace storm {
 
         /*!
          * BE which is either constant failed or constant failsafe.
+         * The BE is either always failed (from the beginning) or can never fail (failsafe).
          */
         template<typename ValueType>
         class BEConst : public DFTBE<ValueType> {
@@ -38,7 +39,7 @@ namespace storm {
                 return this->failed();
             }
 
-            bool isTypeEqualTo(DFTElement <ValueType> const& other) const override {
+            bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
                 if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
                     return false;
                 }

src/storm-dft/storage/dft/elements/BEExponential.h

@@ -78,7 +78,7 @@ namespace storm {
                 return storm::utility::isZero(this->passiveFailureRate());
             }
 
-            bool isTypeEqualTo(DFTElement <ValueType> const& other) const override {
+            bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
                 if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
                     return false;
                 }

src/storm-dft/storage/dft/elements/DFTAnd.h

@@ -1,43 +1,52 @@
 #pragma once
+
 #include "DFTGate.h"
 
 namespace storm {
     namespace storage {
+
+        /*!
+         * AND gate.
+         * Fails if all children have failed.
+         */
         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)
-            {}
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param children Children.
+             */
+            DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children) {
+                // Intentionally empty
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::AND;
+            }
 
             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())) {
+                if (state.isOperational(this->mId)) {
+                    for (auto const& child : this->mChildren) {
+                        if (!state.hasFailed(child->id())) {
                             return;
                         }
                     }
+                    // All children have failed
                     this->fail(state, queues);
                 }
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
-                if(state.isOperational(this->mId)) {
+                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";
-            }
         };
 
     }

src/storm-dft/storage/dft/elements/DFTBE.h

@@ -6,7 +6,8 @@ namespace storm {
     namespace storage {
 
         /*!
-         * Abstract base class for basic elements (BEs) in DFTs.
+         * Abstract base class for basic events (BEs) in DFTs.
+         * BEs are atomic and not further subdivided.
          */
         template<typename ValueType>
         class DFTBE : public DFTElement<ValueType> {
@@ -36,8 +37,7 @@ namespace storm {
              * @param dependency Ingoing dependency.
              */
             void addIngoingDependency(std::shared_ptr<DFTDependency<ValueType>> const& dependency) {
-                // TODO write this assertion for n-ary dependencies, probably by adding a method to the dependencies to support this.
-                //STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match.");
+                STORM_LOG_ASSERT(dependency->containsDependentEvent(this->id()), "Dependency " << *dependency << " has no dependent BE " << *this << ".");
                 STORM_LOG_ASSERT(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), dependency) == mIngoingDependencies.end(),
                                  "Ingoing Dependency " << dependency << " already present.");
                 mIngoingDependencies.push_back(dependency);
@@ -69,19 +69,19 @@ namespace storm {
                 }
                 DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                 if (elemsInSubtree.empty()) {
-                    // Parent in the subdft, ie it is *not* a subdft
+                    // Parent in the subDFT, i.e., it is *not* a subDFT
                     return;
                 }
-                for (auto const& incDep : ingoingDependencies()) {
-                    incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+                for (auto const& inDep : ingoingDependencies()) {
+                    inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
                     if (elemsInSubtree.empty()) {
-                        // Parent in the subdft, ie it is *not* a subdft
+                        // Parent in the subDFT, i.e., it is *not* a subDFT
                         return;
                     }
                 }
             }
 
-            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 if (DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {
                     state.beNoLongerFailable(this->id());
                     return true;

src/storm-dft/storage/dft/elements/DFTDependency.h

@@ -1,98 +1,151 @@
 #pragma once
 
-
 #include "DFTElement.h"
+
 namespace storm {
     namespace storage {
 
+        /*!
+         * Dependency gate with probability p.
+         * If p=1 the gate is a functional dependency (FDEP), otherwise it is a probabilistic dependency (PDEP).
+         *
+         * If the trigger event (i.e., the first child) fails, a coin is flipped.
+         * With probability p the failure is forwarded to all other children.
+         * With probability 1-p the failure is not forwarded and the dependency has no effect.
+         *
+         * The failure forwarding to the children happens in a strict (non-deterministically chosen) order.
+         */
         template<typename ValueType>
         class DFTDependency : public DFTElement<ValueType> {
 
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
 
-        protected:
-            ValueType mProbability;
-            DFTGatePointer mTriggerEvent;
-            std::vector<DFTBEPointer> mDependentEvents;
-
         public:
-            DFTDependency(size_t id, std::string const& name, ValueType probability) :
-                DFTElement<ValueType>(id, name), mProbability(probability)
-            {
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param probability Probability p of failure forwarding.
+             */
+            DFTDependency(size_t id, std::string const& name, ValueType probability) : DFTElement<ValueType>(id, name), mProbability(probability) {
+                // We cannot assert 0<=p<=1 in general, because ValueType might be RationalFunction.
             }
 
-            virtual ~DFTDependency() {}
-
-            void setTriggerElement(DFTGatePointer const& triggerEvent) {
-                mTriggerEvent = triggerEvent;
-
-            }
-
-            void setDependentEvents(std::vector<DFTBEPointer> const& dependentEvents) {
-                mDependentEvents = dependentEvents;
+            DFTElementType type() const override {
+                return DFTElementType::PDEP;
             }
 
-
+            /*!
+             * Get probability of forwarding the failure.
+             * @return Probability.
+             */
             ValueType const& probability() const {
                 return mProbability;
             }
 
+            /*!
+             * Get trigger event, i.e., the first child.
+             * @return Trigger event.
+             */
             DFTGatePointer const& triggerEvent() const {
                 STORM_LOG_ASSERT(mTriggerEvent, "Trigger does not exist.");
                 return mTriggerEvent;
             }
 
+            /*!
+             * Set the trigger event, i.e., the first child.
+             * @param triggerEvent Trigger event.
+             */
+            void setTriggerElement(DFTGatePointer const& triggerEvent) {
+                mTriggerEvent = triggerEvent;
+            }
+
+            /*!
+             * Get dependent events.
+             * @return Dependent events.
+             */
             std::vector<DFTBEPointer> const& dependentEvents() const {
-                STORM_LOG_ASSERT(mDependentEvents.size() > 0, "Dependent element does not exists.");
+                STORM_LOG_ASSERT(mDependentEvents.size() > 0, "Dependent event does not exists.");
                 return mDependentEvents;
             }
 
-            DFTElementType type() const override {
-                return DFTElementType::PDEP;
+            /*!
+             * Add dependent event.
+             * @param dependentEvent Dependent event.
+             */
+            void addDependentEvent(DFTBEPointer const& dependentEvent) {
+                mDependentEvents.push_back(dependentEvent);
             }
 
+            /*!
+             * Check whether the given element is a dependent event.
+             * @param id Id of element to search for.
+             * @return True iff element was found in dependent events.
+             */
+            bool containsDependentEvent(size_t id) {
+                auto it = std::find_if(this->mDependentEvents.begin(), this->mDependentEvents.end(), [&id](DFTBEPointer be) -> bool {
+                    return be->id() == id;
+                });
+                return it != this->mDependentEvents.end();
+            }
+
+
             virtual size_t nrChildren() const override {
                 return 1;
             }
 
-            virtual bool isDependency() const override {
+            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);
+            /*!
+             * Check whether the dependency is an FDEP, i.e., p=1.
+             * @return True iff p=1.
+             */
+            bool isFDEP() const {
+                return storm::utility::isOne(this->probability());
             }
 
-            virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+            bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+                if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
+                    return false;
+                }
+                auto& otherDEP = static_cast<DFTDependency<ValueType> const&>(other);
+                return this->probability() == otherDEP.probability();
+            }
+
+            void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
                 // Do nothing
             }
 
-            virtual std::vector<size_t> independentUnit() const override {
+            std::vector<size_t> independentUnit() const override {
                 std::set<size_t> unit = {this->mId};
-                for(auto const& depEv : mDependentEvents) {
+                for (auto const& depEv : mDependentEvents) {
                     depEv->extendUnit(unit);
-                    if(unit.count(mTriggerEvent->id()) != 0) {
+                    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, bool sparesAsLeaves) const override {
-                if(elemsInSubtree.count(this->id())) return;
+            void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
+                if (elemsInSubtree.count(this->id())) {
+                    return;
+                }
                 DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
-                if(elemsInSubtree.empty()) {
+                if (elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
                 for (auto const& depEv : mDependentEvents) {
                     depEv->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
-                    if (elemsInSubtree.empty()) return;
+                    if (elemsInSubtree.empty()) {
+                        return;
+                    }
                 }
-                if(elemsInSubtree.empty()) {
+                if (elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
@@ -100,21 +153,23 @@ namespace storm {
 
             }
 
-            virtual std::string toString() const override {
+            std::string toString() const override {
                 std::stringstream stream;
-                bool isFDEP = storm::utility::isOne(this->probability());
-                stream << "{" << this->name() << "} " << (isFDEP ? "FDEP" : "PDEP") << "(" << this->triggerEvent()->name() << " => { ";
-                for(auto const& depEv : this->dependentEvents()) {
+                stream << "{" << this->name() << "} " << (this->isFDEP() ? "FDEP" : "PDEP") << "(" << this->triggerEvent()->name() << " => { ";
+                for (auto const& depEv : this->dependentEvents()) {
                     stream << depEv->name() << " ";
                 }
                 stream << "}";
-                if (!isFDEP) {
+                if (!this->isFDEP()) {
                     stream << " with probability " << this->probability();
                 }
                 return stream.str();
             }
 
-        protected:
+        private:
+            ValueType mProbability;
+            DFTGatePointer mTriggerEvent;
+            std::vector<DFTBEPointer> mDependentEvents;
 
         };
 

src/storm-dft/storage/dft/elements/DFTGate.h

@@ -40,7 +40,9 @@ namespace storm {
             }
             
             
-            virtual std::string typestring() const = 0;
+            virtual std::string typestring() const {
+                return storm::storage::toString(this->type());
+            }
 
             virtual void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const = 0;
 

src/storm-dft/storage/dft/elements/DFTOr.h

@@ -1,39 +1,49 @@
 #pragma once
 
 #include "DFTGate.h"
+
 namespace storm {
     namespace storage {
+
+        /*!
+         * OR gate.
+         * Fails if at least one child has failed.
+         */
         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)
-            {}
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param children Children.
+             */
+            DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children) {
+                // Intentionally empty
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::OR;
+            }
 
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 STORM_LOG_ASSERT(this->hasFailedChild(state), "No failed child.");
-                if(state.isOperational(this->mId)) {
+                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;
+                for (auto const& child : this->mChildren) {
+                    if (!state.isFailsafe(child->id())) {
+                        return;
+                    }
+                }
+                // All chidren are failsafe
+                this->failsafe(state, queues);
             }
 
-            std::string typestring() const override {
-                return "OR";
-            }
         };
 
     }

src/storm-dft/storage/dft/elements/DFTPand.h

@@ -1,57 +1,78 @@
 #pragma once
 
 #include "DFTGate.h"
+
 namespace storm {
     namespace storage {
-          template<typename ValueType>
+
+        /*!
+         * Priority AND (PAND) gate.
+         * Fails if all children fail in order from first to last child.
+         * If a child fails before its left sibling, the PAND becomes failsafe.
+         * For inclusive PAND<= gates, simultaneous failures are allowed.
+         * For exclusive PAND< gates, simultaneous failure make the gate failsafe.
+         */
+        template<typename ValueType>
         class DFTPand : public DFTGate<ValueType> {
 
         public:
-            DFTPand(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
-                    DFTGate<ValueType>(id, name, children),
-                    inclusive(inclusive)
-            {}
-
-            void checkFails(storm::storage::DFTState<ValueType>& state,  DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(inclusive);
-                if(state.isOperational(this->mId)) {
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param inclusive If true, simultaneous failures are allowed.
+             * parame children Children.
+             */
+            DFTPand(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children), inclusive(inclusive) {
+                // Intentionally left empty.
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::PAND;
+            }
+
+            std::string typestring() const override {
+                return isInclusive() ? "PAND (incl)" : "PAND (excl)";
+            }
+
+            /*!
+             * Return whether the PAND is inclusive.
+             * @return True iff PAND is inclusive.
+             */
+            bool isInclusive() const {
+                return inclusive;
+            }
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+                STORM_LOG_ASSERT(isInclusive(), "Exclusive PAND not supported.");
+                if (state.isOperational(this->mId)) {
                     bool childOperationalBefore = false;
-                    for(auto const& child : this->mChildren)
-                    {
-                        if(!state.hasFailed(child->id())) {
+                    for (auto const& child : this->mChildren) {
+                        if (!state.hasFailed(child->id())) {
                             childOperationalBefore = true;
-                        } else if(childOperationalBefore && state.hasFailed(child->id())){
+                        } else if (childOperationalBefore && state.hasFailed(child->id())) {
+                            // Child failed before sibling -> failsafe
                             this->failsafe(state, queues);
                             this->childrenDontCare(state, queues);
                             return;
                         }
                     }
-                    if(!childOperationalBefore) {
+                    if (!childOperationalBefore) {
+                        // All children have failed
                         this->fail(state, queues);
                     }
                 }
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(inclusive);
+                STORM_LOG_ASSERT(isInclusive(), "Exclusive PAND not supported.");
                 STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
-                if(state.isOperational(this->mId)) {
+                if (state.isOperational(this->mId)) {
                     this->failsafe(state, queues);
                     this->childrenDontCare(state, queues);
                 }
             }
 
-            virtual DFTElementType type() const override {
-                return DFTElementType::PAND;
-            }
-            
-            bool isInclusive() const {
-                return inclusive;
-            }
-            
-            std::string typestring() const override {
-                return inclusive ? "PAND-inc" : "PAND-ex";
-            }
         protected:
             bool inclusive;
         };

src/storm-dft/storage/dft/elements/DFTPor.h

@@ -1,53 +1,76 @@
 #pragma once
 
 #include "DFTGate.h"
+
 namespace storm {
     namespace storage {
+
+        /*!
+         * Priority OR (POR) gate.
+         * Fails if the leftmost child fails before all other children.
+         * If a child fails before the leftmost child, the POR becomes failsafe.
+         * For inclusive POR<= gates, simultaneous failures are allowed.
+         * For exclusive POR< gates, simultaneous failures make the gate failsafe.
+         */
         template<typename ValueType>
         class DFTPor : public DFTGate<ValueType> {
         public:
-            DFTPor(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
-                    DFTGate<ValueType>(id, name, children),
-                    inclusive(inclusive)
-            {}
-
-            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(inclusive);
-                if(state.isOperational(this->mId)) {
-                    if (state.hasFailed(this->mChildren.front()->id())) {
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param inclusive If true, simultaneous failures are allowed.
+             * parame children Children.
+             */
+            DFTPor(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) : DFTGate<ValueType>(id, name, children), inclusive(inclusive) {
+                // Intentionally left empty.
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::POR;
+            }
+
+            std::string typestring() const override {
+                return isInclusive() ? "POR (incl)" : "POR (excl)";
+            }
+
+            /*!
+             * Return whether the PAND is inclusive.
+             * @return True iff PAND is inclusive.
+             */
+            bool isInclusive() const {
+                return inclusive;
+            }
+
+            void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
+                STORM_LOG_ASSERT(isInclusive(), "Exclusive POR not supported.");
+                if (state.isOperational(this->mId)) {
+                    auto childIter = this->mChildren.begin();
+                    if (state.hasFailed((*childIter)->id())) {
                         // First child has failed before others
                         this->fail(state, queues);
-                    } else {
-                        for (size_t i = 1; i < this->nrChildren(); ++i) {
-                            if (state.hasFailed(this->mChildren[i]->id())) {
-                                // Child has failed before first child
-                                this->failsafe(state, queues);
-                                this->childrenDontCare(state, queues);
-                            }
+                        return;
+                    }
+                    // Iterate over other children
+                    for (; childIter != this->mChildren.end(); ++childIter) {
+                        if (state.hasFailed((*childIter)->id())) {
+                            // Child has failed before first child
+                            this->failsafe(state, queues);
+                            this->childrenDontCare(state, queues);
                         }
                     }
                 }
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(inclusive);
+                STORM_LOG_ASSERT(isInclusive(), "Exclusive POR not supported.");
+                // If first child is not failsafe, it could still fail.
                 if (state.isFailsafe(this->mChildren.front()->id())) {
                     this->failsafe(state, queues);
                     this->childrenDontCare(state, queues);
                 }
             }
 
-            virtual DFTElementType type() const override {
-                return DFTElementType::POR;
-            }
-            
-            std::string  typestring() const override {
-                return inclusive ? "POR-inc" : "POR-ex";
-            }
-            
-            bool isInclusive() const {
-                return inclusive;
-            }
         protected:
             bool inclusive;
         };

src/storm-dft/storage/dft/elements/DFTVot.h

@@ -1,29 +1,53 @@
 #pragma once
+
 #include "DFTGate.h"
+
 namespace storm {
     namespace storage {
 
-
+        /*!
+         * VOT gate with threshold k.
+         * Fails if k children have failed.
+         */
         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)
-            {}
+            /*!
+             * Constructor.
+             * @param id Id.
+             * @param name Name.
+             * @param threshold Threshold k, nr of failed children needed for failure.
+             * @param children Children.
+             */
+            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) {
+                STORM_LOG_ASSERT(mThreshold > 1, "Should use OR gate instead of VOT1");
+                // k=n cannot be checked as children might be added later
+            }
+
+            /*!
+             * Get the threshold k.
+             * @return Threshold.
+             */
+            unsigned threshold() const {
+                return mThreshold;
+            }
+
+            DFTElementType type() const override {
+                return DFTElementType::VOT;
+            }
+
+            std::string typestring() const override {
+                return storm::storage::toString(this->type()) + " (" + std::to_string(mThreshold) + ")";
+            }
 
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                if(state.isOperational(this->mId)) {
+                if (state.isOperational(this->mId)) {
                     unsigned nrFailedChildren = 0;
-                    for(auto const& child : this->mChildren)
-                    {
-                        if(state.hasFailed(child->id())) {
+                    for (auto const& child : this->mChildren) {
+                        if (state.hasFailed(child->id())) {
                             ++nrFailedChildren;
-                            if(nrFailedChildren >= mThreshold) 
-                            {
+                            if (nrFailedChildren >= mThreshold) {
                                 this->fail(state, queues);
                                 return;
                             }
@@ -35,14 +59,12 @@ namespace storm {
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
-                if(state.isOperational(this->mId)) {
+                if (state.isOperational(this->mId)) {
                     unsigned nrFailsafeChildren = 0;
-                    for(auto const& child : this->mChildren)
-                    {
-                        if(state.isFailsafe(child->id())) {
+                    for (auto const& child : this->mChildren) {
+                        if (state.isFailsafe(child->id())) {
                             ++nrFailsafeChildren;
-                            if(nrFailsafeChildren > this->nrChildren() - mThreshold)
-                            {
+                            if (nrFailsafeChildren > this->nrChildren() - mThreshold) {
                                 this->failsafe(state, queues);
                                 this->childrenDontCare(state, queues);
                                 return;
@@ -52,23 +74,17 @@ namespace storm {
                 }
             }
 
-            unsigned threshold() const {
-                return mThreshold;
-            }
-
-            virtual DFTElementType type() const override {
-                return DFTElementType::VOT;
+            bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+                if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
+                    return false;
+                }
+                auto& otherVOT = static_cast<DFTVot<ValueType> const&>(other);
+                return this->threshold() == otherVOT.threshold();
             }
 
-            std::string typestring() const override{
-                return "VOT (" + std::to_string(mThreshold) + ")";
-            }
+        private:
+            unsigned 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);
-            }
         };
 
     }