From 0e7a194f5bab03564338bb0bc605ff569bad4d81 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 4 Oct 2018 22:39:27 +0200 Subject: [PATCH 1/3] support for chaning the build_temp folder --- setup.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/setup.py b/setup.py index 9475487..48068e8 100755 --- a/setup.py +++ b/setup.py @@ -34,7 +34,7 @@ class CMakeBuild(build_ext): ('disable-dft', None, 'Disable support for DFTs'), ('disable-pars', None, 'Disable support for parametric models'), ('debug', None, 'Build in Debug mode'), - ('jobs=', 'j', 'Number of jobs to use for compiling'), + ('jobs=', 'j', 'Number of jobs to use for compiling') ] config = SetupConfig() @@ -50,12 +50,13 @@ class CMakeBuild(build_ext): ", ".join(e.name for e in self.extensions)) # Build cmake version info + print("Stormpy - Building into {}".format(self.build_temp)) build_temp_version = self.build_temp + "-version" setup_helper.ensure_dir_exists(build_temp_version) # Write config - setup_helper.ensure_dir_exists("build") - self.config.write_config("build/build_config.cfg") + setup_helper.ensure_dir_exists(self.build_temp) + self.config.write_config(os.path.join(self.build_temp, "build_config.cfg")) cmake_args = [] storm_dir = os.path.expanduser(self.config.get_as_string("storm_dir")) From 19677815271fcf510b628091a9d46cc9be8a741e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 5 Oct 2018 17:48:37 +0200 Subject: [PATCH 2/3] add (failing) prism to jani test --- tests/storage/test_prism.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/storage/test_prism.py diff --git a/tests/storage/test_prism.py b/tests/storage/test_prism.py new file mode 100644 index 0000000..7ea3fa0 --- /dev/null +++ b/tests/storage/test_prism.py @@ -0,0 +1,12 @@ +import stormpy +import stormpy.logic +from helpers.helper import get_example_path +import pytest + +class TestPrism: + def test_prism_to_jani(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) From ad4ce3199fa48510d61c3df5d022455f355b6f9e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 5 Oct 2018 18:12:42 +0200 Subject: [PATCH 3/3] 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