Symbolic bisimulation

lib/stormpy/__init__.py

@@ -217,6 +217,17 @@ def perform_bisimulation(model, properties, bisimulation_type):
     :param bisimulation_type: Type of bisimulation (weak or strong).
     :return: Model after bisimulation.
     """
+    return perform_sparse_bisimulation(model, properties, bisimulation_type)
+
+
+def perform_sparse_bisimulation(model, properties, bisimulation_type):
+    """
+    Perform bisimulation on model in sparse representation.
+    :param model: Model.
+    :param properties: Properties to preserve during bisimulation.
+    :param bisimulation_type: Type of bisimulation (weak or strong).
+    :return: Model after bisimulation.
+    """
     formulae = [prop.raw_formula for prop in properties]
     if model.supports_parameters:
         return core._perform_parametric_bisimulation(model, formulae, bisimulation_type)
@@ -224,6 +235,21 @@ def perform_bisimulation(model, properties, bisimulation_type):
         return core._perform_bisimulation(model, formulae, bisimulation_type)
 
 
+def perform_symbolic_bisimulation(model, properties):
+    """
+    Perform bisimulation on model in symbolic representation.
+    :param model: Model.
+    :param properties: Properties to preserve during bisimulation.
+    :return: Model after bisimulation.
+    """
+    formulae = [prop.raw_formula for prop in properties]
+    bisimulation_type = BisimulationType.STRONG
+    if model.supports_parameters:
+        return core._perform_symbolic_parametric_bisimulation(model, formulae, bisimulation_type)
+    else:
+        return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type)
+
+
 def model_checking(model, property, only_initial_states=False, extract_scheduler=False):
     """
     Perform model checking on model for property.

src/core/bisimulation.cpp

@@ -1,11 +1,19 @@
 #include "bisimulation.h"
 
+
+template <storm::dd::DdType DdType, typename ValueType>
+std::shared_ptr<storm::models::Model<ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong) {
+    return storm::api::performBisimulationMinimization<DdType, ValueType, ValueType>(model, formulas, bisimulationType, storm::dd::bisimulation::SignatureMode::Eager);
+}
+
 // Define python bindings
 void define_bisimulation(py::module& m) {
 
     // Bisimulation
     m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization<double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
     m.def("_perform_parametric_bisimulation", &storm::api::performBisimulationMinimization<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
+    m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
+    m.def("_perform_symbolic_parametric_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
 
     // BisimulationType
     py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")

tests/core/test_bisimulation.py

@@ -31,6 +31,21 @@ class TestBisimulation:
         assert initial_state_bisim == 34
         assert math.isclose(result.at(initial_state), result_bisim.at(initial_state_bisim), rel_tol=1e-4)
 
+    def test_symbolic_bisimulation(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm"))
+        prop = "P=? [F \"observe0Greater1\"]"
+        properties = stormpy.parse_properties_for_prism_program(prop, program)
+        model = stormpy.build_symbolic_model(program, properties)
+        assert model.nr_states == 7403
+        assert model.nr_transitions == 13041
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert not model.supports_parameters
+        model_bisim = stormpy.perform_symbolic_bisimulation(model, properties)
+        assert model_bisim.nr_states == 65
+        assert model_bisim.nr_transitions == 105
+        assert model_bisim.model_type == stormpy.ModelType.DTMC
+        assert not model_bisim.supports_parameters
+
     def test_parametric_bisimulation(self):
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
         assert program.nr_modules == 5
@@ -60,4 +75,4 @@ class TestBisimulation:
         initial_state_bisim = model_bisim.initial_states[0]
         assert initial_state_bisim == 316
         ratFunc_bisim = result_bisim.at(initial_state_bisim)
-        assert ratFunc == ratFunc_bisim
+        assert ratFunc == ratFunc_bisim