29template<
typename ValueType>
30std::shared_ptr<storm::dft::storage::DFT<ValueType>>
loadDFTGalileoFile(std::string
const& file) {
40template<
typename ValueType>
41std::shared_ptr<storm::dft::storage::DFT<ValueType>>
loadDFTJsonString(std::string
const& jsonString) {
41std::shared_ptr<storm::dft::storage::DFT<ValueType>>
loadDFTJsonString(std::string
const& jsonString) {
…}
51template<
typename ValueType>
52std::shared_ptr<storm::dft::storage::DFT<ValueType>>
loadDFTJsonFile(std::string
const& file) {
52std::shared_ptr<storm::dft::storage::DFT<ValueType>>
loadDFTJsonFile(std::string
const& file) {
…}
63template<
typename ValueType>
65 std::stringstream stream;
66 bool wellFormed =
false;
67 if (validForMarkovianAnalysis) {
72 return std::pair<bool, std::string>(wellFormed, stream.str());
84template<
typename ValueType>
86 bool exponentialDistributions) {
87 std::shared_ptr<storm::dft::storage::DFT<ValueType>> transformedDft = std::make_shared<storm::dft::storage::DFT<ValueType>>(dft);
97 return transformedDft;
106template<
typename ValueType>
111template<
typename ValueType>
115 return std::make_pair(lowerBEBound, upperBEBound);
118template<
typename ValueType>
120 std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts =
123 for (
auto const& pair : fdepConflicts) {
128 std::set<size_t> conflict_set;
129 for (
auto const& conflict : fdepConflicts) {
130 conflict_set.insert(
size_t(conflict.first));
131 conflict_set.insert(
size_t(conflict.second));
134 if (!conflict_set.count(depId)) {
138 return !fdepConflicts.empty();
149 std::vector<std::string>
const& additionalRelevantEventNames);
168template<
typename ValueType>
174 bool printOutput =
false) {
177 modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic,
178 eliminateChains, labelBehavior);
180 modelChecker.printTimings();
181 modelChecker.printResults(results);
235template<
typename ValueType>
237 bool const calculateMttf,
double const mttfPrecision,
double const mttfStepsize, std::string
const mttfAlgorithmName,
238 bool const calculateMCS,
bool const calculateProbability,
bool const useModularisation, std::string
const importanceMeasureName,
239 std::vector<double>
const& timepoints, std::vector<std::shared_ptr<storm::logic::Formula const>>
const& properties,
240 std::vector<std::string>
const& additionalRelevantEventNames,
size_t const chunksize);
249template<
typename ValueType>
258template<
typename ValueType>
267template<
typename ValueType>
276template<
typename ValueType>
285template<
typename ValueType>
std::vector< boost::variant< ValueType, approximation_result > > dft_results
static storm::dft::storage::DFT< ValueType > parseDFT(std::string const &filename)
Parse DFT in Galileo format and build DFT.
static storm::dft::storage::DFT< ValueType > parseJsonFromFile(std::string const &filename)
Parse DFT from JSON format given as file and build DFT.
static storm::dft::storage::DFT< ValueType > parseJsonFromString(std::string const &jsonString)
Parse DFT from JSON format given as a string and build DFT.
Represents a Dynamic Fault Tree.
void setDependencyNotInConflict(size_t id)
DFTElementCPointer getElement(size_t index) const
Get a pointer to an element in the DFT.
std::vector< size_t > const & getDependencies() const
static bool isDftValidForMarkovianAnalysis(storm::dft::storage::DFT< ValueType > const &dft, std::ostream &stream)
Check whether the DFT can be analysed by translation to a Markov model.
static bool isDftWellFormed(storm::dft::storage::DFT< ValueType > const &dft, std::ostream &stream)
Check whether the DFT is well-formed.
static std::vector< std::pair< uint64_t, uint64_t > > getDependencyConflicts(storm::dft::storage::DFT< ValueType > const &dft, bool useSMT=false, uint_fast64_t timeout=10)
Get a vector of index pairs of FDEPs in the DFT which are conflicting.
static uint64_t getLeastFailureBound(storm::dft::storage::DFT< double > const &dft, bool useSMT=false, uint_fast64_t timeout=10)
Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to ch...
static uint64_t getAlwaysFailedBound(storm::dft::storage::DFT< double > const &dft, bool useSMT=false, uint_fast64_t timeout=10)
Get the number of BE failures for which the TLE always fails (upper bound for number of failures to c...
#define STORM_LOG_DEBUG(message)
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)
Compute the exact or approximate analysis result of the given DFT according to the given properties.
std::pair< uint64_t, uint64_t > computeBEFailureBounds(storm::dft::storage::DFT< ValueType > const &dft, bool useSMT, double solverTimeout)
std::shared_ptr< storm::jani::Model > transformToJani(storm::gspn::GSPN const &gspn, uint64_t toplevelFailedPlace)
Transform GSPN to Jani model.
void exportDFTToJsonFile(storm::dft::storage::DFT< ValueType > const &dft, std::string const &file)
Export DFT to JSON file.
void analyzeDFTBdd(std::shared_ptr< storm::dft::storage::DFT< double > > 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)
std::shared_ptr< storm::dft::storage::DFT< ValueType > > prepareForMarkovAnalysis(storm::dft::storage::DFT< ValueType > const &dft)
Apply transformations to make DFT feasible for Markovian analysis.
std::pair< bool, std::string > isWellFormed(storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis=true)
Check whether the DFT is well-formed.
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t > transformToGSPN(storm::dft::storage::DFT< double > const &dft)
std::string exportDFTToJsonString(storm::dft::storage::DFT< ValueType > const &dft)
Export DFT to JSON string.
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTGalileoFile(std::string const &file)
Load DFT from Galileo file.
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTJsonFile(std::string const &file)
Load DFT from JSON file.
storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, std::vector< std::string > const &additionalRelevantEventNames)
Get relevant event ids from given relevant event names and labels in properties.
void exportDFTToSMT(storm::dft::storage::DFT< double > const &dft, std::string const &file)
void analyzeDFTSMT(storm::dft::storage::DFT< double > const &dft, bool printOutput)
std::shared_ptr< storm::dft::storage::DFT< ValueType > > applyTransformations(storm::dft::storage::DFT< ValueType > const &dft, bool uniqueBE, bool binaryFDEP, bool exponentialDistributions)
Apply transformations for DFT.
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTJsonString(std::string const &jsonString)
Load DFT from JSON string.
bool computeDependencyConflicts(storm::dft::storage::DFT< ValueType > &dft, bool useSMT, double solverTimeout)
ApproximationHeuristic
Enum representing the heuristic used for deciding which states to expand.