SFTBDDChecker.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <memory>
#include <set>
#include <unordered_map>
#include <utility>
#include <vector>
 
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/SylvanBddManager.h"
#include "storm-dft/transformations/SftToBddTransformator.h"
#include "storm/environment/Environment.h"
 
namespace storm::dft {
namespace modelchecker {

class SFTBDDChecker {
   public:
    using ValueType = double;
#ifdef STORM_HAVE_SYLVAN
    using Bdd = sylvan::Bdd;
#endif
 
    SFTBDDChecker(std::shared_ptr<storm::dft::storage::DFT<ValueType>> dft, std::shared_ptr<storm::dft::storage::SylvanBddManager> sylvanBddManager);
 
    SFTBDDChecker(std::shared_ptr<storm::dft::transformations::SftToBddTransformator<ValueType>> transformator);

    std::shared_ptr<storm::dft::storage::DFT<ValueType>> getDFT() const;

    std::shared_ptr<storm::dft::storage::SylvanBddManager> getSylvanBddManager() const;

    std::shared_ptr<storm::dft::transformations::SftToBddTransformator<ValueType>> getTransformator() const;

    void exportBddToDot(std::string const &filename) {
#ifdef STORM_HAVE_SYLVAN
        getSylvanBddManager()->exportBddToDot(getTopLevelElementBdd(), filename);
#else
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
#endif
    }

    std::vector<std::vector<std::string>> getMinimalCutSets();

    std::vector<std::vector<uint32_t>> getMinimalCutSetsAsIndices();

    ValueType getProbabilityAtTimebound(ValueType timebound) {
#ifdef STORM_HAVE_SYLVAN
        return getProbabilityAtTimebound(getTopLevelElementBdd(), timebound);
#else
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
#endif
    }
 
#ifdef STORM_HAVE_SYLVAN
    ValueType getProbabilityAtTimebound(Bdd bdd, ValueType timebound) const;
#endif

    std::vector<ValueType> getProbabilitiesAtTimepoints(std::vector<ValueType> const &timepoints, size_t const chunksize = 0) {
#ifdef STORM_HAVE_SYLVAN
        return getProbabilitiesAtTimepoints(getTopLevelElementBdd(), timepoints, chunksize);
#else
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
#endif
    }
 
#ifdef STORM_HAVE_SYLVAN
    std::vector<ValueType> getProbabilitiesAtTimepoints(Bdd bdd, std::vector<ValueType> const &timepoints, size_t chunksize = 0) const;
#endif

    ValueType getBirnbaumFactorAtTimebound(std::string const &beName, ValueType timebound);

    std::vector<ValueType> getAllBirnbaumFactorsAtTimebound(ValueType timebound);

    std::vector<ValueType> getBirnbaumFactorsAtTimepoints(std::string const &beName, std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    std::vector<std::vector<ValueType>> getAllBirnbaumFactorsAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    ValueType getCIFAtTimebound(std::string const &beName, ValueType timebound);

    std::vector<ValueType> getAllCIFsAtTimebound(ValueType timebound);

    std::vector<ValueType> getCIFsAtTimepoints(std::string const &beName, std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    std::vector<std::vector<ValueType>> getAllCIFsAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    ValueType getDIFAtTimebound(std::string const &beName, ValueType timebound);

    std::vector<ValueType> getAllDIFsAtTimebound(ValueType timebound);

    std::vector<ValueType> getDIFsAtTimepoints(std::string const &beName, std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    std::vector<std::vector<ValueType>> getAllDIFsAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    ValueType getRAWAtTimebound(std::string const &beName, ValueType timebound);

    std::vector<ValueType> getAllRAWsAtTimebound(ValueType timebound);

    std::vector<ValueType> getRAWsAtTimepoints(std::string const &beName, std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    std::vector<std::vector<ValueType>> getAllRAWsAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    ValueType getRRWAtTimebound(std::string const &beName, ValueType timebound);

    std::vector<ValueType> getAllRRWsAtTimebound(ValueType timebound);

    std::vector<ValueType> getRRWsAtTimepoints(std::string const &beName, std::vector<ValueType> const &timepoints, size_t chunksize = 0);

    std::vector<std::vector<ValueType>> getAllRRWsAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize = 0);
 
   private:
#ifdef STORM_HAVE_SYLVAN
    void recursiveMCS(Bdd const bdd, std::vector<uint32_t> &buffer, std::vector<std::vector<uint32_t>> &minimalCutSets) const;
 
    template<typename FuncType>
    void chunkCalculationTemplate(std::vector<ValueType> const &timepoints, size_t chunksize, FuncType func) const;
 
    template<typename FuncType>
    ValueType getImportanceMeasureAtTimebound(std::string const &beName, ValueType timebound, FuncType func);
 
    template<typename FuncType>
    std::vector<ValueType> getAllImportanceMeasuresAtTimebound(ValueType timebound, FuncType func);
 
    template<typename FuncType>
    std::vector<ValueType> getImportanceMeasuresAtTimepoints(std::string const &beName, std::vector<ValueType> const &timepoints, size_t chunksize,
                                                             FuncType func);
 
    template<typename FuncType>
    std::vector<std::vector<ValueType>> getAllImportanceMeasuresAtTimepoints(std::vector<ValueType> const &timepoints, size_t chunksize, FuncType func);

    Bdd getTopLevelElementBdd();
 
    std::shared_ptr<storm::dft::transformations::SftToBddTransformator<ValueType>> transformator;
#endif
};
 
}  // namespace modelchecker
}  // namespace storm::dft