Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft

Former-commit-id: 11e14df42e

src/storage/dft/DFTElementType.h

@@ -6,6 +6,7 @@ namespace storm {
 
         enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQAND = 11};
 
+        
         inline bool isGateType(DFTElementType const& tp) {
             switch(tp) {
                 case DFTElementType::AND:
@@ -24,9 +25,30 @@ namespace storm {
                     return false;
                 default:
                     assert(false);
+                    return false;
             }
         }
 
+        
+        inline bool isStaticGateType(DFTElementType const& tp) {
+            if(!isGateType(tp)) return false;
+            switch(tp) {
+                case DFTElementType::AND:
+                case DFTElementType::OR:
+                case DFTElementType::VOT:
+                    return true;
+                case DFTElementType::POR:
+                case DFTElementType::SPARE:
+                case DFTElementType::PAND:
+                case DFTElementType::SEQAND:
+                    return false;
+                default:
+                    assert(false);
+                    return false;
+            }
+        }
+        
+        
     }
 }
 

src/storage/dft/DFTElements.h

@@ -118,10 +118,20 @@ namespace storm {
                 }
             }
 
+             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();
             }
@@ -194,7 +204,9 @@ namespace storm {
              */
             virtual void extendSubDft(std::set<size_t> elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const;
 
-
+            virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
+                return type() == other.type();
+            }
 
 
         protected:
@@ -368,7 +380,7 @@ namespace storm {
                 }
                 return false;
             }
-
+            
         };
         
        
@@ -442,6 +454,13 @@ namespace storm {
             bool isColdBasicElement() const override{
                 return storm::utility::isZero(mPassiveFailureRate);
             }
+            
+            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;
         };
 
@@ -483,6 +502,12 @@ namespace storm {
                 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);
+            }
+            
         };
 
 
@@ -547,6 +572,13 @@ namespace storm {
             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};
@@ -848,7 +880,12 @@ namespace storm {
             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>
@@ -916,7 +953,12 @@ namespace storm {
                 }
             }
         };
-
+        
+        template<typename ValueType>
+        bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
+            return e1.isTypeEqualTo(e2);
+        }
+        
     }
 }