From 59fe9ace09ab2c7a607b6aceac7a11dc64aa2bab Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 17 Jul 2015 14:06:15 +0200
Subject: [PATCH] Further work on state space generation

Former-commit-id: bb373138e5982beaa6188ddd21d76751c7a71f19
---
 src/storage/dft/DFT.cpp          |  3 ++-
 src/storage/dft/DFTElements.cpp  | 14 ++++++++++++++
 src/storage/dft/DFTElements.h    | 32 +++++++++++++++++++++++++++++++-
 src/storage/dft/DFTUnit.h        | 22 ++++++++++++++++++++++
 src/storage/dft/SymmetricUnits.h |  7 +++++++
 5 files changed, 76 insertions(+), 2 deletions(-)
 create mode 100644 src/storage/dft/DFTUnit.h
 create mode 100644 src/storage/dft/SymmetricUnits.h

diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index e06661988..551c7ad2a 100644
--- a/src/storage/dft/DFT.cpp
+++ b/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;
diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp
index b96ceafb4..699fe47e5 100644
--- a/src/storage/dft/DFTElements.cpp
+++ b/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;
         }
+        
     }
 }
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 9d3338022..12da6a4bf 100644
--- a/src/storage/dft/DFTElements.h
+++ b/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;
         };
         
diff --git a/src/storage/dft/DFTUnit.h b/src/storage/dft/DFTUnit.h
new file mode 100644
index 000000000..18319b70c
--- /dev/null
+++ b/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 */
+
diff --git a/src/storage/dft/SymmetricUnits.h b/src/storage/dft/SymmetricUnits.h
new file mode 100644
index 000000000..3959593a1
--- /dev/null
+++ b/src/storage/dft/SymmetricUnits.h
@@ -0,0 +1,7 @@
+#ifndef SYMMETRICUNITS_H
+#define	SYMMETRICUNITS_H
+
+
+
+#endif	/* SYMMETRICUNITS_H */
+