From 3606edfa963ef12b684a7375068551adf02e8b1c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 5 Aug 2019 10:01:32 +0200 Subject: [PATCH] Test for symbolic parametric bisimulation --- tests/core/test_bisimulation.py | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index b16ccc2..5dad419 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -75,4 +75,19 @@ 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 \ No newline at end of file + assert ratFunc == ratFunc_bisim + + def test_symbolic_parametric_bisimulation(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F \"error\"]" + properties = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_symbolic_parametric_model(program, properties) + assert model.nr_states == 613 + assert model.nr_transitions == 803 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + model_bisim = stormpy.perform_symbolic_bisimulation(model, properties) + assert model_bisim.nr_states == 326 + assert model_bisim.nr_transitions == 454 + assert model_bisim.model_type == stormpy.ModelType.DTMC + assert model_bisim.has_parameters