From 64c663a809100c489296e335abba56a995232b2c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 6 Mar 2017 16:57:26 +0100 Subject: [PATCH] Started with Python bindings for storm-dft --- CMakeLists.txt | 5 +- lib/stormpy/dft/__init__.py | 4 ++ lib/stormpy/examples/files/dft/and.json | 71 +++++++++++++++++++++++++ setup.py | 5 +- src/dft/common.h | 1 + src/dft/dft.cpp | 29 ++++++++++ src/dft/dft.h | 8 +++ src/mod_dft.cpp | 15 ++++++ tests/dft/test_build.py | 19 +++++++ 9 files changed, 153 insertions(+), 4 deletions(-) create mode 100644 lib/stormpy/dft/__init__.py create mode 100644 lib/stormpy/examples/files/dft/and.json create mode 100644 src/dft/common.h create mode 100644 src/dft/dft.cpp create mode 100644 src/dft/dft.h create mode 100644 src/mod_dft.cpp create mode 100644 tests/dft/test_build.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ec1761..3183182 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/lib/stormpy/dft/__init__.py b/lib/stormpy/dft/__init__.py new file mode 100644 index 0000000..ae53cc2 --- /dev/null +++ b/lib/stormpy/dft/__init__.py @@ -0,0 +1,4 @@ +from . import dft +from .dft import * + +dft._set_up() diff --git a/lib/stormpy/examples/files/dft/and.json b/lib/stormpy/examples/files/dft/and.json new file mode 100644 index 0000000..ce62b7f --- /dev/null +++ b/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" + } + ] +} \ No newline at end of file diff --git a/setup.py b/setup.py index 5ab038a..2188718 100755 --- a/setup.py +++ b/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, diff --git a/src/dft/common.h b/src/dft/common.h new file mode 100644 index 0000000..c9b9b0c --- /dev/null +++ b/src/dft/common.h @@ -0,0 +1 @@ +#include "src/common.h" diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp new file mode 100644 index 0000000..4c2ca64 --- /dev/null +++ b/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 +std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft) { + // Build DFT + storm::parser::DFTJsonParser parser; + storm::storage::DFT dft = parser.parseJson(jsonDft); + // Build model + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, true); + typename storm::builder::ExplicitDFTModelBuilderApprox::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(); + }, "Initialize Storm-dft"); + // Build model + m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft")); + m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft")); +} diff --git a/src/dft/dft.h b/src/dft/dft.h new file mode 100644 index 0000000..2dc129a --- /dev/null +++ b/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_ */ diff --git a/src/mod_dft.cpp b/src/mod_dft.cpp new file mode 100644 index 0000000..b6a8d41 --- /dev/null +++ b/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(); +} diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py new file mode 100644 index 0000000..059b027 --- /dev/null +++ b/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) +