From c30d5a1433f04b1b19d43866d22537779b20c800 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 18 May 2018 17:47:02 +0200
Subject: [PATCH] Symbolic bisimulation

---
 lib/stormpy/__init__.py         | 26 ++++++++++++++++++++++++++
 src/core/bisimulation.cpp       |  8 ++++++++
 tests/core/test_bisimulation.py | 17 ++++++++++++++++-
 3 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index 1424892..7d76643 100644
--- a/lib/stormpy/__init__.py
+++ b/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.
diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp
index 7feddd0..e7746ba 100644
--- a/src/core/bisimulation.cpp
+++ b/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")
diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py
index 418defc..b16ccc2 100644
--- a/tests/core/test_bisimulation.py
+++ b/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
\ No newline at end of file