Interactive version: .

Dynamic Fault Trees

Building DFTs

01-dfts.py

Dynamic fault trees can be loaded from either the Galileo format or from a custom JSON form. A file containing the DFT in the Galileo format can be loaded via load_dft_galileo_file(path). The custom JSON format can be loaded from a file via load_dft_json_file(path) or directly from a string via load_dft_json_string(path). We start by loading a simple DFT containing an AND gate from JSON:

>>> import stormpy
>>> import stormpy.dft
>>> import stormpy.examples
>>> import stormpy.examples.files
>>> path_json = stormpy.examples.files.dft_json_and
>>> dft_small = stormpy.dft.load_dft_json_file(path_json)
>>> print(dft_small)

Top level index: 2, Nr BEs2

Next we load a more complex DFT from the Galileo format:

>>> path_galileo = stormpy.examples.files.dft_galileo_hecs
>>> dft = stormpy.dft.load_dft_galileo_file(path_galileo)

After loading the DFT, we can display some common statistics about the model:

>>> print("DFT with {} elements.".format(dft.nr_elements()))
>>> print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic()))

DFT with 23 elements.
DFT has 13 BEs and 2 dynamic elements.

Analyzing DFTs

01-dfts.py

The next step is to analyze the DFT via analyze_dft(dft, formula). Here we can use all standard properties as described in Building properties. In our example we compute the Mean-time-to-failure (MTTF):

>>> formula_str = "T=? [ F \"failed\" ]"
>>> formulas = stormpy.parse_properties(formula_str)
>>> results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])
>>> result = results[0]
>>> print("MTTF: {:.2f}".format(result))

MTTF: 363.89