From 10c26106c8fb185acfa089de3340a2414bf60840 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 23 Jun 2020 16:31:48 +0200
Subject: [PATCH] Bindings for DFT elements and modularisation

---
 src/dft/dft.cpp       | 23 +++++++++++++++++++++++
 tests/dft/test_dft.py | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 tests/dft/test_dft.py

diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp
index 758eee0..84d3b64 100644
--- a/src/dft/dft.cpp
+++ b/src/dft/dft.cpp
@@ -7,6 +7,7 @@
 
 
 template<typename ValueType> using DFT = storm::storage::DFT<ValueType>;
+template<typename ValueType> using DFTElement = storm::storage::DFTElement<ValueType>;
 
 
 void define_dft(py::module& m) {
@@ -16,6 +17,18 @@ void define_dft(py::module& m) {
             storm::settings::addModule<storm::settings::modules::DftIOSettings>();
         }, "Initialize Storm-dft");
 
+    // DFT element
+    py::class_<DFTElement<double>, std::shared_ptr<DFTElement<double>>>(m, "DFTElement", "DFT element")
+        .def_property_readonly("id", &DFTElement<double>::id, "Id")
+        .def_property_readonly("name", &DFTElement<double>::name, "Name")
+        .def("__str__", &DFTElement<double>::toString)
+    ;
+
+    py::class_<DFTElement<storm::RationalFunction>, std::shared_ptr<DFTElement<storm::RationalFunction>>>(m, "ParametricDFTElement", "Parametric DFT element")
+        .def_property_readonly("id", &DFTElement<storm::RationalFunction>::id, "Id")
+        .def_property_readonly("name", &DFTElement<storm::RationalFunction>::name, "Name")
+        .def("__str__", &DFTElement<storm::RationalFunction>::toString)
+    ;
 
     // DFT class
     py::class_<DFT<double>, std::shared_ptr<DFT<double>>>(m, "DFT", "Dynamic Fault Tree")
@@ -24,6 +37,11 @@ void define_dft(py::module& m) {
         .def("nr_dynamic", &DFT<double>::nrDynamicElements, "Number of dynamic elements")
         .def("can_have_nondeterminism", &DFT<double>::canHaveNondeterminism, "Whether the model can contain non-deterministic choices")
         .def("__str__", &DFT<double>::getInfoString)
+        .def_property_readonly("top_level_element", [](DFT<double>& dft) {
+                return dft.getElement(dft.getTopLevelIndex());
+            }, "Get top level element")
+        .def("get_element", &DFT<double>::getElement, "Get DFT element at index", py::arg("index"))
+        .def("modularisation", &DFT<double>::topModularisation, "Split DFT into independent modules")
     ;
 
     py::class_<DFT<storm::RationalFunction>, std::shared_ptr<DFT<storm::RationalFunction>>>(m, "ParametricDFT", "Parametric DFT")
@@ -32,6 +50,11 @@ void define_dft(py::module& m) {
         .def("nr_dynamic", &DFT<storm::RationalFunction>::nrDynamicElements, "Number of dynamic elements")
         .def("can_have_nondeterminism", &DFT<storm::RationalFunction>::canHaveNondeterminism, "Whether the model can contain non-deterministic choices")
         .def("__str__", &DFT<storm::RationalFunction>::getInfoString)
+        .def_property_readonly("top_level_element", [](DFT<storm::RationalFunction>& dft) {
+                return dft.getElement(dft.getTopLevelIndex());
+            }, "Get top level element")
+        .def("get_element", &DFT<storm::RationalFunction>::getElement, "Get DFT element at index", py::arg("index"))
+        .def("modularisation", &DFT<storm::RationalFunction>::topModularisation, "Split DFT into independent modules")
     ;
 
 }
diff --git a/tests/dft/test_dft.py b/tests/dft/test_dft.py
new file mode 100644
index 0000000..37cbe27
--- /dev/null
+++ b/tests/dft/test_dft.py
@@ -0,0 +1,32 @@
+import os
+
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+
+from configurations import dft
+
+
+@dft
+class TestDft:
+    def test_modularisation(self):
+        dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft"))
+        assert dft.nr_elements() == 23
+        assert dft.nr_be() == 13
+        assert dft.nr_dynamic() == 2
+        dfts = dft.modularisation()
+        assert len(dfts) == 4
+        for ft in dfts:
+            assert ft.top_level_element.name in ["n116", "n137", "n120", "n21"]
+
+
+@dft
+class TestDftElement:
+    def test_element(self):
+        dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
+        tle = dft.top_level_element
+        assert dft.nr_elements() == 3
+        assert dft.nr_be() == 2
+        assert dft.nr_dynamic() == 0
+        assert tle.id == 2
+        assert tle.name == "A"