diff --git a/tests/dft/test_analysis.py b/tests/dft/test_analysis.py new file mode 100644 index 0000000..1028676 --- /dev/null +++ b/tests/dft/test_analysis.py @@ -0,0 +1,17 @@ +import stormpy +import stormpy.logic +from helpers.helper import get_example_path + +import math +from configurations import dft + + +@dft +class TestAnalysis: + + def test_analyze_mttf(self): + dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) + formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + assert dft.nr_elements() == 3 + results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) + assert math.isclose(results[0], 3) diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py deleted file mode 100644 index 4a3ba51..0000000 --- a/tests/dft/test_build.py +++ /dev/null @@ -1,30 +0,0 @@ -import stormpy -import stormpy.logic -from helpers.helper import get_example_path - -import math -from configurations import dft - - -@dft -class TestBuild: - def test_load_dft_json(self): - dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) - assert dft.nr_elements() == 3 - assert dft.nr_be() == 2 - assert dft.nr_dynamic() == 0 - assert not dft.can_have_nondeterminism() - - def test_load_dft_galileo(self): - dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft")) - assert dft.nr_elements() == 23 - assert dft.nr_be() == 13 - assert dft.nr_dynamic() == 2 - assert not dft.can_have_nondeterminism() - - def test_analyze_mttf(self): - dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) - formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") - assert dft.nr_elements() == 3 - results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) - assert math.isclose(results[0], 3) diff --git a/tests/dft/test_io.py b/tests/dft/test_io.py new file mode 100644 index 0000000..33a8149 --- /dev/null +++ b/tests/dft/test_io.py @@ -0,0 +1,62 @@ +import os + +import stormpy +import stormpy.logic +from helpers.helper import get_example_path + +from configurations import dft + + +@dft +class TestDftLoad: + def test_load_dft_galileo_file(self): + dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft")) + assert dft.nr_elements() == 23 + assert dft.nr_be() == 13 + assert dft.nr_dynamic() == 2 + assert not dft.can_have_nondeterminism() + + def test_load_dft_json_file(self): + dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) + assert dft.nr_elements() == 3 + assert dft.nr_be() == 2 + assert dft.nr_dynamic() == 0 + assert not dft.can_have_nondeterminism() + + def test_load_dft_json_string(self): + # Build json string + json_node_a = '{"data": {"id":"0", "name":"A", "type":"be", "rate":"1", "dorm":"1", "label":"A (1)"}, "group":"nodes", "classes":"be"}' + json_node_b = '{"data": {"id":"1", "name":"B", "type":"be", "rate":"1", "dorm":"1", "label":"B (1)"}, "group":"nodes", "classes":"be"}' + json_node_c = '{"data": {"id":"6", "name":"Z", "type":"pand", "children":["0", "1"], "label":"Z"}, "group":"nodes", "classes":"pand"}' + json_string = '{"toplevel": "6", "parameters": {}, "nodes": [' + json_node_a + ',' + json_node_b + ',' + json_node_c + ']}' + # Load + dft = stormpy.dft.load_dft_json_string(json_string) + assert dft.nr_elements() == 3 + assert dft.nr_be() == 2 + assert dft.nr_dynamic() == 1 + assert not dft.can_have_nondeterminism() + + +class TestDftExport: + def test_export_dft_json_string(self): + dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft")) + assert dft.nr_elements() == 23 + assert dft.nr_be() == 13 + assert dft.nr_dynamic() == 2 + json_string = stormpy.dft.export_dft_json_string(dft) + dft2 = stormpy.dft.load_dft_json_string(json_string) + assert dft2.nr_elements() == 23 + assert dft2.nr_be() == 13 + assert dft2.nr_dynamic() == 2 + + def test_export_dft_json_file(self, tmpdir): + dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft")) + assert dft.nr_elements() == 23 + assert dft.nr_be() == 13 + assert dft.nr_dynamic() == 2 + export_file = os.path.join(str(tmpdir), "hecs.json") + stormpy.dft.export_dft_json_file(dft, export_file) + dft2 = stormpy.dft.load_dft_json_file(export_file) + assert dft2.nr_elements() == 23 + assert dft2.nr_be() == 13 + assert dft2.nr_dynamic() == 2