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

Former-commit-id: 4a7cdbbf5d

src/storage/dft/DFT.cpp

@@ -2,6 +2,7 @@
 
 #include <map>
 #include "DFT.h"
+#include "DFTBuilder.h"
 #include "src/exceptions/NotSupportedException.h"
 
 #include "DFTIsomorphism.h"
@@ -229,6 +230,95 @@ namespace storm {
             return stateIndex;
         }
         
+        template<typename ValueType>
+        DFT<ValueType> DFT<ValueType>::optimize() const {
+            std::vector<size_t> modIdea = findModularisationRewrite();
+            std::cout << "Modularisation idea: " << std::endl;
+    
+            for( auto const& i  : modIdea ) {
+                std::cout << i << ", ";
+            }
+
+            if (modIdea.empty()) {
+                // No rewrite needed
+                return *this;
+            }
+            
+            std::vector<std::vector<size_t>> rewriteIds;
+            rewriteIds.push_back(modIdea);
+            
+            DFTBuilder<ValueType> builder;
+            
+            // Accumulate elements which must be rewritten
+            std::set<size_t> rewriteSet;
+            for (std::vector<size_t> rewrites : rewriteIds) {
+                rewriteSet.insert(rewrites.front());
+            }
+            // Copy all other elements which do not change
+            for (auto elem : mElements) {
+                if (rewriteSet.count(elem->id()) == 0) {
+                    builder.copyElement(elem);
+                }
+            }
+            
+            // Add rewritten elements
+            for (std::vector<size_t> rewrites : rewriteIds) {
+                assert(rewrites.size() > 1);
+                assert(mElements[rewrites[1]]->hasParents());
+                assert(mElements[rewrites[1]]->parents().front()->isGate());
+                DFTGatePointer originalParent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front());
+                std::string newParentName = builder.getUniqueName(originalParent->name());
+                
+                // Accumulate children names
+                std::vector<std::string> childrenNames;
+                for (size_t i = 1; i < rewrites.size(); ++i) {
+                    assert(mElements[rewrites[i]]->parents().front()->id() == originalParent->id()); // Children have the same father
+                    childrenNames.push_back(mElements[rewrites[i]]->name());
+                }
+                
+                // Add element inbetween parent and children
+                switch (originalParent->type()) {
+                    case DFTElementType::AND:
+                        builder.addAndElement(newParentName, childrenNames);
+                        break;
+                    case DFTElementType::OR:
+                        builder.addOrElement(newParentName, childrenNames);
+                        break;
+                    case DFTElementType::BE:
+                    case DFTElementType::CONSTF:
+                    case DFTElementType::CONSTS:
+                    case DFTElementType::VOT:
+                    case DFTElementType::PAND:
+                    case DFTElementType::SPARE:
+                    case DFTElementType::POR:
+                    case DFTElementType::PDEP:
+                    case DFTElementType::SEQ:
+                    case DFTElementType::MUTEX:
+                        // Other elements are not supported
+                        assert(false);
+                        break;
+                    default:
+                        assert(false);
+                }
+                
+                // Add parent with the new child newParent and all its remaining children
+                childrenNames.clear();
+                childrenNames.push_back(newParentName);
+                for (auto const& child : originalParent->children()) {
+                    if (std::find(rewrites.begin()+1, rewrites.end(), child->id()) == rewrites.end()) {
+                        // Child was not rewritten and must be kept
+                        childrenNames.push_back(child->name());
+                    }
+                }
+                builder.copyGate(originalParent, childrenNames);
+            }
+            
+            builder.setTopLevel(mElements[mTopLevelIndex]->name());
+            // TODO use reference?
+            DFT<ValueType> newDft = builder.build();
+            return newDft.optimize();
+        }
+        
         template<typename ValueType>
         std::string DFT<ValueType>::getElementsString() const {
             std::stringstream stream;
@@ -484,7 +574,6 @@ namespace storm {
             return res;
         }
         
-
         // Explicitly instantiate the class.
         template class DFT<double>;
 

src/storage/dft/DFT.h

@@ -35,6 +35,8 @@ namespace storm {
         // Forward declarations
         template<typename T> class DFTColouring;
         
+        template<typename T> class DFTBuilder;
+
         
         
 
@@ -73,6 +75,10 @@ namespace storm {
 
             size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, storm::storage::BitVector& visited, size_t stateIndex) const;
         
+            DFT<ValueType> optimize() const;
+            
+            void copyElements(std::vector<size_t> elements, DFTBuilder<ValueType> builder) const;
+            
             size_t stateVectorSize() const {
                 return mStateVectorSize;
             }
@@ -238,6 +244,7 @@ namespace storm {
             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/storage/dft/DFTBuilder.cpp

@@ -70,7 +70,8 @@ namespace storm {
             for(DFTElementPointer e : elems) {
                 e->setId(id++);
             }
-            return DFT<ValueType>(elems, mElements[topLevelIdentifier]);
+            assert(!mTopLevelIdentifier.empty());
+            return DFT<ValueType>(elems, mElements[mTopLevelIdentifier]);
         }
 
         template<typename ValueType>
@@ -180,7 +181,6 @@ namespace storm {
             }
         }
 
-        // TODO Matthias: use typedefs
         template<typename ValueType>
         std::vector<std::shared_ptr<DFTElement<ValueType>>> DFTBuilder<ValueType>::topoSort() {
             std::map<DFTElementPointer, topoSortColour, OrderElementsById<ValueType>> visited;
@@ -196,6 +196,87 @@ namespace storm {
             return L;
         }
         
+        template<typename ValueType>
+        std::string DFTBuilder<ValueType>::getUniqueName(std::string name) {
+            return name + "_" + std::to_string(++mUniqueOffset);
+        }
+        
+        template<typename ValueType>
+        void DFTBuilder<ValueType>::copyElement(DFTElementPointer element) {
+            std::vector<std::string> children;
+            switch (element->type()) {
+                case DFTElementType::AND:
+                case DFTElementType::OR:
+                case DFTElementType::PAND:
+                case DFTElementType::POR:
+                case DFTElementType::SPARE:
+                case DFTElementType::VOT:
+                {
+                    for (DFTElementPointer const& elem : std::static_pointer_cast<DFTGate<ValueType>>(element)->children()) {
+                        children.push_back(elem->name());
+                    }
+                    copyGate(std::static_pointer_cast<DFTGate<ValueType>>(element), children);
+                    break;
+                }
+                case DFTElementType::BE:
+                {
+                    std::shared_ptr<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(element);
+                    ValueType dormancyFactor = storm::utility::zero<ValueType>();
+                    if (!storm::utility::isZero(be->passiveFailureRate())) {
+                        dormancyFactor = be->activeFailureRate() / be->passiveFailureRate();
+                    }
+                    addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor);
+                    break;
+                }
+                case DFTElementType::CONSTF:
+                case DFTElementType::CONSTS:
+                    // TODO
+                    assert(false);
+                    break;
+                case DFTElementType::PDEP:
+                {
+                    DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
+                    children.push_back(dependency->triggerEvent()->name());
+                    children.push_back(dependency->dependentEvent()->name());
+                    addDepElement(element->name(), children, dependency->probability());
+                    break;
+                }
+                case DFTElementType::SEQ:
+                case DFTElementType::MUTEX:
+                {
+                    for (DFTElementPointer const& elem : std::static_pointer_cast<DFTRestriction<ValueType>>(element)->children()) {
+                        children.push_back(elem->name());
+                    }
+                    addRestriction(element->name(), children, element->type());
+                    break;
+                }
+                default:
+                    assert(false);
+                    break;
+            }
+        }
+
+        template<typename ValueType>
+        void DFTBuilder<ValueType>::copyGate(DFTGatePointer gate, std::vector<std::string> const& children) {
+            switch (gate->type()) {
+                case DFTElementType::AND:
+                case DFTElementType::OR:
+                case DFTElementType::PAND:
+                case DFTElementType::POR:
+                case DFTElementType::SPARE:
+                    addStandardGate(gate->name(), children, gate->type());
+                    break;
+                case DFTElementType::VOT:
+                    addVotElement(gate->name(), std::static_pointer_cast<DFTVot<ValueType>>(gate)->threshold(), children);
+                    break;
+                default:
+                    assert(false);
+                    break;
+            }
+        }
+
+
+
         // Explicitly instantiate the class.
         template class DFTBuilder<double>;
 

src/storage/dft/DFTBuilder.h

@@ -26,7 +26,8 @@ namespace storm {
 
         private:
             std::size_t mNextId = 0;
-            std::string topLevelIdentifier;
+            std::size_t mUniqueOffset = 0;
+            std::string mTopLevelIdentifier;
             std::unordered_map<std::string, DFTElementPointer> mElements;
             std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
             std::unordered_map<DFTRestrictionPointer, std::vector<std::string>> mRestrictionChildNames;
@@ -140,18 +141,36 @@ namespace storm {
             }
             
             bool setTopLevel(std::string const& tle) {
-                topLevelIdentifier = tle;
+                mTopLevelIdentifier = tle;
                 return mElements.count(tle) > 0;
             }
             
+            std::string getUniqueName(std::string name);
+            
             DFT<ValueType> build();
             
+            /**
+             * Copy element and insert it again in the builder.
+             *
+             * @param element Element to copy.
+             */
+            void copyElement(DFTElementPointer element);
+
+            /**
+             * Copy gate with given children and insert it again in the builder. The current children of the element
+             * are discarded.
+             *
+             * @param gate Gate to copy.
+             * @param children New children of copied element.
+             */
+            void copyGate(DFTGatePointer gate, std::vector<std::string> const& children);
 
         private:
             
             unsigned computeRank(DFTElementPointer const& elem);
             
             bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
+
             bool addRestriction(std::string const& name, std::vector<std::string> const& children, DFTElementType tp);
 
             enum class topoSortColour {WHITE, BLACK, GREY}; 

src/storage/dft/elements/DFTVot.h

@@ -52,6 +52,10 @@ namespace storm {
                 }
             }
             
+            unsigned threshold() const {
+                return mThreshold;
+            }
+
             virtual DFTElementType type() const override {
                 return DFTElementType::VOT;
             }

src/storm-dyftee.cpp

@@ -29,13 +29,8 @@ 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;
+    dft = dft.optimize();
     
     std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
     storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);