DftModularizationChecker.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <vector>
 
#include "storm-dft/environment/DftEnvironment.h"
#include "storm-dft/modelchecker/DFTModelChecker.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/DftModule.h"
#include "storm-dft/storage/SylvanBddManager.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(storm::dft::DftEnvironment const &env, 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;
    // Environment used for analysing the dynamic modules.
    storm::dft::DftEnvironment env;
    // 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