Bindings for symmetries in DFTs

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;

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>)
+    ;
+}

src/dft/dft.h

@@ -3,3 +3,4 @@
 #include "common.h"
 
 void define_dft(py::module& m);
+void define_symmetries(py::module& m);

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);

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