Compute FDEP conflicts to avoid non-determinism in DFT analysis

src/dft/analysis.cpp

@@ -28,6 +28,8 @@ void define_analysis(py::module& m) {
 
     m.def("transform_dft", &storm::api::applyTransformations<double>, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"), py::arg("binary_fdeps"));
 
+    m.def("compute_dependency_conflicts", &storm::api::computeDependencyConflicts<double>, "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<double>, "Check whether DFT is well-formed.", py::arg("dft"), py::arg("check_valid_for_analysis") = true);
 
     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

@@ -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)