Bindings for DFT transformations

lib/stormpy/examples/files/dft/rc2.dft

@@ -0,0 +1,16 @@
+toplevel "System";
+"System" or "controller" "sensor_1" "barrier_1";
+"sensor_1" 2of4 "sA_1" "sB_1" "sC_1" "sD_1";
+"network_1_f" fdep "network_1" "sA_1" "sB_1" "sC_1" "sD_1";
+"barrier_1" or "switch_1" "motors_1";
+"motors_1" wsp "mP_1" "mS_1";
+"switch_1" pand "sw_1" "mP_1";
+"network_1" lambda=0.03 dorm=0;
+"sA_1" lambda=0.05 dorm=0;
+"sB_1" lambda=0.05 dorm=0;
+"sC_1" lambda=0.05 dorm=0;
+"sD_1" lambda=0.05 dorm=0;
+"sw_1" lambda=0.015 dorm=0;
+"mP_1" lambda=0.08 dorm=0;
+"mS_1" lambda=0.08 dorm=0.5;
+"controller" lambda=0.03 dorm=0;

src/dft/analysis.cpp

@@ -26,5 +26,9 @@ void define_analysis(py::module& m) {
 
     m.def("analyze_dft", &analyzeDFT<double>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=std::set<size_t>(), py::arg("dc_for_relevant")=false);
 
+    m.def("transform_dft", &storm::api::applyTransformations<double>, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"), py::arg("binary_fdeps"));
+
+    m.def("is_well_formed", &storm::api::isWellFormed<double>, "Check whether DFT is well-formed.", py::arg("dft"), py::arg("check_valid_for_analysis") = true);
+
     m.def("compute_relevant_events", &storm::api::computeRelevantEvents<double>, "Compute relevant event ids from properties and additional relevant names", py::arg("dft"), py::arg("properties"), py::arg("additional_relevant_names") = std::vector<std::string>());
 }

tests/dft/test_analysis.py

@@ -37,3 +37,15 @@ class TestAnalysis:
         assert 1 in relevant_ids
         results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_ids)
         assert math.isclose(results[0], 0.1548181217)
+
+    def test_transformation(self):
+        dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc2.dft"))
+        valid, output = stormpy.dft.is_well_formed(dft)
+        assert not valid
+        assert "not binary" in output
+        dft = stormpy.dft.transform_dft(dft, unique_constant_be=True, binary_fdeps=True)
+        valid, output = stormpy.dft.is_well_formed(dft)
+        assert valid
+        formulas = stormpy.parse_properties("Tmin=? [ F \"failed\" ]")
+        results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])
+        assert math.isclose(results[0], 6.380930905)