From 7342428c5e394e987715c48b51ca396aecfdece6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Mar 2017 18:08:47 +0200 Subject: [PATCH] Improved bisimulation test --- tests/core/test_bisimulation.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index a30b123..6959e6b 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -16,12 +16,18 @@ 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): program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm"))