From 8dfd0b4332233c8911c757fa66ae3150514627d2 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 6 Aug 2018 15:19:15 +0200
Subject: [PATCH] First part of DFT documentation

---
 doc/source/advanced_topics.rst |  3 ++-
 doc/source/doc/dfts.rst        | 48 ++++++++++++++++++++++++++++++++++
 doc/source/getting_started.rst |  1 +
 examples/dfts/01-dfts.py       | 29 ++++++++++++++++++++
 lib/stormpy/examples/files.py  |  6 ++++-
 5 files changed, 85 insertions(+), 2 deletions(-)
 create mode 100644 doc/source/doc/dfts.rst
 create mode 100644 examples/dfts/01-dfts.py

diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst
index 765149a..dc4a8e3 100644
--- a/doc/source/advanced_topics.rst
+++ b/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
\ No newline at end of file
+    doc/parametric_models
+    doc/dfts
\ No newline at end of file
diff --git a/doc/source/doc/dfts.rst b/doc/source/doc/dfts.rst
new file mode 100644
index 0000000..c143a2d
--- /dev/null
+++ b/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
diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst
index 947036a..abf1c57 100644
--- a/doc/source/getting_started.rst
+++ b/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
 --------------------------
diff --git a/examples/dfts/01-dfts.py b/examples/dfts/01-dfts.py
new file mode 100644
index 0000000..691d150
--- /dev/null
+++ b/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()
diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py
index 61d9fdb..cb4718d 100644
--- a/lib/stormpy/examples/files.py
+++ b/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"""
\ No newline at end of file
+"""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)"""