Browse Source

extract parametric prism program parse test

refactoring
Tom Janson 8 years ago
parent
commit
56ba8685d5
  1. 8
      tests/core/test_parse.py
  2. 3
      tests/storage/test_model.py

8
tests/core/test_parse.py

@ -9,7 +9,13 @@ class TestParse:
assert program.nr_modules == 1 assert program.nr_modules == 1
assert program.model_type == stormpy.PrismModelType.DTMC assert program.model_type == stormpy.PrismModelType.DTMC
assert not program.has_undefined_constants 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): def test_parse_formula(self):
formula = "P=? [F \"one\"]" formula = "P=? [F \"one\"]"
properties = stormpy.parse_properties(formula) properties = stormpy.parse_properties(formula)

3
tests/storage/test_model.py

@ -26,9 +26,6 @@ class TestModel:
def test_build_parametric_dtmc_from_prism_program(self): def test_build_parametric_dtmc_from_prism_program(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) 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]" prop = "P=? [F s=5]"
formulas = stormpy.parse_properties_for_prism_program(prop, program) formulas = stormpy.parse_properties_for_prism_program(prop, program)
model = stormpy.build_parametric_model(program, formulas) model = stormpy.build_parametric_model(program, formulas)

Loading…
Cancel
Save