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 using DFT = storm::storage::DFT; +template using DFTElement = storm::storage::DFTElement; void define_dft(py::module& m) { @@ -16,6 +17,18 @@ void define_dft(py::module& m) { storm::settings::addModule(); }, "Initialize Storm-dft"); + // DFT element + py::class_, std::shared_ptr>>(m, "DFTElement", "DFT element") + .def_property_readonly("id", &DFTElement::id, "Id") + .def_property_readonly("name", &DFTElement::name, "Name") + .def("__str__", &DFTElement::toString) + ; + + py::class_, std::shared_ptr>>(m, "ParametricDFTElement", "Parametric DFT element") + .def_property_readonly("id", &DFTElement::id, "Id") + .def_property_readonly("name", &DFTElement::name, "Name") + .def("__str__", &DFTElement::toString) + ; // DFT class py::class_, std::shared_ptr>>(m, "DFT", "Dynamic Fault Tree") @@ -24,6 +37,11 @@ void define_dft(py::module& m) { .def("nr_dynamic", &DFT::nrDynamicElements, "Number of dynamic elements") .def("can_have_nondeterminism", &DFT::canHaveNondeterminism, "Whether the model can contain non-deterministic choices") .def("__str__", &DFT::getInfoString) + .def_property_readonly("top_level_element", [](DFT& dft) { + return dft.getElement(dft.getTopLevelIndex()); + }, "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") ; py::class_, std::shared_ptr>>(m, "ParametricDFT", "Parametric DFT") @@ -32,6 +50,11 @@ void define_dft(py::module& m) { .def("nr_dynamic", &DFT::nrDynamicElements, "Number of dynamic elements") .def("can_have_nondeterminism", &DFT::canHaveNondeterminism, "Whether the model can contain non-deterministic choices") .def("__str__", &DFT::getInfoString) + .def_property_readonly("top_level_element", [](DFT& dft) { + return dft.getElement(dft.getTopLevelIndex()); + }, "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") ; } 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"