storm-dft.h

Go to the documentation of this file.

#pragma once
 
#include <type_traits>
#include <utility>
#include <vector>
 
#include "storm-dft/modelchecker/DFTASFChecker.h"
#include "storm-dft/modelchecker/DFTModelChecker.h"
#include "storm-dft/parser/DFTGalileoParser.h"
#include "storm-dft/parser/DFTJsonParser.h"
#include "storm-dft/transformations/DftToGspnTransformator.h"
#include "storm-dft/transformations/DftTransformer.h"
#include "storm-dft/utility/DftValidator.h"
#include "storm-dft/utility/FDEPConflictFinder.h"
#include "storm-dft/utility/FailureBoundFinder.h"
#include "storm-dft/utility/RelevantEvents.h"
 
#include "storm-gspn/api/storm-gspn.h"
 
namespace storm::dft {
namespace api {
 
template<typename ValueType>
std::shared_ptr<storm::dft::storage::DFT<ValueType>> loadDFTGalileoFile(std::string const& file) {
    return std::make_shared<storm::dft::storage::DFT<ValueType>>(storm::dft::parser::DFTGalileoParser<ValueType>::parseDFT(file));
}
 
template<typename ValueType>
std::shared_ptr<storm::dft::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) {
    return std::make_shared<storm::dft::storage::DFT<ValueType>>(storm::dft::parser::DFTJsonParser<ValueType>::parseJsonFromString(jsonString));
}
 
template<typename ValueType>
std::shared_ptr<storm::dft::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) {
    return std::make_shared<storm::dft::storage::DFT<ValueType>>(storm::dft::parser::DFTJsonParser<ValueType>::parseJsonFromFile(file));
}
 
template<typename ValueType>
std::pair<bool, std::string> isWellFormed(storm::dft::storage::DFT<ValueType> const& dft, bool validForMarkovianAnalysis = true) {
    std::stringstream stream;
    bool wellFormed = false;
    if (validForMarkovianAnalysis) {
        wellFormed = storm::dft::utility::DftValidator<ValueType>::isDftValidForMarkovianAnalysis(dft, stream);
    } else {
        wellFormed = storm::dft::utility::DftValidator<ValueType>::isDftWellFormed(dft, stream);
    }
    return std::pair<bool, std::string>(wellFormed, stream.str());
}
 
template<typename ValueType>
std::shared_ptr<storm::dft::storage::DFT<ValueType>> applyTransformations(storm::dft::storage::DFT<ValueType> const& dft, bool uniqueBE, bool binaryFDEP,
                                                                          bool exponentialDistributions) {
    std::shared_ptr<storm::dft::storage::DFT<ValueType>> transformedDft = std::make_shared<storm::dft::storage::DFT<ValueType>>(dft);
    if (exponentialDistributions && !storm::dft::transformations::DftTransformer<ValueType>::hasOnlyExponentialDistributions(*transformedDft)) {
        transformedDft = storm::dft::transformations::DftTransformer<ValueType>::transformExponentialDistributions(*transformedDft);
    }
    if (uniqueBE && !storm::dft::transformations::DftTransformer<ValueType>::hasUniqueFailedBE(*transformedDft)) {
        transformedDft = storm::dft::transformations::DftTransformer<ValueType>::transformUniqueFailedBE(*transformedDft);
    }
    if (binaryFDEP && storm::dft::transformations::DftTransformer<ValueType>::hasNonBinaryDependency(*transformedDft)) {
        transformedDft = storm::dft::transformations::DftTransformer<ValueType>::transformBinaryDependencies(*transformedDft);
    }
    return transformedDft;
}
 
template<typename ValueType>
std::shared_ptr<storm::dft::storage::DFT<ValueType>> prepareForMarkovAnalysis(storm::dft::storage::DFT<ValueType> const& dft) {
    return storm::dft::api::applyTransformations(dft, true, true, true);
}
 
template<typename ValueType>
std::pair<uint64_t, uint64_t> computeBEFailureBounds(storm::dft::storage::DFT<ValueType> const& dft, bool useSMT, double solverTimeout) {
    uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout);
    uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout);
    return std::make_pair(lowerBEBound, upperBEBound);
}
 
template<typename ValueType>
bool computeDependencyConflicts(storm::dft::storage::DFT<ValueType>& dft, bool useSMT, double solverTimeout) {
    std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts =
        storm::dft::utility::FDEPConflictFinder<ValueType>::getDependencyConflicts(dft, useSMT, solverTimeout);
 
    for (auto const& pair : fdepConflicts) {
        STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name());
    }
 
    // Set the conflict map of the dft
    std::set<size_t> conflict_set;
    for (auto const& conflict : fdepConflicts) {
        conflict_set.insert(size_t(conflict.first));
        conflict_set.insert(size_t(conflict.second));
    }
    for (size_t depId : dft.getDependencies()) {
        if (!conflict_set.count(depId)) {
            dft.setDependencyNotInConflict(depId);
        }
    }
    return !fdepConflicts.empty();
}
 
storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
                                                          std::vector<std::string> const& additionalRelevantEventNames);
 
template<typename ValueType>
typename storm::dft::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(
    storm::dft::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true,
    bool allowModularisation = true, storm::dft::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
    double approximationError = 0.0, storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH,
    bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels,
    bool printOutput = false) {
    storm::dft::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
    typename storm::dft::modelchecker::DFTModelChecker<ValueType>::dft_results results =
        modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic,
                           eliminateChains, labelBehavior);
    if (printOutput) {
        modelChecker.printTimings();
        modelChecker.printResults(results);
    }
    return results;
}
 
template<typename ValueType>
void analyzeDFTBdd(std::shared_ptr<storm::dft::storage::DFT<ValueType>> const& dft, bool const exportToDot, std::string const& filename,
                   bool const calculateMttf, double const mttfPrecision, double const mttfStepsize, std::string const mttfAlgorithmName,
                   bool const calculateMCS, bool const calculateProbability, bool const useModularisation, std::string const importanceMeasureName,
                   std::vector<double> const& timepoints, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
                   std::vector<std::string> const& additionalRelevantEventNames, size_t const chunksize);
 
template<typename ValueType>
void analyzeDFTSMT(storm::dft::storage::DFT<ValueType> const& dft, bool printOutput);
 
template<typename ValueType>
void exportDFTToJsonFile(storm::dft::storage::DFT<ValueType> const& dft, std::string const& file);
 
template<typename ValueType>
std::string exportDFTToJsonString(storm::dft::storage::DFT<ValueType> const& dft);
 
template<typename ValueType>
void exportDFTToSMT(storm::dft::storage::DFT<ValueType> const& dft, std::string const& file);
 
template<typename ValueType>
std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::dft::storage::DFT<ValueType> const& dft);
 
std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace);
 
}  // namespace api
}  // namespace storm::dft