From c7b3fae4d0d11b69944b847ac69c72f6d08bea81 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 31 May 2017 17:36:30 +0200
Subject: [PATCH] Binding for exporting into DRN format

---
 src/core/core.cpp | 18 +++++++++++++++++-
 src/core/core.h   |  1 +
 src/mod_core.cpp  |  1 +
 3 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/core/core.cpp b/src/core/core.cpp
index 0458165..4a7dcf1 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -1,4 +1,5 @@
 #include "core.h"
+#include "storm/utility/DirectEncodingExporter.h"
 
 void define_core(py::module& m) {
     // Init
@@ -60,5 +61,20 @@ void define_build(py::module& m) {
     m.def("_build_sparse_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
     m.def("_build_sparse_model_from_drn", &storm::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"));
     m.def("_build_sparse_parametric_model_from_drn", &storm::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"));
-    
+
+}
+
+// Thin wrapper for exporting model
+template<typename ValueType>
+void exportDRN(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& file) {
+     std::ofstream stream;
+    storm::utility::openFile(file, stream);
+    storm::exporter::explicitExportSparseModel(stream, model, {});
+    storm::utility::closeFile(stream);
+}
+
+void define_export(py::module& m) {
+    // Export
+    m.def("export_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"));
+    m.def("export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"));
 }
diff --git a/src/core/core.h b/src/core/core.h
index ee3b3be..b56aa28 100644
--- a/src/core/core.h
+++ b/src/core/core.h
@@ -6,5 +6,6 @@
 void define_core(py::module& m);
 void define_parse(py::module& m);
 void define_build(py::module& m);
+void define_export(py::module& m);
 
 #endif /* PYTHON_CORE_CORE_H_ */
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 8e7e507..2a557ef 100644
--- a/src/mod_core.cpp
+++ b/src/mod_core.cpp
@@ -19,6 +19,7 @@ PYBIND11_PLUGIN(core) {
     define_property(m);
     define_parse(m);
     define_build(m);
+    define_export(m);
     define_result(m);
     define_modelchecking(m);
     define_bisimulation(m);