analysis.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <string>
#include <utility>
#include <vector>
 
#include "storm-dft/builder/DftExplorationHeuristic.h"
#include "storm-dft/environment/DftEnvironment.h"
#include "storm-dft/modelchecker/DFTModelChecker.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/utility/RelevantEvents.h"
#include "storm/logic/Formula.h"
 
namespace storm::dft {
namespace api {

storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
                                                          std::vector<std::string> const& additionalRelevantEventNames, bool addLabelsClaiming);

template<typename ValueType>
typename storm::dft::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(
    storm::dft::DftEnvironment const& env, storm::dft::storage::DFT<ValueType> const& dft,
    std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, storm::dft::utility::RelevantEvents const& relevantEvents = {},
    bool printOutput = false, typename storm::dft::modelchecker::DFTModelChecker<ValueType>::ModelExportCallback const& exportCallback = {});

template<typename ValueType>
void analyzeDFTBdd(storm::dft::DftEnvironment const& env, 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>
std::pair<uint64_t, uint64_t> computeBEFailureBounds(storm::dft::storage::DFT<ValueType> const& dft, bool useSMT, double solverTimeout);
 
template<typename ValueType>
bool computeDependencyConflicts(storm::dft::storage::DFT<ValueType>& dft, bool useSMT, double solverTimeout);
 
}  // namespace api
}  // namespace storm::dft