diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 532f88c..bca8d35 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -99,12 +99,18 @@ class TestSparseModel: def test_build_ctmc(self): program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) - model = stormpy.build_model(program, formulas) + model = stormpy.build_model(program) assert model.nr_states == 12 assert model.nr_transitions == 22 assert model.model_type == stormpy.ModelType.CTMC assert not model.supports_parameters assert type(model) is stormpy.SparseCtmc + model_for_formula = stormpy.build_model(program, formulas) + assert model_for_formula.nr_states == 1 + assert model_for_formula.nr_transitions == 1 + assert model_for_formula.model_type == stormpy.ModelType.CTMC + assert not model_for_formula.supports_parameters + assert type(model_for_formula) is stormpy.SparseCtmc def test_build_pomdp(self): program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) @@ -115,11 +121,11 @@ class TestSparseModel: def test_build_ma(self): - program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=2 s=2 ]", program) + program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) + formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ F<=2 s=2 ]", program) model = stormpy.build_model(program, formulas) - assert model.nr_states == 5 - assert model.nr_transitions == 8 + assert model.nr_states == 4 + assert model.nr_transitions == 7 assert model.model_type == stormpy.ModelType.MA assert not model.supports_parameters assert type(model) is stormpy.SparseMA