findModularisationRewrite

Former-commit-id: ba948b7720

src/storage/dft/DFT.cpp

@@ -437,6 +437,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 {
             std::pair<std::vector<size_t>, std::vector<size_t>> res;

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;
             

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) {