From 22053e63a918ac2b147a2b9d2f1bab1533fd0003 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 12 May 2016 19:11:14 +0200 Subject: [PATCH] Bisimulation Former-commit-id: e8cb047c3a9f40f2e37441ab1bd92b03d2b51e48 --- stormpy/lib/stormpy/__init__.py | 6 ++++++ stormpy/src/core/bisimulation.cpp | 4 ++-- stormpy/tests/core/test_bisimulation.py | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index 721810266..325d23a6f 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/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) diff --git a/stormpy/src/core/bisimulation.cpp b/stormpy/src/core/bisimulation.cpp index 240c8b1c8..3eafc80d0 100644 --- a/stormpy/src/core/bisimulation.cpp +++ b/stormpy/src/core/bisimulation.cpp @@ -10,8 +10,8 @@ std::shared_ptr> performBisimulation(std void define_bisimulation(py::module& m) { // Bisimulation - m.def("perform_bisimulation", &performBisimulation, "Perform bisimulation", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type")); - m.def("perform_parametric_bisimulation", &performBisimulation, "Perform bisimulation on parametric model", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type")); + m.def("_perform_bisimulation", &performBisimulation, "Perform bisimulation", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type")); + m.def("_perform_parametric_bisimulation", &performBisimulation, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type")); // BisimulationType py::enum_(m, "BisimulationType", "Types of bisimulation") diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py index 17c5fa706..2bd9bd974 100644 --- a/stormpy/tests/core/test_bisimulation.py +++ b/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