Started extending DFT bindings

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

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<typename ValueType>
+std::vector<ValueType> analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC) {
+    typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results dftResults = storm::api::analyzeDFT(dft, properties, symred, allowModularisation, enableDC, false);
+    std::vector<ValueType> results;
+    for (auto result : dftResults) {
+        results.push_back(boost::get<ValueType>(result));
+    }
+    return results;
+}
+
+
+// Define python bindings
+void define_analysis(py::module& m) {
+
+    m.def("analyze_dft", &analyzeDFT<double>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred")=true, py::arg("allow_modularisation")=false, py::arg("enable_dont_care")=true);
+
+}

src/dft/analysis.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_analysis(py::module& m);

src/dft/common.h

@@ -1 +1,2 @@
 #include "src/common.h"
+#include "storm-dft/api/storm-dft.h"

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<typename ValueType>
-std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModelFromJsonDft(std::string const& jsonDft, bool symred) {
-    // Build DFT
-    storm::parser::DFTJsonParser<ValueType> parser;
-    storm::storage::DFT<ValueType> dft = parser.parseJson(jsonDft);
-    // Build model
-    std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
-    storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
-    if (symred) {
-        auto colouring = dft.colourDFT();
-        symmetries = dft.findSymmetries(colouring);
-    }
-    storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, true);
-    typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions({}, true);
-    builder.buildModel(labeloptions, 0, 0.0);
-    return builder.getModel();
-}
+
+
+template<typename ValueType> using DFT = storm::storage::DFT<ValueType>;
+
 
 void define_dft(py::module& m) {
+
     m.def("_set_up", []() {
             storm::settings::addModule<storm::settings::modules::FaultTreeSettings>();
         }, "Initialize Storm-dft");
-    // Build model
-    m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft<double>, "Build the model", py::arg("jsonDft"), py::arg("symred") = false);
-    m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft<storm::RationalFunction>, "Build the parametric model", py::arg("jsonDft"), py::arg("symred") = false);
+
+
+    // DFT class
+    py::class_<DFT<double>, std::shared_ptr<DFT<double>>>(m, "DFT", "DFT")
+        .def("nr_elements", &DFT<double>::nrElements)
+    ;
+
+    py::class_<DFT<storm::RationalFunction>, std::shared_ptr<DFT<storm::RationalFunction>>>(m, "ParametricDFT", "Parametric DFT")
+        .def("nr_elements", &DFT<storm::RationalFunction>::nrElements)
+    ;
+
 }

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_ */

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<double>, "Load DFT from Galileo file", py::arg("path"));
+    // Parse Jani model
+    m.def("load_dft_json", &storm::api::loadDFTJson<double>, "Load DFT from JSON file", py::arg("path"));
+}
+
+void define_output(py::module& m) {
+
+    // Export DFT
+    m.def("export_dft_json", &storm::api::exportDFTToJson<double>, "Export DFT to JSON file", py::arg("dft"), py::arg("path"));
+}

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);

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);
 }

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)