Binding for computing relevant events in DFTs

src/dft/analysis.cpp

@@ -3,6 +3,8 @@
 #include "storm-dft/parser/DFTJsonParser.h"
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
+#include "storm-dft/api/storm-dft.h"
+
 
 
 // Thin wrapper for DFT analysis
@@ -24,4 +26,5 @@ 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("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

@@ -15,3 +15,25 @@ class TestAnalysis:
         assert dft.nr_elements() == 3
         results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])
         assert math.isclose(results[0], 3)
+
+    def test_relevant_events_property(self):
+        dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
+        properties = stormpy.parse_properties("P=? [ F<=1 \"A_failed\" ]")
+        formulas = [p.raw_formula for p in properties]
+        relevant_ids = stormpy.dft.compute_relevant_events(dft, formulas)
+        assert len(relevant_ids) == 1
+        index = next(iter(relevant_ids))
+        assert dft.get_element(index).name == "A"
+        results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_ids)
+        assert math.isclose(results[0], 0.1548181217)
+
+    def test_relevant_events_additional(self):
+        dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
+        properties = stormpy.parse_properties("P=? [ F<=1 \"failed\" ]")
+        formulas = [p.raw_formula for p in properties]
+        relevant_ids = stormpy.dft.compute_relevant_events(dft, formulas, ["B", "C"])
+        assert len(relevant_ids) == 2
+        assert 0 in relevant_ids
+        assert 1 in relevant_ids
+        results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_ids)
+        assert math.isclose(results[0], 0.1548181217)