Extended bindings for DFT class

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;

src/dft/dft.cpp

@@ -17,11 +17,19 @@ void define_dft(py::module& m) {
 
     // DFT class
     py::class_<DFT<double>, std::shared_ptr<DFT<double>>>(m, "DFT", "DFT")
-        .def("nr_elements", &DFT<double>::nrElements)
+        .def("nr_elements", &DFT<double>::nrElements, "Total number of elements")
+        .def("nr_be", &DFT<double>::nrBasicElements, "Number of basic elements")
+        .def("nr_dynamic", &DFT<double>::nrDynamicElements, "Number of dynamic elements")
+        .def("can_have_nondeterminism", &DFT<double>::canHaveNondeterminism, "Whether the model can contain non-deterministic choices")
+        .def("__str__", &DFT<double>::getInfoString)
     ;
 
     py::class_<DFT<storm::RationalFunction>, std::shared_ptr<DFT<storm::RationalFunction>>>(m, "ParametricDFT", "Parametric DFT")
-        .def("nr_elements", &DFT<storm::RationalFunction>::nrElements)
+        .def("nr_elements", &DFT<storm::RationalFunction>::nrElements, "Total number of elements")
+        .def("nr_be", &DFT<storm::RationalFunction>::nrBasicElements, "Number of basic elements")
+        .def("nr_dynamic", &DFT<storm::RationalFunction>::nrDynamicElements, "Number of dynamic elements")
+        .def("can_have_nondeterminism", &DFT<storm::RationalFunction>::canHaveNondeterminism, "Whether the model can contain non-deterministic choices")
+        .def("__str__", &DFT<storm::RationalFunction>::getInfoString)
     ;
 
 }

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