diff --git a/lib/stormpy/examples/files/dft/hecs.dft b/lib/stormpy/examples/files/dft/hecs.dft new file mode 100644 index 0000000..b470ff9 --- /dev/null +++ b/lib/stormpy/examples/files/dft/hecs.dft @@ -0,0 +1,24 @@ +toplevel "n0"; +"n0" or "n116" "n137" "n120" "n21"; +"n137" wsp "n139" "n9"; +"n120" wsp "n118" "n134" "n10"; +"n21" 3of5 "n111" "n109" "n117" "n110" "n112"; +"n110" or "n18" "n7"; +"n117" or "n17" "n7"; +"n109" or "n15" "n23"; +"n112" or "n19" "n13"; +"n13" and "n23" "n7"; +"n111" or "n14" "n23"; +"n116" lambda=0.0018 dorm=0.0; +"n139" lambda=2.0E-5 dorm=0.0; +"n10" lambda=0.001 dorm=0.0; +"n118" lambda=0.002 dorm=0.0; +"n18" lambda=6.0E-4 dorm=0.0; +"n17" lambda=6.0E-4 dorm=0.0; +"n15" lambda=6.0E-4 dorm=0.0; +"n19" lambda=6.0E-4 dorm=0.0; +"n7" lambda=5.0E-4 dorm=0.0; +"n23" lambda=5.0E-4 dorm=0.0; +"n14" lambda=6.0E-4 dorm=0.0; +"n134" lambda=0.002 dorm=0.0; +"n9" lambda=1.0E-5 dorm=0.0; diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp index c9c06a4..7af27d4 100644 --- a/src/dft/dft.cpp +++ b/src/dft/dft.cpp @@ -17,11 +17,19 @@ void define_dft(py::module& m) { // DFT class py::class_, std::shared_ptr>>(m, "DFT", "DFT") - .def("nr_elements", &DFT::nrElements) + .def("nr_elements", &DFT::nrElements, "Total number of elements") + .def("nr_be", &DFT::nrBasicElements, "Number of basic elements") + .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) ; py::class_, std::shared_ptr>>(m, "ParametricDFT", "Parametric DFT") - .def("nr_elements", &DFT::nrElements) + .def("nr_elements", &DFT::nrElements, "Total number of elements") + .def("nr_be", &DFT::nrBasicElements, "Number of basic elements") + .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) ; } diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py index 09fcc3f..d9a84fe 100644 --- a/tests/dft/test_build.py +++ b/tests/dft/test_build.py @@ -8,7 +8,21 @@ from configurations import dft @dft class TestBuild: - def test_build_dft(self): + def test_load_dft_json(self): + dft = stormpy.dft.load_dft_json(get_example_path("dft", "and.json")) + assert dft.nr_elements() == 3 + assert dft.nr_be() == 2 + assert dft.nr_dynamic() == 0 + assert not dft.can_have_nondeterminism() + + def test_load_dft_galileo(self): + dft = stormpy.dft.load_dft_galileo(get_example_path("dft", "hecs.dft")) + assert dft.nr_elements() == 23 + assert dft.nr_be() == 13 + assert dft.nr_dynamic() == 2 + assert not dft.can_have_nondeterminism() + + def test_analyze_mttf(self): dft = stormpy.dft.load_dft_json(get_example_path("dft", "and.json")) formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") assert dft.nr_elements() == 3