stormpy.dft

API for Dynamic Fault Tree (DFT) analysis.

Makes the functionality of storm::dft:: available.

Functions

analyze_dft(dft, properties, *[, ...])	Analyze the DFT with respect to the given properties.
build_model(dft, *[, symmetries, ...])	Build state-space model (CTMC or MA) for the given DFT.
check_dft_validity(dft)	Check validity of DFT.
compute_relevant_events(properties, *[, ...])	Compute the relevant events for the analysis of a DFT.
export_dft_json_file(dft, path)	Export a DFT to a file in the JSON format.
export_dft_json_string(...)	Export DFT to JSON string
load_dft_galileo_file	Load a DFT from a file in the Galileo format.
load_dft_json_file	Load a DFT from a file in the JSON format.
load_dft_json_string	Load DFT from JSON string
modules(dft)	Compute the independent-module decomposition of a DFT.
modules_json(dft)	Create JSON representation of DFT modules.
prepare_for_analysis(dft)	Prepare a DFT for analysis.

Classes

AnalysisEnvironment	Environment configuring the DFT analysis
ApproximationHeuristic(*values)	Heuristic for selecting states to explore next
DFT	Dynamic Fault Tree
DFTBE	Basic Event
DFTDependency	Dependency
DFTElement	DFT element
DFTElementType(*values)
DftEnvironment(self)	Environment for DFT
DftIndependentModule(native, dft)	An independent module of a DFT: a subtree that can be analyzed in isolation.
DftInstantiator	Instantiator for parametric DFT
DFTSimulator(dft, *[, seed, relevant_events])	High-level simulator for Dynamic Fault Trees.
DFTState	DFT state
DftSymmetries(self)	Symmetries in DFT
ModelBuilderEnvironment	Environment configuring the Markov model building from a DFT
RelevantEvents(self)	Relevant events which should be observed
SimulationStepResult(*values)
SimulationTraceResult(*values)
TransformationEnvironment	Environment configuring transformation of the built model