diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py index 1a8fb8fe4..0edb49ffc 100644 --- a/stormpy/tests/core/test_bisimulation.py +++ b/stormpy/tests/core/test_bisimulation.py @@ -21,7 +21,7 @@ class TestBisimulation: assert not model_bisim.supports_parameters() def test_parametric_bisimulation(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds", "crowds_3-5.pm")) + program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds", "crowds3_5.pm")) assert program.nr_modules() == 1 assert program.model_type() == stormpy.PrismModelType.DTMC assert program.has_undefined_constants() diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py index d6033b1c3..0b692df69 100644 --- a/stormpy/tests/core/test_modelchecking.py +++ b/stormpy/tests/core/test_modelchecking.py @@ -25,8 +25,8 @@ class TestModelChecking: def test_parametric_state_elimination(self): import pycarl import pycarl.formula - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm")) - prop = "P=? [F \"target\"]" + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) + prop = "P=? [F s=5]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_parametric_model_from_prism_program(program, formulas) assert model.nr_states() == 613 diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py index 3cc3a5a16..8e8c98a47 100644 --- a/stormpy/tests/storage/test_matrix.py +++ b/stormpy/tests/storage/test_matrix.py @@ -68,8 +68,8 @@ class TestMatrix: def test_change_parametric_sparse_matrix_modelchecking(self): import stormpy.logic import pycarl - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program) + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) + formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas[0]) matrix = model.transition_matrix() # Check matrix diff --git a/stormpy/tests/storage/test_model.py b/stormpy/tests/storage/test_model.py index df50c6f31..493e21e5e 100644 --- a/stormpy/tests/storage/test_model.py +++ b/stormpy/tests/storage/test_model.py @@ -15,11 +15,11 @@ class TestModel: assert type(model) is stormpy.SparseDtmc def test_build_parametric_dtmc_from_prism_program(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm")) + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) assert program.nr_modules() == 5 assert program.model_type() == stormpy.PrismModelType.DTMC assert program.has_undefined_constants() - prop = "P=? [F \"target\"]" + prop = "P=? [F s=5]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_parametric_model_from_prism_program(program, formulas) assert model.nr_states() == 613 @@ -40,8 +40,8 @@ class TestModel: assert type(model) is stormpy.SparseDtmc def test_build_parametric_dtmc(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program) + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) + formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas[0]) assert model.nr_states() == 613 assert model.nr_transitions() == 803 @@ -81,16 +81,16 @@ class TestModel: assert 0 in initial_states def test_label_parametric(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program) + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) + formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas[0]) labels = model.labels() assert len(labels) == 3 assert "init" in labels - assert "target" in labels + assert "(s = 5)" in labels assert "init" in model.labels_state(0) - assert "target" in model.labels_state(28) - assert "target" in model.labels_state(611) + assert "(s = 5)" in model.labels_state(28) + assert "(s = 5)" in model.labels_state(611) initial_states = model.initial_states() assert len(initial_states) == 1 assert 0 in initial_states