Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm-dft.h
Go to the documentation of this file.
1#pragma once
2
3#include <type_traits>
4#include <utility>
5#include <vector>
6
17
19
20namespace storm::dft {
21namespace api {
22
29template<typename ValueType>
30std::shared_ptr<storm::dft::storage::DFT<ValueType>> loadDFTGalileoFile(std::string const& file) {
31 return std::make_shared<storm::dft::storage::DFT<ValueType>>(storm::dft::parser::DFTGalileoParser<ValueType>::parseDFT(file));
32}
33
40template<typename ValueType>
41std::shared_ptr<storm::dft::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) {
42 return std::make_shared<storm::dft::storage::DFT<ValueType>>(storm::dft::parser::DFTJsonParser<ValueType>::parseJsonFromString(jsonString));
43}
44
51template<typename ValueType>
52std::shared_ptr<storm::dft::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) {
53 return std::make_shared<storm::dft::storage::DFT<ValueType>>(storm::dft::parser::DFTJsonParser<ValueType>::parseJsonFromFile(file));
54}
55
63template<typename ValueType>
64std::pair<bool, std::string> isWellFormed(storm::dft::storage::DFT<ValueType> const& dft, bool validForMarkovianAnalysis = true) {
65 std::stringstream stream;
66 bool wellFormed = false;
67 if (validForMarkovianAnalysis) {
69 } else {
71 }
72 return std::pair<bool, std::string>(wellFormed, stream.str());
73}
74
84template<typename ValueType>
85std::shared_ptr<storm::dft::storage::DFT<ValueType>> applyTransformations(storm::dft::storage::DFT<ValueType> const& dft, bool uniqueBE, bool binaryFDEP,
86 bool exponentialDistributions) {
87 std::shared_ptr<storm::dft::storage::DFT<ValueType>> transformedDft = std::make_shared<storm::dft::storage::DFT<ValueType>>(dft);
90 }
93 }
96 }
97 return transformedDft;
98}
99
106template<typename ValueType>
107std::shared_ptr<storm::dft::storage::DFT<ValueType>> prepareForMarkovAnalysis(storm::dft::storage::DFT<ValueType> const& dft) {
108 return storm::dft::api::applyTransformations(dft, true, true, true);
109}
110
111template<typename ValueType>
112std::pair<uint64_t, uint64_t> computeBEFailureBounds(storm::dft::storage::DFT<ValueType> const& dft, bool useSMT, double solverTimeout) {
113 uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout);
114 uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout);
115 return std::make_pair(lowerBEBound, upperBEBound);
116}
117
118template<typename ValueType>
119bool computeDependencyConflicts(storm::dft::storage::DFT<ValueType>& dft, bool useSMT, double solverTimeout) {
120 std::vector<std::pair<uint64_t, uint64_t>> fdepConflicts =
122
123 for (auto const& pair : fdepConflicts) {
124 STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name());
125 }
126
127 // Set the conflict map of the dft
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));
132 }
133 for (size_t depId : dft.getDependencies()) {
134 if (!conflict_set.count(depId)) {
136 }
137 }
138 return !fdepConflicts.empty();
139}
140
148storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
149 std::vector<std::string> const& additionalRelevantEventNames);
150
168template<typename ValueType>
170 storm::dft::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true,
171 bool allowModularisation = true, storm::dft::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
172 double approximationError = 0.0, storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH,
174 bool printOutput = false) {
177 modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic,
178 eliminateChains, labelBehavior);
179 if (printOutput) {
180 modelChecker.printTimings();
181 modelChecker.printResults(results);
182 }
183 return results;
184}
185
235template<typename ValueType>
236void analyzeDFTBdd(std::shared_ptr<storm::dft::storage::DFT<ValueType>> const& dft, bool const exportToDot, std::string const& filename,
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);
241
249template<typename ValueType>
250void analyzeDFTSMT(storm::dft::storage::DFT<ValueType> const& dft, bool printOutput);
251
258template<typename ValueType>
259void exportDFTToJsonFile(storm::dft::storage::DFT<ValueType> const& dft, std::string const& file);
260
267template<typename ValueType>
269
276template<typename ValueType>
277void exportDFTToSMT(storm::dft::storage::DFT<ValueType> const& dft, std::string const& file);
278
285template<typename ValueType>
286std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::dft::storage::DFT<ValueType> const& dft);
287
295std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace);
296
297} // namespace api
298} // namespace storm::dft
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.
Definition DFT.h:52
void setDependencyNotInConflict(size_t id)
Definition DFT.h:148
DFTElementCPointer getElement(size_t index) const
Get a pointer to an element in the DFT.
Definition DFT.h:188
std::vector< size_t > const & getDependencies() const
Definition DFT.h:153
Transformer for operations on DFT.
static std::shared_ptr< storm::dft::storage::DFT< ValueType > > transformUniqueFailedBE(storm::dft::storage::DFT< ValueType > const &dft)
Introduce unique BE which is always failed (instead of multiple ones).
static std::shared_ptr< storm::dft::storage::DFT< ValueType > > transformBinaryDependencies(storm::dft::storage::DFT< ValueType > const &dft)
Introduce binary dependencies (with only one dependent event) instead of dependencies with multiple d...
static std::shared_ptr< storm::dft::storage::DFT< ValueType > > transformExponentialDistributions(storm::dft::storage::DFT< ValueType > const &dft)
Replace certain BE distributions by DFT constructs using only exponential distributions to make them ...
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)
Definition logging.h:23
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.
Definition storm-dft.h:169
std::pair< uint64_t, uint64_t > computeBEFailureBounds(storm::dft::storage::DFT< ValueType > const &dft, bool useSMT, double solverTimeout)
Definition storm-dft.h:112
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)
Definition storm-dft.cpp:23
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.
Definition storm-dft.h:107
std::pair< bool, std::string > isWellFormed(storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis=true)
Check whether the DFT is well-formed.
Definition storm-dft.h:64
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.
Definition storm-dft.h:30
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTJsonFile(std::string const &file)
Load DFT from JSON file.
Definition storm-dft.h:52
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.
Definition storm-dft.h:85
std::shared_ptr< storm::dft::storage::DFT< ValueType > > loadDFTJsonString(std::string const &jsonString)
Load DFT from JSON string.
Definition storm-dft.h:41
bool computeDependencyConflicts(storm::dft::storage::DFT< ValueType > &dft, bool useSMT, double solverTimeout)
Definition storm-dft.h:119
ApproximationHeuristic
Enum representing the heuristic used for deciding which states to expand.
EliminationLabelBehavior
Specify criteria whether a state can be eliminated and how its labels should be treated.