From e322c568207240e1327963c7c42d03b0d232ee17 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 2 Mar 2016 15:30:00 +0100
Subject: [PATCH] findModularisationRewrite

Former-commit-id: ba948b7720f6742a8ebe2f101f17c422b30b24ab
---
 src/storage/dft/DFT.cpp | 35 +++++++++++++++++++++++++++++++++++
 src/storage/dft/DFT.h   |  2 ++
 src/storm-dyftee.cpp    |  8 ++++++++
 3 files changed, 45 insertions(+)

diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index bf68a095c..890e2de25 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -436,6 +436,41 @@ namespace storm {
             }
             return DFTIndependentSymmetries(res);
         }
+        
+        template<typename ValueType>
+        std::vector<size_t> DFT<ValueType>::findModularisationRewrite() const {
+           for(auto const& e : mElements) {
+               if(e->isGate() && (e->type() == DFTElementType::AND || e->type() == DFTElementType::OR) ) {
+                   // suitable parent gate! - Lets check the independent submodules of the children
+                   auto const& children = std::static_pointer_cast<DFTGate<ValueType>>(e)->children();
+                   for(auto const& child : children) {
+                       //std::cout << "check idea for: " << child->id() << std::endl;;
+                       auto ISD = std::static_pointer_cast<DFTGate<ValueType>>(child)->independentSubDft(true);
+                       // In the ISD, check for other children:
+                       //std::cout << "** subdft = ";
+                       for(auto const& isdelemid : ISD) {
+                           std::cout << isdelemid << " ";
+                       }
+                       std::cout << std::endl;
+                       
+                       std::vector<size_t> rewrite = {e->id(), child->id()};
+                       for(size_t isdElemId : ISD) {
+                           if(isdElemId == child->id()) continue;
+                           if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr<DFTElement<ValueType>> const& e) { return e->id() == isdElemId; } ) != children.end()) {
+                               //std::cout << "** found child in subdft: " <<  isdElemId << std::endl;
+                               rewrite.push_back(isdElemId);
+                           }
+                       }
+                       if(rewrite.size() > 2) {
+                           return rewrite;
+                       }
+                       
+                   }    
+               }
+           } 
+           return {};
+        }
+    
 
         template<typename ValueType>
         std::pair<std::vector<size_t>, std::vector<size_t>> DFT<ValueType>::getSortedParentAndOutDepIds(size_t index) const {
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 32e807197..75092e479 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -236,6 +236,8 @@ namespace storm {
             DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
 
             std::vector<size_t> immediateFailureCauses(size_t index) const;
+            
+            std::vector<size_t> findModularisationRewrite() const;
         private:
             std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
             
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 13b43f5ff..c5997ddd3 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -29,6 +29,14 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
     std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
     assert(formulas.size() == 1);
     std::cout << "Parsed formula." << std::endl;
+    auto modIdea = dft.findModularisationRewrite();
+    std::cout << "Modularisation idea: " << std::endl;
+    
+    for( auto const& i  : modIdea ) {
+        std::cout << i << ", ";
+    }
+    std::cout << std::endl;
+    
     std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
     storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
     if(symred) {