Started with Python bindings for storm-dft

CMakeLists.txt

@@ -23,8 +23,8 @@ function(stormpy_module NAME)
 
     file(GLOB_RECURSE "STORM_${NAME}_SOURCES" "${CMAKE_CURRENT_SOURCE_DIR}/src/${NAME}/*.cpp")
     pybind11_add_module(${NAME} "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_${NAME}.cpp" ${STORM_${NAME}_SOURCES})
-    target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/generated)
-    target_link_libraries(${NAME} PRIVATE storm)
+    target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${storm-dft_INCLUDE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/generated)
+    target_link_libraries(${NAME} PRIVATE storm storm-dft)
 
     # setup.py will override this (because pip may want a different install
     # path), but also specifying it here has the advantage that invoking cmake
@@ -40,3 +40,4 @@ stormpy_module(expressions)
 stormpy_module(logic)
 stormpy_module(storage)
 stormpy_module(utility)
+stormpy_module(dft)

lib/stormpy/dft/__init__.py

@@ -0,0 +1,4 @@
+from . import dft
+from .dft import *
+
+dft._set_up()

lib/stormpy/examples/files/dft/and.json

@@ -0,0 +1,71 @@
+{
+    "toplevel": "2",
+    "parameters": {},
+    "nodes": [
+        {
+            "data": {
+                "id": "0",
+                "name": "B",
+                "type": "be",
+                "rate": "0.5",
+                "dorm": "1",
+                "label": "B (0.5)"
+            },
+            "position": {
+                "x": 426,
+                "y": 142
+            },
+            "group": "nodes",
+            "removed": false,
+            "selected": false,
+            "selectable": true,
+            "locked": false,
+            "grabbable": true,
+            "classes": "be"
+        },
+        {
+            "data": {
+                "id": "1",
+                "name": "C",
+                "type": "be",
+                "rate": "0.5",
+                "dorm": "1",
+                "label": "C (0.5)"
+            },
+            "position": {
+                "x": 598,
+                "y": 139
+            },
+            "group": "nodes",
+            "removed": false,
+            "selected": false,
+            "selectable": true,
+            "locked": false,
+            "grabbable": true,
+            "classes": "be"
+        },
+        {
+            "data": {
+                "id": "2",
+                "name": "A",
+                "type": "and",
+                "children": [
+                    "0",
+                    "1"
+                ],
+                "label": "A"
+            },
+            "position": {
+                "x": 503,
+                "y": 42
+            },
+            "group": "nodes",
+            "removed": false,
+            "selected": false,
+            "selectable": true,
+            "locked": false,
+            "grabbable": true,
+            "classes": "and toplevel"
+        }
+    ]
+}

setup.py

@@ -81,7 +81,7 @@ setup(
     maintainer_email="sebastian.junges@cs.rwth-aachen.de",
     url="http://moves.rwth-aachen.de",
     description="stormpy - Python Bindings for Storm",
-    packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility'],
+    packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', 'stormpy.dft'],
     package_dir={'': 'lib'},
     ext_package='stormpy',
     ext_modules=[CMakeExtension('core', subdir=''),
@@ -89,7 +89,8 @@ setup(
                  CMakeExtension('expressions', subdir='expressions'),
                  CMakeExtension('logic', subdir='logic'),
                  CMakeExtension('storage', subdir='storage'),
-                 CMakeExtension('utility', subdir='utility')
+                 CMakeExtension('utility', subdir='utility'),
+                 CMakeExtension('dft', subdir='dft')
                  ],
     cmdclass=dict(build_ext=CMakeBuild, test=PyTest),
     zip_safe=False,

src/dft/common.h

@@ -0,0 +1 @@
+#include "src/common.h"

src/dft/dft.cpp

@@ -0,0 +1,29 @@
+#include "dft.h"
+#include "storm-dft/parser/DFTJsonParser.h"
+#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm-dft/settings/modules/DFTSettings.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) {
+    // 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);
+    storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, true);
+    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions({}, true);
+    builder.buildModel(labeloptions, 0, 0.0);
+    return builder.getModel();
+}
+
+void define_dft(py::module& m) {
+    m.def("_set_up", []() {
+            storm::settings::addModule<storm::settings::modules::DFTSettings>();
+        }, "Initialize Storm-dft");
+    // Build model
+    m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft<double>, "Build the model", py::arg("jsonDft"));
+    m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft<storm::RationalFunction>, "Build the parametric model", py::arg("jsonDft"));
+}

src/dft/dft.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_DFT_DFT_H_
+#define PYTHON_DFT_DFT_H_
+
+#include "common.h"
+
+void define_dft(py::module& m);
+
+#endif /* PYTHON_DFT_DFT_H_ */

src/mod_dft.cpp

@@ -0,0 +1,15 @@
+#include "common.h"
+
+#include "dft/dft.h"
+
+PYBIND11_PLUGIN(dft) {
+    py::module m("dft", "Functionality for DFT analysis");
+
+#ifdef STORMPY_DISABLE_SIGNATURE_DOC
+    py::options options;
+    options.disable_function_signatures();
+#endif
+    
+    define_dft(m);
+    return m.ptr();
+}

tests/dft/test_build.py

@@ -0,0 +1,19 @@
+import stormpy
+import stormpy.dft
+import stormpy.logic
+from helpers.helper import get_example_path
+
+import math
+
+class TestBuild:
+    def test_build_dft(self):
+        model = stormpy.dft.build_sparse_model_from_json_dft(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 == 0
+        result = stormpy.model_checking(model, formulas[0])
+        assert math.isclose(result.at(initial_state), 3)
+