Further work on state space generation

Former-commit-id: bb373138e5

src/storage/dft/DFT.cpp

@@ -37,7 +37,6 @@ namespace storm {
                     mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
                     stateIndex += mUsageInfoBits;
 
-
                 }
             }
 
@@ -68,6 +67,8 @@ namespace storm {
                 os << std::endl;
             }
         }
+        
+        
 
         void DFT::printInfo(std::ostream& os) const {
             os << "Top level index: " << mTopLevelIndex << std::endl << "Nr BEs" << mNrOfBEs << std::endl;

src/storage/dft/DFTElements.cpp

@@ -26,6 +26,19 @@ namespace storm {
             }
         }
         
+        void DFTElement::extendUnit(std::set<size_t>& unit) const {
+            unit.insert(mId);
+            for(auto const& parent : mParents) {
+                if(unit.count(parent->id()) != 0) {
+                    parent->extendUnit(unit);
+                }
+            }
+        }
+        
+        void DFTElement::checkForSymmetricChildren() const {
+            
+        }
+        
         template<>
         bool DFTBE<double>::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
             if(DFTElement::checkDontCareAnymore(state, queues)) {
@@ -34,5 +47,6 @@ namespace storm {
             }
             return false;
         }
+        
     }
 }

src/storage/dft/DFTElements.h

@@ -99,6 +99,10 @@ namespace storm {
             virtual void print(std::ostream& = std::cout) const = 0;
             
             virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
+            
+            virtual std::vector<size_t> independentUnit() const = 0;
+        
+            virtual void  extendUnit(std::set<size_t>& unit) const;
         };
 
 
@@ -166,6 +170,21 @@ namespace storm {
                 }
             }
             
+            virtual std::vector<size_t> independentUnit() const {
+                std::set<size_t> unit = {mId};
+                for(auto const& child : mChildren) {
+                    child->extendUnit(unit);
+                }
+                for(auto const& parent : mParents) {
+                    if(unit.count(parent->id()) != 0) {
+                        return {};
+                    } 
+                }
+                return std::vector<size_t>(unit.begin(), unit.end()); 
+           }
+
+            
+            
             virtual void print(std::ostream& os = std::cout) const {
                 os << "{" << name() << "} " << typestring() << "( ";
                 std::vector<std::shared_ptr<DFTElement>>::const_iterator it = mChildren.begin();
@@ -185,7 +204,16 @@ namespace storm {
                 }
                 return false;
             }
+            
+            virtual void extendUnit(std::set<size_t>& unit) const {
+                DFTElement::extendUnit(unit);
+                for(auto const& child : mChildren) {
+                    child->extendUnit(unit);
+                }
+            }
+            
         protected:
+            
             void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
                 for(std::shared_ptr<DFTGate> parent : mParents) {
                     if(state.isOperational(parent->id())) {
@@ -269,7 +297,9 @@ namespace storm {
                 return mPassiveFailureRate == 0;
             }
             
-
+            virtual std::vector<size_t> independentUnit() const {
+                return {mId};
+            }
             virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
         };
         

src/storage/dft/DFTUnit.h

@@ -0,0 +1,22 @@
+#ifndef DFTUNIT_H
+#define	DFTUNIT_H
+
+namespace storm {
+    namespace storage {
+        class DFT;
+        
+        class DFTUnit {
+        private:
+            DFT const& mDft;
+            BitVector mMembers;
+            
+            
+        public:
+            DFTUnit(DFT const& dft, BitVector const& members);
+        };
+    }
+}
+
+
+#endif	/* DFTUNIT_H */
+

src/storage/dft/SymmetricUnits.h

@@ -0,0 +1,7 @@
+#ifndef SYMMETRICUNITS_H
+#define	SYMMETRICUNITS_H
+
+
+
+#endif	/* SYMMETRICUNITS_H */
+