From ad4ce3199fa48510d61c3df5d022455f355b6f9e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 5 Oct 2018 18:12:42 +0200 Subject: [PATCH] add some variants of prism to jani --- tests/storage/test_prism.py | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/tests/storage/test_prism.py b/tests/storage/test_prism.py index 7ea3fa0..cbb9788 100644 --- a/tests/storage/test_prism.py +++ b/tests/storage/test_prism.py @@ -4,9 +4,27 @@ from helpers.helper import get_example_path import pytest class TestPrism: - def test_prism_to_jani(self): + + def test_prism_to_jani_states(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + orig_properties = stormpy.parse_properties_for_prism_program("P=? [F s=7]", program) + assert len(orig_properties) == 1 + jani_model, new_properties = program.to_jani(orig_properties) + assert len(new_properties) == len(orig_properties) + + def test_prism_to_jani_labels(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program) assert len(orig_properties) == 1 jani_model, new_properties = program.to_jani(orig_properties) assert len(new_properties) == len(orig_properties) + + + def test_prism_to_jani_repetitive(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program) + jani_model, new_properties = program.to_jani(orig_properties) + assert len(new_properties) == len(orig_properties) + orig_properties = stormpy.parse_properties_for_prism_program("P=? [F s=7]", program) + jani_model, new_properties = program.to_jani(orig_properties, suffix = "2") + assert len(new_properties) == len(orig_properties) \ No newline at end of file