Browse Source

added options for the DRN parser, reflects recent changes in storm

refactoring
Sebastian Junges 5 years ago
parent
commit
2ac4805554
  1. 10
      lib/stormpy/__init__.py
  2. 10
      src/core/core.cpp

10
lib/stormpy/__init__.py

@ -189,25 +189,27 @@ def build_symbolic_parametric_model(symbolic_description, properties=None):
return _convert_symbolic_model(intermediate, parametric=True) 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. Build a model in sparse representation from the explicit DRN representation.
:param String file: DRN file containing the model. :param String file: DRN file containing the model.
:param DirectEncodingParserOptions: Options for the parser.
:return: Model in sparse representation. :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) 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. Build a parametric model in sparse representation from the explicit DRN representation.
:param String file: DRN file containing the model. :param String file: DRN file containing the model.
:param DirectEncodingParserOptions: Options for the parser.
:return: Parametric model in sparse representation. :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) return _convert_sparse_model(intermediate, parametric=True)

10
src/core/core.cpp

@ -94,6 +94,11 @@ std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> buildSymbolic
} }
void define_build(py::module& m) { 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 // 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_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); 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_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_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_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") = ""); 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_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_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); .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) { void define_optimality_type(py::module& m) {

Loading…
Cancel
Save