DftModularizationChecker.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <vector>
 
#include "storm-dft/modelchecker/DFTModelChecker.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/DftModule.h"
#include "storm-dft/storage/SylvanBddManager.h"
#include "storm/logic/Formula.h"
 
namespace storm::dft {
namespace modelchecker {
 
template<typename ValueType>
class DftModularizationChecker {
   public:
    using DFTElementCPointer = std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const>;
    using FormulaVector = typename DFTModelChecker<ValueType>::property_vector;
 
    DftModularizationChecker(std::shared_ptr<storm::dft::storage::DFT<ValueType>> dft);
 
    std::vector<ValueType> check(FormulaVector const &formulas, size_t chunksize = 0);
 
    std::vector<ValueType> getProbabilitiesAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize = 0);
 
    ValueType getProbabilityAtTimebound(ValueType const timebound) {
        // workDFT will be set in getProbabilitiesAtTimepoints()
        return getProbabilitiesAtTimepoints({timebound}).at(0);
    }
 
   private:
    void populateDynamicModules(storm::dft::storage::DftIndependentModule const &module);
 
    std::shared_ptr<storm::dft::storage::DFT<ValueType>> replaceDynamicModules(std::vector<ValueType> const &timepoints);
 
    typename storm::dft::modelchecker::DFTModelChecker<ValueType>::dft_results analyseDynamicModule(storm::dft::storage::DftIndependentModule const &module,
                                                                                                    std::vector<ValueType> const &timepoints);
 
    // DFT.
    std::shared_ptr<storm::dft::storage::DFT<ValueType>> dft;
    // DFT modelchecker
    storm::dft::modelchecker::DFTModelChecker<ValueType> modelchecker;
    // don't reinitialize Sylvan BDD
    // temporary
    std::shared_ptr<storm::dft::storage::SylvanBddManager> sylvanBddManager;
    // Independent modules with their top element
    std::vector<storm::dft::storage::DftIndependentModule> dynamicModules;
};
 
}  // namespace modelchecker
}  // namespace storm::dft