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> buildSymbolic } void define_build(py::module& m) { + + py::class_(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, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), 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, "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, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); - m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); - m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); + m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "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, "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, "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) {