DftModularizer.h

Go to the documentation of this file.

#pragma once
 
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/DftModule.h"
 
namespace storm::dft {
namespace utility {
 
template<typename ValueType>
class DftModularizer {
   public:
    using DFTElementCPointer = std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const>;
    using ElementId = size_t;
 
    DftModularizer() = default;
 
    storm::dft::storage::DftIndependentModule computeModules(storm::dft::storage::DFT<ValueType> const& dft);
 
   private:
    void populateDfsCounters(DFTElementCPointer const element);
 
    void obtainModules(DFTElementCPointer const element);
 
    static std::vector<DFTElementCPointer> getChildren(DFTElementCPointer const element);
 
    static std::vector<DFTElementCPointer> getAffectingElements(DFTElementCPointer const element);
 
    static bool containsElement(std::vector<DFTElementCPointer> const& list, DFTElementCPointer const element);
 
    struct DfsCounter {
        uint64_t firstVisit{0};
        uint64_t secondVisit{0};
        uint64_t lastVisit{0};
 
        uint64_t minFirstVisit{0};
        uint64_t maxLastVisit{0};
    };
    struct ModularizationInfo {
        bool isModule = false;
        std::set<ElementId> elements;
        std::set<storm::dft::storage::DftIndependentModule> submodules;
        bool isStatic = true;
        bool fullyStatic = true;
    };
 
    std::map<ElementId, DfsCounter> dfsCounters{};
    std::map<ElementId, ModularizationInfo> modInfos{};
    uint64_t lastDate{};
};
 
}  // namespace utility
}  // namespace storm::dft