diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 9098233..a594a56 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -6,8 +6,13 @@ from .version import __version__ core._set_up("") -def build_model(program, formulae): - intermediate = core._build_model(program, formulae) + +def build_model(program, properties = None): + if properties: + formulae = [prop.raw_formula for prop in properties] + else: + formulae = [] + intermediate = core._build_sparse_model_from_prism_program(program, formulae) assert not intermediate.supports_parameters if intermediate.model_type == ModelType.DTMC: return intermediate._as_dtmc() @@ -16,8 +21,12 @@ def build_model(program, formulae): else: raise RuntimeError("Not supported non-parametric model constructed") -def build_parametric_model(program, formulae): - intermediate = core._build_parametric_model(program, formulae) +def build_parametric_model(program, properties = None): + if properties: + formulae = [prop.raw_formula for prop in properties] + else: + formulae = [] + intermediate = core._build_sparse_parametric_model_from_prism_program(program, formulae) assert intermediate.supports_parameters if intermediate.model_type == ModelType.DTMC: return intermediate._as_pdtmc() diff --git a/src/core/core.cpp b/src/core/core.cpp index cd3ed7e..6d4090d 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -41,9 +41,7 @@ std::shared_ptr buildSparseModel(storm::prism::Program void define_build(py::module& m) { // Build model - m.def("_build_model", &buildSparseModel, "Build the model", py::arg("program"), py::arg("formula")); - m.def("_build_parametric_model", &buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formula")); - m.def("build_model_from_prism_program", &storm::buildSparseModel, "Build the model", py::arg("program"), py::arg("formulas") = std::vector>()); - m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); + m.def("_build_sparse_model_from_prism_program", &storm::buildSparseModel, "Build the model", py::arg("program"), py::arg("formulas") = std::vector>()); + m.def("_build_sparse_parametric_model_from_prism_program", &storm::buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); }