From 1c4e589a11413edca343b1b6ccfd218e9b71282b Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 8 Aug 2018 15:10:31 +0200
Subject: [PATCH] I/O tests for DFTs

---
 tests/dft/test_analysis.py | 17 +++++++++++
 tests/dft/test_build.py    | 30 ------------------
 tests/dft/test_io.py       | 62 ++++++++++++++++++++++++++++++++++++++
 3 files changed, 79 insertions(+), 30 deletions(-)
 create mode 100644 tests/dft/test_analysis.py
 delete mode 100644 tests/dft/test_build.py
 create mode 100644 tests/dft/test_io.py

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