From 2ac480555452affe235eeb77b13458cc33eca035 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 7 Feb 2020 15:20:31 +0100
Subject: [PATCH] added options for the DRN parser, reflects recent changes in
 storm

---
 lib/stormpy/__init__.py | 10 ++++++----
 src/core/core.cpp       | 10 ++++++++--
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index 376a941..039b11b 100644
--- a/lib/stormpy/__init__.py
+++ b/lib/stormpy/__init__.py
@@ -189,25 +189,27 @@ def build_symbolic_parametric_model(symbolic_description, properties=None):
     return _convert_symbolic_model(intermediate, parametric=True)
 
 
-def build_model_from_drn(file):
+def build_model_from_drn(file, options = DirectEncodingParserOptions()):
     """
     Build a model in sparse representation from the explicit DRN representation.
 
     :param String file: DRN file containing the model.
+    :param DirectEncodingParserOptions: Options for the parser.
     :return: Model in sparse representation.
     """
-    intermediate = core._build_sparse_model_from_drn(file)
+    intermediate = core._build_sparse_model_from_drn(file, options)
     return _convert_sparse_model(intermediate, parametric=False)
 
 
-def build_parametric_model_from_drn(file):
+def build_parametric_model_from_drn(file, options = DirectEncodingParserOptions()):
     """
     Build a parametric model in sparse representation from the explicit DRN representation.
 
     :param String file: DRN file containing the model.
+    :param DirectEncodingParserOptions: Options for the parser.
     :return: Parametric model in sparse representation.
     """
-    intermediate = core._build_sparse_parametric_model_from_drn(file)
+    intermediate = core._build_sparse_parametric_model_from_drn(file, options)
     return _convert_sparse_model(intermediate, parametric=True)
 
 
diff --git a/src/core/core.cpp b/src/core/core.cpp
index b1619fe..e17473f 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -94,6 +94,11 @@ std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> buildSymbolic
 }
 
 void define_build(py::module& m) {
+
+    py::class_<storm::parser::DirectEncodingParserOptions>(m, "DirectEncodingParserOptions", "Options for the .drn parser")
+            .def(py::init<>(), "initialise")
+            .def_readwrite("build_choice_labels", &storm::parser::DirectEncodingParserOptions::buildChoiceLabeling, "Build with choice labels");
+
     // Build model
     m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
     m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
@@ -101,8 +106,8 @@ void define_build(py::module& m) {
     m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions<storm::RationalFunction>, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"), py::arg("use_jit") = false, py::arg("doctor") = false);
     m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, double>, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
-    m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"));
-    m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"));
+    m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
+    m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
 
 
@@ -114,6 +119,7 @@ void define_build(py::module& m) {
             .def("set_build_with_choice_origins", &storm::builder::BuilderOptions::setBuildChoiceOrigins, "Build choice origins", py::arg("new_value")=true)
             .def("set_add_out_of_bounds_state", &storm::builder::BuilderOptions::setAddOutOfBoundsState, "Build with out of bounds state", py::arg("new_value")=true)
             .def("set_add_overlapping_guards_label", &storm::builder::BuilderOptions::setAddOverlappingGuardsLabel, "Build with overlapping guards state labeled", py::arg("new_value")=true);
+
 }
 
 void define_optimality_type(py::module& m) {