Adaption to changes of relevant events in Storm

src/dft/analysis.cpp

@@ -9,9 +9,8 @@
 
 // Thin wrapper for DFT analysis
 template<typename ValueType>
-//std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH) {
-std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevant) {
-    typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false);
+std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) {
+    typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, relevantEvents, 0.0, storm::builder::ApproximationHeuristic::DEPTH, false);
 
     std::vector<ValueType> results;
     for (auto result : dftResults) {
@@ -23,8 +22,12 @@ std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std
 
 // Define python bindings
 void define_analysis(py::module& m) {
+    // RelevantEvents
+    py::class_<storm::utility::RelevantEvents, std::shared_ptr<storm::utility::RelevantEvents>>(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<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("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")=storm::utility::RelevantEvents());
 
     m.def("transform_dft", &storm::api::applyTransformations<double>, "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<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>());
+    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>(), py::arg("allow_dc_relevant") = false);
 }

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