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 using DFT = storm::storage::DFT; template using DFTElement = storm::storage::DFTElement; +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::getElement, "Get DFT element at index", py::arg("index")) .def("modularisation", &DFT::topModularisation, "Split DFT into independent modules") + .def("symmetries", [](DFT& dft) { + return dft.findSymmetries(dft.colourDFT()); + }, "Compute symmetries in DFT") ; py::class_, std::shared_ptr>>(m, "ParametricDFT", "Parametric DFT") @@ -55,6 +60,18 @@ void define_dft(py::module& m) { }, "Get top level element") .def("get_element", &DFT::getElement, "Get DFT element at index", py::arg("index")) .def("modularisation", &DFT::topModularisation, "Split DFT into independent modules") + .def("symmetries", [](DFT& dft) { + return dft.findSymmetries(dft.colourDFT()); + }, "Compute symmetries in DFT") ; } + + +void define_symmetries(py::module& m) { + + py::class_>(m, "DFTSymmetries", "Symmetries in DFT") + .def_readonly("groups", &DFTSymmetries::groups, "Symmetry groups") + .def("__str__", &streamToString) + ; +} 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