|
@ -16,12 +16,18 @@ class TestBisimulation: |
|
|
assert model.nr_transitions == 13041 |
|
|
assert model.nr_transitions == 13041 |
|
|
assert model.model_type == stormpy.ModelType.DTMC |
|
|
assert model.model_type == stormpy.ModelType.DTMC |
|
|
assert not model.supports_parameters |
|
|
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_states == 64 |
|
|
assert model_bisim.nr_transitions == 104 |
|
|
assert model_bisim.nr_transitions == 104 |
|
|
assert model_bisim.model_type == stormpy.ModelType.DTMC |
|
|
assert model_bisim.model_type == stormpy.ModelType.DTMC |
|
|
assert not model_bisim.supports_parameters |
|
|
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): |
|
|
def test_parametric_bisimulation(self): |
|
|
program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm")) |
|
|
program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm")) |
|
|