diff --git a/CHANGELOG.md b/CHANGELOG.md index d5e60a5..0e51bc5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,7 @@ Requires storm version >= 1.2.2 and pycarl version >= 2.0.2 * transforming symbolic to sparse models - Extraction of schedulers and queries on schedulers - Extended PLA bindings +- Extended DFT bindings - Extended documentation ### Version 1.2.0 diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp new file mode 100644 index 0000000..3edbdf4 --- /dev/null +++ b/src/dft/analysis.cpp @@ -0,0 +1,25 @@ +#include "analysis.h" + +#include "storm-dft/parser/DFTJsonParser.h" +#include "storm-dft/builder/ExplicitDFTModelBuilder.h" +#include "storm-dft/storage/dft/DFTIsomorphism.h" + + +// Thin wrapper for DFT analysis +template +std::vector analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred, bool allowModularisation, bool enableDC) { + typename storm::modelchecker::DFTModelChecker::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, enableDC, false); + std::vector results; + for (auto result : dftResults) { + results.push_back(boost::get(result)); + } + return results; +} + + +// Define python bindings +void define_analysis(py::module& m) { + + m.def("analyze_dft", &analyzeDFT, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("enable_dont_care")=true); + +} diff --git a/src/dft/analysis.h b/src/dft/analysis.h new file mode 100644 index 0000000..102b3b9 --- /dev/null +++ b/src/dft/analysis.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_analysis(py::module& m); diff --git a/src/dft/common.h b/src/dft/common.h index c9b9b0c..2de6bc0 100644 --- a/src/dft/common.h +++ b/src/dft/common.h @@ -1 +1,2 @@ #include "src/common.h" +#include "storm-dft/api/storm-dft.h" \ No newline at end of file diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp index ccd2465..c9c06a4 100644 --- a/src/dft/dft.cpp +++ b/src/dft/dft.cpp @@ -1,34 +1,27 @@ #include "dft.h" -#include "storm-dft/parser/DFTJsonParser.h" -#include "storm-dft/builder/ExplicitDFTModelBuilder.h" +#include "src/helpers.h" +#include "storm-dft/storage/dft/DFT.h" #include "storm/settings/SettingsManager.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" -#include "storm-dft/storage/dft/DFTIsomorphism.h" - -// Thin wrapper for model building using one formula as argument -template -std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft, bool symred) { - // Build DFT - storm::parser::DFTJsonParser parser; - storm::storage::DFT dft = parser.parseJson(jsonDft); - // Build model - std::map>> emptySymmetry; - storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); - if (symred) { - auto colouring = dft.colourDFT(); - symmetries = dft.findSymmetries(colouring); - } - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, true); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions({}, true); - builder.buildModel(labeloptions, 0, 0.0); - return builder.getModel(); -} + + +template using DFT = storm::storage::DFT; + void define_dft(py::module& m) { + m.def("_set_up", []() { storm::settings::addModule(); }, "Initialize Storm-dft"); - // Build model - m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft"), py::arg("symred") = false); - m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft"), py::arg("symred") = false); + + + // DFT class + py::class_, std::shared_ptr>>(m, "DFT", "DFT") + .def("nr_elements", &DFT::nrElements) + ; + + py::class_, std::shared_ptr>>(m, "ParametricDFT", "Parametric DFT") + .def("nr_elements", &DFT::nrElements) + ; + } diff --git a/src/dft/dft.h b/src/dft/dft.h index 2dc129a..147b75a 100644 --- a/src/dft/dft.h +++ b/src/dft/dft.h @@ -1,8 +1,5 @@ -#ifndef PYTHON_DFT_DFT_H_ -#define PYTHON_DFT_DFT_H_ +#pragma once #include "common.h" void define_dft(py::module& m); - -#endif /* PYTHON_DFT_DFT_H_ */ diff --git a/src/dft/io.cpp b/src/dft/io.cpp new file mode 100644 index 0000000..6c56334 --- /dev/null +++ b/src/dft/io.cpp @@ -0,0 +1,18 @@ +#include "io.h" +#include "src/helpers.h" + + +// Define python bindings +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")); + // Parse Jani model + m.def("load_dft_json", &storm::api::loadDFTJson, "Load DFT from JSON file", py::arg("path")); +} + +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")); +} diff --git a/src/dft/io.h b/src/dft/io.h new file mode 100644 index 0000000..663b9e3 --- /dev/null +++ b/src/dft/io.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +void define_input(py::module& m); +void define_output(py::module& m); diff --git a/src/mod_dft.cpp b/src/mod_dft.cpp index 4d840eb..315cc7c 100644 --- a/src/mod_dft.cpp +++ b/src/mod_dft.cpp @@ -1,6 +1,8 @@ #include "common.h" #include "dft/dft.h" +#include "dft/io.h" +#include "dft/analysis.h" PYBIND11_MODULE(dft, m) { m.doc() = "Functionality for DFT analysis"; @@ -11,4 +13,7 @@ PYBIND11_MODULE(dft, m) { #endif define_dft(m); + define_input(m); + define_output(m); + define_analysis(m); } diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py index e09bc66..09fcc3f 100644 --- a/tests/dft/test_build.py +++ b/tests/dft/test_build.py @@ -9,12 +9,8 @@ from configurations import dft @dft class TestBuild: def test_build_dft(self): - model = stormpy.dft.build_sparse_model_from_json_dft(get_example_path("dft", "and.json")) + dft = stormpy.dft.load_dft_json(get_example_path("dft", "and.json")) formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") - assert model.nr_states == 4 - assert model.nr_transitions == 5 - assert len(model.initial_states) == 1 - initial_state = model.initial_states[0] - assert initial_state == 1 - result = stormpy.model_checking(model, formulas[0]) - assert math.isclose(result.at(initial_state), 3) + assert dft.nr_elements() == 3 + results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) + assert math.isclose(results[0], 3)