From 56ba8685d5854ceb85b36a3ce39504cb2f1c4d3a Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Mon, 2 Jan 2017 20:40:42 +0100 Subject: [PATCH] extract parametric prism program parse test --- tests/core/test_parse.py | 8 +++++++- tests/storage/test_model.py | 3 --- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 8646beb..139d145 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -9,7 +9,13 @@ class TestParse: assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC assert not program.has_undefined_constants - + + def test_parse_parametric_prism_program(self): + 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 + def test_parse_formula(self): formula = "P=? [F \"one\"]" properties = stormpy.parse_properties(formula) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 2b68655..21dbb63 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -26,9 +26,6 @@ class TestModel: def test_build_parametric_dtmc_from_prism_program(self): 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 s=5]" formulas = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_parametric_model(program, formulas)