From 432893aa556b6e6a4af5bfb31d8afb8a720ef5c9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 29 Jul 2020 16:38:50 +0200 Subject: [PATCH] Bindings for DFT transformations --- lib/stormpy/examples/files/dft/rc2.dft | 16 ++++++++++++++++ src/dft/analysis.cpp | 4 ++++ tests/dft/test_analysis.py | 12 ++++++++++++ 3 files changed, 32 insertions(+) create mode 100644 lib/stormpy/examples/files/dft/rc2.dft diff --git a/lib/stormpy/examples/files/dft/rc2.dft b/lib/stormpy/examples/files/dft/rc2.dft new file mode 100644 index 0000000..dc65f3c --- /dev/null +++ b/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; diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index ba58d90..12cb279 100644 --- a/src/dft/analysis.cpp +++ b/src/dft/analysis.cpp @@ -26,5 +26,9 @@ void define_analysis(py::module& m) { m.def("analyze_dft", &analyzeDFT, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("relevant_events")=std::set(), py::arg("dc_for_relevant")=false); + m.def("transform_dft", &storm::api::applyTransformations, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"), py::arg("binary_fdeps")); + + m.def("is_well_formed", &storm::api::isWellFormed, "Check whether DFT is well-formed.", py::arg("dft"), py::arg("check_valid_for_analysis") = true); + m.def("compute_relevant_events", &storm::api::computeRelevantEvents, "Compute relevant event ids from properties and additional relevant names", py::arg("dft"), py::arg("properties"), py::arg("additional_relevant_names") = std::vector()); } diff --git a/tests/dft/test_analysis.py b/tests/dft/test_analysis.py index 9517ebe..a3280ad 100644 --- a/tests/dft/test_analysis.py +++ b/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)