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

Former-commit-id: 3b469abd3a

src/storage/dft/DFT.cpp

@@ -1,5 +1,6 @@
 #include <boost/container/flat_set.hpp>
 
+#include <map>
 #include "DFT.h"
 #include "src/exceptions/NotSupportedException.h"
 
@@ -247,40 +248,87 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::vector<std::vector<size_t>> DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
+        DFTIndependentSymmetries DFT<ValueType>::findSymmetries(DFTColouring<ValueType> const& colouring) const {
             std::vector<size_t> vec;
             vec.reserve(nrElements());
-            storm::utility::iota_n(std::back_inserter(vec), 14, 0);
+            storm::utility::iota_n(std::back_inserter(vec), nrElements(), 0);
             BijectionCandidates<ValueType> completeCategories = colouring.colourSubdft(vec);
-            std::vector<std::vector<size_t>> res;
+            std::map<size_t, std::vector<std::vector<size_t>>> res;
+            
             for(auto const& colourClass : completeCategories.gateCandidates) {
                 if(colourClass.second.size() > 1) {
+                    std::set<size_t> foundEqClassFor;
                     for(auto it1 = colourClass.second.cbegin(); it1 != colourClass.second.cend(); ++it1) {
-                        std::vector<size_t> sortedParent1Ids = getGate(*it1)->parentIds();
-                        std::sort(sortedParent1Ids.begin(), sortedParent1Ids.end());
+                        std::vector<std::vector<size_t>> symClass;
+                        if(foundEqClassFor.count(*it1) > 0) {
+                            continue;
+                        }
+                        if(!getGate(*it1)->hasOnlyStaticParents()) {
+                            continue;
+                        }
+                        
+                        std::pair<std::vector<size_t>, std::vector<size_t>> influencedElem1Ids = getSortedParentAndOutDepIds(*it1);
                         auto it2 = it1;
                         for(++it2; it2 != colourClass.second.cend(); ++it2) {
+                            if(!getGate(*it2)->hasOnlyStaticParents()) {
+                                continue;
+                            }
                             std::vector<size_t> sortedParent2Ids = getGate(*it2)->parentIds();
                             std::sort(sortedParent2Ids.begin(), sortedParent2Ids.end());
-                            if(sortedParent1Ids == sortedParent2Ids) {
+                            
+                            if(influencedElem1Ids == getSortedParentAndOutDepIds(*it2)) {
                                 std::cout << "Considering ids " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
+                                bool isSymmetry = false;
                                 std::vector<size_t> isubdft1 = getGate(*it1)->independentSubDft();
                                 std::vector<size_t> isubdft2 = getGate(*it2)->independentSubDft();
-                                if(!isubdft1.empty() && !isubdft2.empty() && isubdft1.size() == isubdft2.size()) {
-                                    std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
-                                    auto LHS = colouring.colourSubdft(isubdft1);
-                                    auto RHS = colouring.colourSubdft(isubdft2);
-                                    auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
-                                    IsoCheck.findIsomorphism();
+                                if(isubdft1.empty() || isubdft2.empty() || isubdft1.size() != isubdft2.size()) {
+                                    continue;
+                                }
+                                std::cout << "Checking subdfts from " << *it1 << ", " << *it2 << " for isomorphism." << std::endl;
+                                auto LHS = colouring.colourSubdft(isubdft1);
+                                auto RHS = colouring.colourSubdft(isubdft2);
+                                auto IsoCheck = DFTIsomorphismCheck<ValueType>(LHS, RHS, *this);
+                                isSymmetry = IsoCheck.findIsomorphism();
+                                if(isSymmetry) {
+                                    std::cout << "subdfts are symmetric" << std::endl;
+                                    foundEqClassFor.insert(*it2);
+                                    if(symClass.empty()) {
+                                        for(auto const& i : isubdft1) {
+                                            symClass.push_back(std::vector<size_t>({i}));
+                                        }
+                                    }
+                                    auto symClassIt = symClass.begin();
+                                    for(auto const& i : isubdft1) {
+                                        symClassIt->emplace_back(IsoCheck.getIsomorphism().at(i));
+                                        ++symClassIt;
+                                        
+                                    }
+                                    
                                 }
                             }
                         }
+                        if(!symClass.empty()) {
+                            res.emplace(*it1, symClass);
+                        }
                     }
+                    
                 }
             }
-            return res;
+            return DFTIndependentSymmetries(res);
         }
 
+        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;
+            res.first = getElement(index)->parentIds();
+            std::sort(res.first.begin(), res.first.end());
+            for(auto const& dep : getElement(index)->outgoingDependencies()) {
+                res.second.push_back(dep->id());
+            }
+            std::sort(res.second.begin(), res.second.end());
+            return res;
+        }
+        
 
         // Explicitly instantiate the class.
         template class DFT<double>;

src/storage/dft/DFT.h

@@ -11,7 +11,7 @@
 
 #include "DFTElements.h"
 #include "../BitVector.h"
-
+#include "SymmetricUnits.h"
 #include "../../utility/math.h"
 #include "src/utility/macros.h"
 
@@ -262,9 +262,11 @@ namespace storm {
 
             DFTColouring<ValueType> colourDFT() const;
 
-            std::vector<std::vector<size_t>> findSymmetries(DFTColouring<ValueType> const& colouring) const;
+            DFTIndependentSymmetries findSymmetries(DFTColouring<ValueType> const& colouring) const;
 
         private:
+            std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
+            
             bool elementIndicesCorrect() const {
                 for(size_t i = 0; i < mElements.size(); ++i) {
                     if(mElements[i]->id() != i) return false;

src/storage/dft/DFTBuilder.cpp

@@ -123,7 +123,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L) {
+        void DFTBuilder<ValueType>::topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L) {
             if(visited[n] == topoSortColour::GREY) {
                 throw storm::exceptions::WrongFormatException("DFT is cyclic");
             } else if(visited[n] == topoSortColour::WHITE) {
@@ -141,7 +141,7 @@ namespace storm {
         // TODO Matthias: use typedefs
         template<typename ValueType>
         std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
-            std::map<DFTElementPointer, topoSortColour> visited;
+            std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
             for(auto const& e : mElements) {
                 visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); 
             }

src/storage/dft/DFTBuilder.h

@@ -141,7 +141,7 @@ namespace storm {
             
             enum class topoSortColour {WHITE, BLACK, GREY}; 
             
-            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour>& visited, DFTElementVector& L);
+            void topoVisit(DFTElementPointer const& n, std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>>& visited, DFTElementVector& L);
 
             DFTElementVector topoSort();
             

src/storage/dft/DFTElements.cpp

@@ -46,14 +46,15 @@ namespace storm {
 
         template<typename ValueType>
         std::vector<size_t> DFTElement<ValueType>::independentSubDft() const {
+            std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl;
             std::vector<size_t> res;
             res.push_back(this->id());
-            // Extend for pdeps.
             return res;
         }
 
         template<typename ValueType>
-        void DFTElement<ValueType>::extendSubDft(std::set<size_t> elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const {
+        void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const {
+            if(elemsInSubtree.count(this->id()) > 0) return;
             if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) {
                 // This is a parent of the suspected root, thus it is not a subdft.
                 elemsInSubtree.clear();
@@ -61,13 +62,19 @@ namespace storm {
             }
             elemsInSubtree.insert(mId);
             for(auto const& parent : mParents) {
-                if(elemsInSubtree.count(parent->id()) != 0) {
-                    parent->extendUnit(elemsInSubtree);
-                    if(elemsInSubtree.empty()) {
-                        return;
-                    }
+                
+                parent->extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                if(elemsInSubtree.empty()) {
+                    return;
                 }
             }
+            for(auto const& dep : mOutgoingDependencies) {
+                dep->extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                if(elemsInSubtree.empty()) {
+                    return;
+                }
+
+            }
         }
 
 

src/storage/dft/DFTElements.h

@@ -168,7 +168,7 @@ namespace storm {
                 return mOutgoingDependencies.size();
             }
             
-            DFTDependencyVector const& getOutgoingDependencies() const {
+            DFTDependencyVector const& outgoingDependencies() const {
                 return mOutgoingDependencies;
             }
             
@@ -202,7 +202,7 @@ namespace storm {
              * Helper to the independent subtree computation
              * @see independentSubDft
              */
-            virtual void extendSubDft(std::set<size_t> elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const;
+            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();
@@ -299,9 +299,10 @@ namespace storm {
                 return std::vector<size_t>(unit.begin(), unit.end());
             }
 
-            virtual void extendSubDft(std::set<size_t> elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const override {
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const override {
+                if(elemsInSubtree.count(this->id()) > 0) return;
                 DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot);
-                if(!elemsInSubtree.empty()) {
+                if(elemsInSubtree.empty()) {
                     // Parent in the subdft, ie it is *not* a subdft
                     return;
                 }
@@ -309,7 +310,7 @@ namespace storm {
                     child->extendSubDft(elemsInSubtree, parentsOfSubRoot);
                     if(elemsInSubtree.empty()) {
                         // Parent in the subdft, ie it is *not* a subdft
-                        break;
+                        return;
                     }
                 }
             }
@@ -437,7 +438,7 @@ namespace storm {
                 return mIngoingDependencies.size();
             }
             
-            DFTDependencyVector const& getIngoingDependencies() const {
+            DFTDependencyVector const& ingoingDependencies() const {
                 return mIngoingDependencies;
             }
         
@@ -455,6 +456,22 @@ namespace storm {
                 return storm::utility::isZero(mPassiveFailureRate);
             }
             
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const override {
+                 if(elemsInSubtree.count(this->id())) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                for(auto const& incDep : mIngoingDependencies) {
+                    incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                    if(elemsInSubtree.empty()) {
+                        // Parent in the subdft, ie it is *not* a subdft
+                        return;
+                    }
+                }
+            }
+            
             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);
@@ -502,6 +519,8 @@ 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);
@@ -589,6 +608,23 @@ namespace storm {
                 return std::vector<size_t>(unit.begin(), unit.end());
             }
 
+            virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const override {
+                 if(elemsInSubtree.count(this->id())) return;
+                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                if(elemsInSubtree.empty()) {
+                    // Parent in the subdft, ie it is *not* a subdft
+                    return;
+                }
+                mTriggerEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot);
+                
+                
+            }
+            
             virtual std::string toString() const override {
                 std::stringstream stream;
                 bool fdep = storm::utility::isOne(mProbability);

src/storage/dft/DFTIsomorphism.h

@@ -63,6 +63,87 @@ namespace storage {
         std::unordered_map<size_t, std::vector<size_t>> gateCandidates;
         std::unordered_map<BEColourClass<ValueType>, std::vector<size_t>> beCandidates;
         std::unordered_map<std::pair<ValueType, ValueType>, std::vector<size_t>> pdepCandidates;
+        
+        size_t nrGroups() const {
+            return gateCandidates.size() + beCandidates.size() + pdepCandidates.size();
+        }
+        
+        size_t size() const {
+            return nrGates() + nrBEs() + nrDeps();
+        }
+        
+        size_t nrGates() const {
+            size_t res = 0;
+            for(auto const& x : gateCandidates) {
+                res += x.second.size();
+            }
+            return res;
+        }
+        
+        size_t nrBEs() const {
+            size_t res = 0;
+            for(auto const& x : beCandidates) {
+                res += x.second.size();
+            }
+            return res;
+        }
+        
+        size_t nrDeps() const {
+            size_t res = 0;
+            for(auto const& x : pdepCandidates) {
+                res += x.second.size();
+            }
+            return res;
+        }
+        
+        bool hasGate(size_t index) const {
+            for(auto const& x : gateCandidates) {
+                for( auto const& ind : x.second) {
+                    if(index == ind) return true;
+                }
+            }
+            return false;
+        }
+        
+        bool hasBE(size_t index) const {
+            for(auto const& x : beCandidates) {
+                for(auto const& ind : x.second) {
+                    if(index == ind) return true;
+                }
+            }
+            return false;
+        }
+        
+        bool hasDep(size_t index) const {
+            for(auto const& x : pdepCandidates) {
+                for(auto const& ind : x.second) {
+                    if(index == ind) return true;
+                }
+            }
+            return false;
+        }
+        
+        bool has(size_t index) const {
+            return hasGate(index) || hasBE(index) || hasDep(index);
+        }
+        
+        
+        
+        size_t trivialGateGroups() const {
+            size_t res = 0;
+            for(auto const& x : gateCandidates) {
+                if(x.second.size() == 1) ++res;
+            }
+            return res;
+        }
+        
+        size_t trivialBEGroups() const {
+            size_t res = 0;
+            for(auto const& x : beCandidates) {
+                if(x.second.size() == 1) ++res;
+            }
+            return res;
+        }
     };
 
     template<typename ValueType>
@@ -175,8 +256,8 @@ namespace storage {
          * Can only be called after the findIsomorphism procedure returned that an isomorphism has found.
          * @see findIsomorphism
          */
-        std::vector<std::pair<size_t, size_t>> getIsomorphism() const {
-
+        std::map<size_t, size_t> const& getIsomorphism() const {
+            return bijection;
         }
 
         /**
@@ -207,6 +288,9 @@ namespace storage {
             initializePermutationsAndTreatTrivialGroups(bleft.beCandidates, bright.beCandidates, currentPermutations.beCandidates);
             initializePermutationsAndTreatTrivialGroups(bleft.gateCandidates, bright.gateCandidates, currentPermutations.gateCandidates);
             initializePermutationsAndTreatTrivialGroups(bleft.pdepCandidates, bright.pdepCandidates, currentPermutations.pdepCandidates);
+            std::cout << bijection.size() << " vs. " << bleft.size() << " vs. " << bright.size() << std::endl;
+            assert(bijection.size() == bleft.size());
+            
         }
 
         /**
@@ -214,6 +298,7 @@ namespace storage {
          * @return true if a next bijection exists.
          */
         bool findNextBijection() {
+            assert(candidatesCompatible);
             bool foundNext = false;
             if(!currentPermutations.beCandidates.empty()) {
                 auto it = currentPermutations.beCandidates.begin();
@@ -260,12 +345,46 @@ namespace storage {
          *
          */
         bool check() {
+            assert(bijection.size() == bleft.size());
             // We can skip BEs, as they are identified by they're homomorphic if they are in the same class
-            for(auto const& index : bijection) {
-                // As they are in the same group, the types are fine already. We just have to check the children.
-
+            for(auto const& indexpair : bijection) {
+                // Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds)
+                equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second));
+                if(dft.isGate(indexpair.first)) {
+                    assert(dft.isGate(indexpair.second));
+                    auto const& lGate = dft.getGate(indexpair.first);
+                    std::set<size_t> childrenLeftMapped;
+                    for(auto const& child : lGate->children() ) {
+                        assert(bleft.has(child->id()));
+                        childrenLeftMapped.insert(bijection.at(child->id()));
+                    }
+                    auto const& rGate = dft.getGate(indexpair.second);
+                    std::set<size_t> childrenRight;
+                    for(auto const& child : rGate->children() ) {
+                        assert(bright.has(child->id()));
+                        childrenRight.insert(child->id());
+                    }
+                    if(childrenLeftMapped != childrenRight) {
+                        return false;
+                    }
+                } else if(dft.isDependency(indexpair.first)) {
+                    assert(dft.isDependency(indexpair.second));
+                    auto const& lDep = dft.getDependency(indexpair.first);
+                    auto const& rDep = dft.getDependency(indexpair.second);
+                    if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) {
+                        return false;
+                    } 
+                    if(bijection.at(lDep->dependentEvent()->id()) != rDep->dependentEvent()->id()) {
+                        return false;
+                    }
+                }
+                else {
+                    assert(dft.isBasicElement(indexpair.first));
+                    assert(dft.isBasicElement(indexpair.second));
+                    // No operations required.
+                }
             }
-            return false;
+            return true;
         }
 
     private:
@@ -318,7 +437,7 @@ namespace storage {
                     auto it = permutations.insert(colour);
                     assert(it.second);
                     std::sort(it.first->second.begin(), it.first->second.end());
-                    zipVectorsIntoMap(colour.second, permutations.find(colour.first)->second, bijection);
+                    zipVectorsIntoMap(left.at(colour.first), it.first->second, bijection);
                 } else {
                     assert(colour.second.size() == 1);
                     assert(bijection.count(left.at(colour.first).front()) == 0);
@@ -341,9 +460,7 @@ namespace storage {
         }
 
 
-        //std::vector<std::pair<size_t, size_t>> computeNextCandidate(){
-
-        //}
+        
     };
 
 

src/storage/dft/SymmetricUnits.h

@@ -1,7 +1,28 @@
-#ifndef SYMMETRICUNITS_H
-#define	SYMMETRICUNITS_H
-
-
-
-#endif	/* SYMMETRICUNITS_H */
+#pragma once
 
+namespace storm {
+    namespace storage {
+        struct DFTIndependentSymmetries {
+            std::map<size_t, std::vector<std::vector<size_t>>> groups;
+            
+            DFTIndependentSymmetries(std::map<size_t, std::vector<std::vector<size_t>>> groups) : groups(groups) {
+                
+            }
+        };
+        
+        inline std::ostream& operator<<(std::ostream& os, DFTIndependentSymmetries const& s)  {
+            for(auto const& cl : s.groups) {
+                std::cout << "SYM GROUP FOR " << cl.first << std::endl;
+                for(auto const& eqClass : cl.second) {
+                    for(auto const& i : eqClass) {
+                        std::cout << i << " ";
+                    }
+                    std::cout << std::endl;
+                }
+            }
+            
+            
+            return os;
+        }
+    }
+}

src/storm-dyftee.cpp

@@ -4,6 +4,7 @@
 #include "builder/ExplicitDFTModelBuilder.h"
 #include "modelchecker/results/CheckResult.h"
 #include "utility/storm.h"
+#include "storage/dft/DFTIsomorphism.h"
 
 /*!
  * Load DFT from filename, build corresponding Model and check against given property.
@@ -12,13 +13,20 @@
  * @param property PCTC formula capturing the property to check.
  */
 template <typename ValueType>
-void analyzeDFT(std::string filename, std::string property) {
+void analyzeDFT(std::string filename, std::string property, bool symred = false) {
     // Parsing DFT
     std::cout << "Parsing DFT file..." << std::endl;
     storm::parser::DFTGalileoParser<ValueType> parser;
     storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
     std::cout << "Built data structure" << std::endl;
-
+    
+    if(symred) {
+        std::cout << dft.getElementsString() << std::endl;
+        auto colouring = dft.colourDFT();
+        auto res = dft.findSymmetries(colouring);
+        std::cout << res;
+    }
+        
     // Building Markov Automaton
     std::cout << "Building Model..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft);
@@ -52,6 +60,7 @@ int main(int argc, char** argv) {
 
     // Parse cli arguments
     bool parametric = false;
+    bool symred = false;
     log4cplus::LogLevel level = log4cplus::WARN_LOG_LEVEL;
     std::string filename = argv[1];
     std::string pctlFormula = "";
@@ -74,6 +83,8 @@ int main(int argc, char** argv) {
             ++i;
             assert(i < argc);
             pctlFormula = argv[i];
+        } else if (option == "--symred") {
+            symred = true;
         } else {
             std::cout << "Option '" << option << "' not recognized." << std::endl;
             return 1;
@@ -88,8 +99,8 @@ int main(int argc, char** argv) {
     std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl;
 
     if (parametric) {
-        analyzeDFT<storm::RationalFunction>(filename, pctlFormula);
+        analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred);
     } else {
-        analyzeDFT<double>(filename, pctlFormula);
+        analyzeDFT<double>(filename, pctlFormula, symred);
     }
 }