From 1308fe2e931e3b6b426a4b53f98c28b8e3665899 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 8 Aug 2018 13:48:00 +0200 Subject: [PATCH] Changes according to DFT loading in Storm --- doc/source/doc/dfts.rst | 8 +++++--- examples/dfts/01-dfts.py | 4 ++-- src/dft/io.cpp | 8 +++++--- tests/dft/test_build.py | 6 +++--- 4 files changed, 15 insertions(+), 11 deletions(-) diff --git a/doc/source/doc/dfts.rst b/doc/source/doc/dfts.rst index c143a2d..d46d821 100644 --- a/doc/source/doc/dfts.rst +++ b/doc/source/doc/dfts.rst @@ -7,7 +7,9 @@ Building DFTs ============= .. seealso:: `01-dfts.py `_ -Dynamic fault trees can be loaded from either the Galileo format via ``load_dft_json(path)`` or from a custom JSON format via ``load_dft_galileo(path)``. +Dynamic fault trees can be loaded from either the Galileo format or from a custom JSON form. +A file containing the DFT in the Galileo format can be loaded via ``load_dft_galileo_file(path)``. +The custom JSON format can be loaded from a file via ``load_dft_json_file(path)`` or directly from a string via ``load_dft_json_string(path)``. We start by loading a simple DFT containing an AND gate from JSON:: >>> import stormpy @@ -15,14 +17,14 @@ We start by loading a simple DFT containing an AND gate from JSON:: >>> import stormpy.examples >>> import stormpy.examples.files >>> path_json = stormpy.examples.files.dft_json_and - >>> dft_small = stormpy.dft.load_dft_json(path_json) + >>> dft_small = stormpy.dft.load_dft_json_file(path_json) >>> print(dft_small) Top level index: 2, Nr BEs2 Next we load a more complex DFT from the Galileo format:: >>> path_galileo = stormpy.examples.files.dft_galileo_hecs - >>> dft = stormpy.dft.load_dft_galileo(path_galileo) + >>> dft = stormpy.dft.load_dft_galileo_file(path_galileo) After loading the DFT, we can display some common statistics about the model:: diff --git a/examples/dfts/01-dfts.py b/examples/dfts/01-dfts.py index 691d150..160c975 100644 --- a/examples/dfts/01-dfts.py +++ b/examples/dfts/01-dfts.py @@ -8,12 +8,12 @@ import stormpy.examples.files def example_dfts_01(): # Load from JSON path_json = stormpy.examples.files.dft_json_and - dft_small = stormpy.dft.load_dft_json(path_json) + dft_small = stormpy.dft.load_dft_json_file(path_json) print(dft_small) # Load from Galileo path = stormpy.examples.files.dft_galileo_hecs - dft = stormpy.dft.load_dft_galileo(path) + dft = stormpy.dft.load_dft_galileo_file(path) print("DFT with {} elements.".format(dft.nr_elements())) print("DFT has {} BEs and {} dynamic elements.".format(dft.nr_be(), dft.nr_dynamic())) diff --git a/src/dft/io.cpp b/src/dft/io.cpp index 6c56334..38526d9 100644 --- a/src/dft/io.cpp +++ b/src/dft/io.cpp @@ -6,13 +6,15 @@ void define_input(py::module& m) { // Load DFT input - m.def("load_dft_galileo", &storm::api::loadDFTGalileo, "Load DFT from Galileo file", py::arg("path")); + m.def("load_dft_galileo_file", &storm::api::loadDFTGalileoFile, "Load DFT from Galileo file", py::arg("path")); // Parse Jani model - m.def("load_dft_json", &storm::api::loadDFTJson, "Load DFT from JSON file", py::arg("path")); + m.def("load_dft_json_file", &storm::api::loadDFTJsonFile, "Load DFT from JSON file", py::arg("path")); + m.def("load_dft_json_string", &storm::api::loadDFTJsonString, "Load DFT from JSON string", py::arg("json_string")); } void define_output(py::module& m) { // Export DFT - m.def("export_dft_json", &storm::api::exportDFTToJson, "Export DFT to JSON file", py::arg("dft"), py::arg("path")); + m.def("export_dft_json_file", &storm::api::exportDFTToJsonFile, "Export DFT to JSON file", py::arg("dft"), py::arg("path")); + m.def("export_dft_json_string", &storm::api::exportDFTToJsonString, "Export DFT to JSON string", py::arg("dft")); } diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py index d9a84fe..4a3ba51 100644 --- a/tests/dft/test_build.py +++ b/tests/dft/test_build.py @@ -9,21 +9,21 @@ from configurations import dft @dft class TestBuild: def test_load_dft_json(self): - dft = stormpy.dft.load_dft_json(get_example_path("dft", "and.json")) + 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(get_example_path("dft", "hecs.dft")) + 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(get_example_path("dft", "and.json")) + 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])