From b913f216b426b6d79e729e28b6186891963d6d0d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 7 Apr 2017 14:03:01 +0200 Subject: [PATCH] Smaller bisimulation model which takes less time --- tests/core/test_bisimulation.py | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index 32d9d17..07e8151 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -33,29 +33,31 @@ class TestBisimulation: def test_parametric_bisimulation(self): import pycarl - program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm")) - assert program.nr_modules == 1 + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + assert program.nr_modules == 5 assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants - - prop = "P=? [F \"observe0Greater1\"]" + prop = "P=? [F s=5]" properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_parametric_model(program, properties) - assert model.nr_states == 1367 - assert model.nr_transitions == 2027 + assert model.nr_states == 613 + assert model.nr_transitions == 803 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters - result = stormpy.model_checking(model, properties[0]) initial_state = model.initial_states[0] assert initial_state == 0 + + result = stormpy.model_checking(model, properties[0]) ratFunc = result.result.at(initial_state) + 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.nr_states == 324 + assert model_bisim.nr_transitions == 452 assert model_bisim.model_type == stormpy.ModelType.DTMC assert model_bisim.has_parameters + result_bisim = stormpy.model_checking(model_bisim, properties[0]) initial_state_bisim = model_bisim.initial_states[0] - assert initial_state_bisim == 48 + assert initial_state_bisim == 316 ratFunc_bisim = result_bisim.result.at(initial_state_bisim) assert ratFunc == ratFunc_bisim