Bisimulation takes properties

lib/stormpy/__init__.py

@@ -94,11 +94,12 @@ def build_parametric_model_from_drn(file):
     else:
         raise RuntimeError("Not supported parametric model constructed")
 
-def perform_bisimulation(model, property, bisimulation_type):
+def perform_bisimulation(model, properties, bisimulation_type):
+    formulae = [prop.raw_formula for prop in properties]
     if model.supports_parameters:
-        return core._perform_parametric_bisimulation(model, property.raw_formula, bisimulation_type)
+        return core._perform_parametric_bisimulation(model, formulae, bisimulation_type)
     else:
-        return core._perform_bisimulation(model, property.raw_formula, bisimulation_type)
+        return core._perform_bisimulation(model, formulae, bisimulation_type)
 
 def model_checking(model, property):
     if model.supports_parameters:

src/core/bisimulation.cpp

@@ -2,16 +2,16 @@
 
 // Thin wrapper for bisimulation
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, storm::storage::BisimulationType bisimulationType) {
-    return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formula, bisimulationType);
+std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType bisimulationType) {
+    return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formulas, bisimulationType);
 }
 
 // Define python bindings
 void define_bisimulation(py::module& m) {
 
     // Bisimulation
-    m.def("_perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type"));
-    m.def("_perform_parametric_bisimulation", &performBisimulation<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type"));
+    m.def("_perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
+    m.def("_perform_parametric_bisimulation", &performBisimulation<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

@@ -2,6 +2,8 @@ import stormpy
 import stormpy.logic
 from helpers.helper import get_example_path
 
+import math
+
 class TestBisimulation:
     def test_bisimulation(self):
         program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm"))
@@ -14,13 +16,21 @@ class TestBisimulation:
         assert model.nr_transitions == 13041
         assert model.model_type == stormpy.ModelType.DTMC
         assert not model.supports_parameters
-        model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG)
+        initial_state = model.initial_states[0]
+        assert initial_state == 0
+        result = stormpy.model_checking(model, properties[0])
+        model_bisim = stormpy.perform_bisimulation(model, properties, stormpy.BisimulationType.STRONG)
         assert model_bisim.nr_states == 64
         assert model_bisim.nr_transitions == 104
         assert model_bisim.model_type == stormpy.ModelType.DTMC
         assert not model_bisim.supports_parameters
+        result_bisim = stormpy.model_checking(model_bisim, properties[0])
+        initial_state_bisim = model_bisim.initial_states[0]
+        assert initial_state_bisim == 34
+        assert math.isclose(result.at(initial_state), result_bisim.at(initial_state_bisim), rel_tol=1e-4)
     
     def test_parametric_bisimulation(self):
+        import pycarl
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm"))
         assert program.nr_modules == 1
         assert program.model_type == stormpy.PrismModelType.DTMC
@@ -32,8 +42,11 @@ class TestBisimulation:
         assert model.nr_transitions == 2027
         assert model.model_type == stormpy.ModelType.DTMC
         assert model.has_parameters
-        model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG)
+        result = stormpy.model_checking(model, properties[0])
+        model_bisim = stormpy.perform_bisimulation(model, properties, stormpy.BisimulationType.STRONG)
         assert model_bisim.nr_states == 80
         assert model_bisim.nr_transitions == 120
         assert model_bisim.model_type == stormpy.ModelType.DTMC
         assert model_bisim.has_parameters
+        result_bisim = stormpy.model_checking(model_bisim, properties[0])
+        assert result.result_function == result_bisim.result_function