From 0d756c42f115e760010c5d8453c4e117fb2a5758 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Jul 2020 16:14:16 +0200 Subject: [PATCH] Binding for computing relevant events in DFTs --- src/dft/analysis.cpp | 3 +++ tests/dft/test_analysis.py | 22 ++++++++++++++++++++++ 2 files changed, 25 insertions(+) diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index ed8033f..ba58d90 100644 --- a/src/dft/analysis.cpp +++ b/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, "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("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 1028676..9517ebe 100644 --- a/tests/dft/test_analysis.py +++ b/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)