diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index 164d884..544d2f3 100644 --- a/src/dft/analysis.cpp +++ b/src/dft/analysis.cpp @@ -9,9 +9,8 @@ // Thin wrapper for DFT analysis template -//std::vector analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH) { -std::vector analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, std::set const& relevantEvents, bool allowDCForRelevant) { - typename storm::modelchecker::DFTModelChecker::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false); +std::vector analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) { + typename storm::modelchecker::DFTModelChecker::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false); std::vector results; for (auto result : dftResults) { @@ -23,8 +22,12 @@ std::vector analyzeDFT(storm::storage::DFT const& dft, std // Define python bindings void define_analysis(py::module& m) { + // RelevantEvents + py::class_>(m, "RelevantEvents", "Relevant events which should be observed") + .def("is_relevant", &storm::utility::RelevantEvents::isRelevant, "Check whether the given name is a relevant event", py::arg("name")) + ; - 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("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")=storm::utility::RelevantEvents()); m.def("transform_dft", &storm::api::applyTransformations, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"), py::arg("binary_fdeps")); @@ -32,5 +35,5 @@ void define_analysis(py::module& m) { 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()); + 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(), py::arg("allow_dc_relevant") = false); } diff --git a/tests/dft/test_analysis.py b/tests/dft/test_analysis.py index ea4f4fa..dffb3b5 100644 --- a/tests/dft/test_analysis.py +++ b/tests/dft/test_analysis.py @@ -20,22 +20,22 @@ class TestAnalysis: 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) + relevant_events = stormpy.dft.compute_relevant_events(dft, formulas) + assert relevant_events.is_relevant("A") + assert not relevant_events.is_relevant("B") + assert not relevant_events.is_relevant("C") + results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_events) 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) + relevant_events = stormpy.dft.compute_relevant_events(dft, formulas, ["B", "C"]) + assert relevant_events.is_relevant("B") + assert relevant_events.is_relevant("C") + assert not relevant_events.is_relevant("A") + results = stormpy.dft.analyze_dft(dft, formulas, relevant_events = relevant_events) assert math.isclose(results[0], 0.1548181217) def test_transformation(self):