From 5cb06f2ee98e4682a3c31873949fc25cf276ca12 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 23 Jun 2020 17:07:31 +0200
Subject: [PATCH] Bindings for symmetries in DFTs

---
 lib/stormpy/examples/files/dft/rc.dft | 23 +++++++++++++++++++++++
 src/dft/dft.cpp                       | 17 +++++++++++++++++
 src/dft/dft.h                         |  1 +
 src/mod_dft.cpp                       |  1 +
 tests/dft/test_dft.py                 | 26 ++++++++++++++++++++++++++
 5 files changed, 68 insertions(+)
 create mode 100644 lib/stormpy/examples/files/dft/rc.dft

diff --git a/lib/stormpy/examples/files/dft/rc.dft b/lib/stormpy/examples/files/dft/rc.dft
new file mode 100644
index 0000000..89ee18a
--- /dev/null
+++ b/lib/stormpy/examples/files/dft/rc.dft
@@ -0,0 +1,23 @@
+toplevel "n21";
+"n21" or "n198" "n210" "n160" "n165" "n235" "n199" "n217";
+"n199" wsp "n202" "n206" "n209";
+"n235" wsp "n238" "n17";
+"n210" wsp "n213" "n216";
+"n160" wsp "n163" "n162";
+"n165" wsp "n168" "n167";
+"n217" wsp "n219" "n233" "n35";
+"n202" lambda=0.0029999999999999996 dorm=0.0;
+"n206" lambda=0.0024 dorm=0.0;
+"n17" lambda=1.0E-5 dorm=0.0;
+"n198" lambda=0.3016 dorm=0.0;
+"n209" lambda=0.0018 dorm=0.0;
+"n216" lambda=1.5 dorm=0.0;
+"n213" lambda=2.0 dorm=0.0;
+"n163" lambda=1.35 dorm=0.0;
+"n238" lambda=2.0E-5 dorm=0.0;
+"n167" lambda=0.8 dorm=0.0;
+"n168" lambda=1.35 dorm=0.0;
+"n162" lambda=0.8 dorm=0.0;
+"n35" lambda=0.001 dorm=0.0;
+"n233" lambda=0.002 dorm=0.0;
+"n219" lambda=0.002 dorm=0.0;
diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp
index 84d3b64..2345012 100644
--- a/src/dft/dft.cpp
+++ b/src/dft/dft.cpp
@@ -4,10 +4,12 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
 #include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/storage/dft/DFTIsomorphism.h"
 
 
 template<typename ValueType> using DFT = storm::storage::DFT<ValueType>;
 template<typename ValueType> using DFTElement = storm::storage::DFTElement<ValueType>;
+using DFTSymmetries = storm::storage::DFTIndependentSymmetries;
 
 
 void define_dft(py::module& m) {
@@ -42,6 +44,9 @@ void define_dft(py::module& m) {
             }, "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")
+        .def("symmetries", [](DFT<double>& dft) {
+                return dft.findSymmetries(dft.colourDFT());
+            }, "Compute symmetries in DFT")
     ;
 
     py::class_<DFT<storm::RationalFunction>, std::shared_ptr<DFT<storm::RationalFunction>>>(m, "ParametricDFT", "Parametric DFT")
@@ -55,6 +60,18 @@ void define_dft(py::module& m) {
             }, "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")
+        .def("symmetries", [](DFT<storm::RationalFunction>& dft) {
+                return dft.findSymmetries(dft.colourDFT());
+            }, "Compute symmetries in DFT")
     ;
 
 }
+
+
+void define_symmetries(py::module& m) {
+
+    py::class_<DFTSymmetries, std::shared_ptr<DFTSymmetries>>(m, "DFTSymmetries", "Symmetries in DFT")
+        .def_readonly("groups", &DFTSymmetries::groups, "Symmetry groups")
+        .def("__str__", &streamToString<DFTSymmetries>)
+    ;
+}
diff --git a/src/dft/dft.h b/src/dft/dft.h
index 147b75a..e11200f 100644
--- a/src/dft/dft.h
+++ b/src/dft/dft.h
@@ -3,3 +3,4 @@
 #include "common.h"
 
 void define_dft(py::module& m);
+void define_symmetries(py::module& m);
diff --git a/src/mod_dft.cpp b/src/mod_dft.cpp
index 315cc7c..cede358 100644
--- a/src/mod_dft.cpp
+++ b/src/mod_dft.cpp
@@ -13,6 +13,7 @@ PYBIND11_MODULE(dft, m) {
 #endif
 
     define_dft(m);
+    define_symmetries(m);
     define_input(m);
     define_output(m);
     define_analysis(m);
diff --git a/tests/dft/test_dft.py b/tests/dft/test_dft.py
index 37cbe27..d68b029 100644
--- a/tests/dft/test_dft.py
+++ b/tests/dft/test_dft.py
@@ -30,3 +30,29 @@ class TestDftElement:
         assert dft.nr_dynamic() == 0
         assert tle.id == 2
         assert tle.name == "A"
+
+@dft
+class TestDftSymmetries:
+    def test_symmetries_small(self):
+        dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
+        symmetries = dft.symmetries()
+        assert len(symmetries.groups) == 1
+        for index, group in symmetries.groups.items():
+            assert len(group) == 1
+            for syms in group:
+                assert len(syms) == 2
+                for elem in syms:
+                    assert elem == 0 or elem == 1
+
+    def test_symmetries(self):
+        dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc.dft"))
+        symmetries = dft.symmetries()
+        assert len(symmetries.groups) == 1
+        for index, group in symmetries.groups.items():
+            assert len(group) == 3
+            i = 4
+            for syms in group:
+                assert len(syms) == 2
+                for elem in syms:
+                    assert elem == i or elem == i+3
+                i += 1