From 20b1b01139b177057bbef32d202827df566fdd2c Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 28 Mar 2017 14:01:29 +0200
Subject: [PATCH] Bisimulation takes properties

---
 lib/stormpy/__init__.py         |  7 ++++---
 src/core/bisimulation.cpp       |  8 ++++----
 tests/core/test_bisimulation.py | 17 +++++++++++++++--
 3 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index 7893c6f..7337b65 100644
--- a/lib/stormpy/__init__.py
+++ b/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:
diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp
index 3eafc80..cdd3bf0 100644
--- a/src/core/bisimulation.cpp
+++ b/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")
diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py
index ae69462..bb69111 100644
--- a/tests/core/test_bisimulation.py
+++ b/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