Bisimulation

Former-commit-id: e8cb047c3a

stormpy/lib/stormpy/__init__.py

@@ -28,3 +28,9 @@ def build_parametric_model(program, formulae):
              raise RuntimeError("Not supported parametric model constructed")
     else:
         raise RuntimeError("Model should be parametric")
+
+def perform_bisimulation(model, formula, bisimulation_type):
+    if model.parametric():
+        return core._perform_parametric_bisimulation(model, formula, bisimulation_type)
+    else:
+        return core._perform_bisimulation(model, formula, bisimulation_type)

stormpy/src/core/bisimulation.cpp

@@ -10,8 +10,8 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std
 void define_bisimulation(py::module& m) {
 
     // Bisimulation
-    m.def("perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type"));
-    m.def("perform_parametric_bisimulation", &performBisimulation<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type"));
+    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"));
 
     // BisimulationType 
     py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")

stormpy/tests/core/test_bisimulation.py

@@ -33,7 +33,7 @@ class TestBisimulation:
         assert model.nr_transitions() == 2027
         assert model.model_type() == stormpy.ModelType.DTMC
         assert model.parametric()
-        model_bisim = stormpy.perform_parametric_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
+        model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
         assert model_bisim.nr_states() == 80
         assert model_bisim.nr_transitions() == 120
         assert model_bisim.model_type() == stormpy.ModelType.DTMC