First part of DFT documentation

doc/source/advanced_topics.rst

@@ -11,4 +11,5 @@ This guide is a collection of examples meant to bridge the gap between the getti
     doc/building_models
     doc/reward_models
     doc/shortest_paths
-    doc/parametric_models
+    doc/parametric_models
+    doc/dfts

doc/source/doc/dfts.rst

@@ -0,0 +1,48 @@
+*******************
+Dynamic Fault Trees
+*******************
+
+
+Building DFTs
+=============
+.. seealso:: `01-dfts.py <https://github.com/moves-rwth/stormpy/blob/master/examples/dfts/01-dfts.py>`_
+
+Dynamic fault trees can be loaded from either the Galileo format via ``load_dft_json(path)`` or from a custom JSON format via ``load_dft_galileo(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(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(path_galileo)
+
+After loading the DFT, we can display some common statistics about the model::
+
+    >>> print("DFT with {} elements.".format(dft.nr_elements()))
+    DFT with 23 elements.
+    >>> print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic()))
+    DFT has 13 BEs and 2 dynamic elements.
+
+
+Analyzing DFTs
+==============
+.. seealso:: `01-dfts.py <https://github.com/moves-rwth/stormpy/blob/master/examples/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 :ref:`getting-started-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

doc/source/getting_started.rst

@@ -58,6 +58,7 @@ Moreover, initial states and deadlocks are indicated with a labelling function.
 	
 We will investigate ways to examine the model in more detail in :ref:`getting-started-investigating-the-model`.
 
+.. _getting-started-building-properties:
 
 Building properties
 --------------------------

examples/dfts/01-dfts.py

@@ -0,0 +1,29 @@
+import stormpy
+import stormpy.dft
+
+import stormpy.examples
+import stormpy.examples.files
+
+
+def example_dfts_01():
+    # Load from JSON
+    path_json = stormpy.examples.files.dft_json_and
+    dft_small = stormpy.dft.load_dft_json(path_json)
+    print(dft_small)
+
+    # Load from Galileo
+    path = stormpy.examples.files.dft_galileo_hecs
+    dft = stormpy.dft.load_dft_galileo(path)
+    print("DFT with {} elements.".format(dft.nr_elements()))
+    print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic()))
+
+    # Analyze
+    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(result)
+
+
+if __name__ == '__main__':
+    example_dfts_01()

lib/stormpy/examples/files.py

@@ -26,4 +26,8 @@ drn_pdtmc_die = _path("pdtmc", "die.drn")
 jani_dtmc_die = _path("dtmc", "die.jani")
 """Jani Version of Knuth Yao Die Example"""
 prism_mdp_coin_2_2 = _path("mdp", "coin2-2.nm")
-"""Prism example for coin MDP"""
+"""Prism example for coin MDP"""
+dft_galileo_hecs = _path("dft", "hecs.dft")
+"""DFT example for HECS (Galileo format)"""
+dft_json_and = _path("dft", "and.json")
+"""DFT example for AND gate (JSON format)"""