From 77fe824f0aa018b6dd32da78933f8a0f00866f39 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Jul 2020 13:47:10 +0200 Subject: [PATCH] Compute FDEP conflicts to avoid non-determinism in DFT analysis --- src/dft/analysis.cpp | 2 ++ tests/dft/test_analysis.py | 9 +++++++++ 2 files changed, 11 insertions(+) diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index 12cb279..164d884 100644 --- a/src/dft/analysis.cpp +++ b/src/dft/analysis.cpp @@ -28,6 +28,8 @@ void define_analysis(py::module& m) { 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("compute_dependency_conflicts", &storm::api::computeDependencyConflicts, "Set conflicts between FDEPs. Is used in analysis.", py::arg("dft"), py::arg("use_smt") = false, py::arg("solver_timeout") = 0); + 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 a3280ad..ea4f4fa 100644 --- a/tests/dft/test_analysis.py +++ b/tests/dft/test_analysis.py @@ -49,3 +49,12 @@ class TestAnalysis: formulas = stormpy.parse_properties("Tmin=? [ F \"failed\" ]") results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) assert math.isclose(results[0], 6.380930905) + + def test_fdep_conflicts(self): + dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc2.dft")) + dft = stormpy.dft.transform_dft(dft, unique_constant_be=True, binary_fdeps=True) + has_conflicts = stormpy.dft.compute_dependency_conflicts(dft, use_smt=False, solver_timeout=0) + assert not has_conflicts + formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) + assert math.isclose(results[0], 6.380930905)