diff --git a/doc/source/code_stormpy_core.rst b/doc/source/code_stormpy_core.rst index 4dfd7af..77329a0 100644 --- a/doc/source/code_stormpy_core.rst +++ b/doc/source/code_stormpy_core.rst @@ -2,11 +2,13 @@ Stormpy.core ************************** .. automodule:: stormpy - + :members: + :undoc-members: Core members ========================= .. automodule:: stormpy.core - :members: \ No newline at end of file + :members: + :undoc-members: diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index b3907dd..3749e51 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -8,6 +8,12 @@ core._set_up("") def build_model(program, properties = None): + """ + Build a model from a symbolic description + + :param PrismProgram program: Prism program to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + """ if properties: formulae = [prop.raw_formula for prop in properties] else: @@ -22,6 +28,11 @@ def build_model(program, properties = None): raise RuntimeError("Not supported non-parametric model constructed") def build_parametric_model(program, properties = None): + """ + + :param PrismProgram program: Prism program with open constants to translate into a parametric model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + """ if properties: formulae = [prop.raw_formula for prop in properties] else: @@ -49,6 +60,13 @@ def model_checking(model, property): def compute_prob01_states(model, phi_states, psi_states): + """ + Compute prob01 states for properties of the form phi_states until psi_states + + :param SparseDTMC model: + :param BitVector phi_states: + :param BitVector psi_states: + """ if model.model_type != ModelType.DTMC: raise ValueError("Prob 01 is only defined for DTMCs -- model must be a DTMC") diff --git a/src/core/core.cpp b/src/core/core.cpp index 40933f4..a191403 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -11,8 +11,22 @@ void define_core(py::module& m) { void define_parse(py::module& m) { // Parse formulas - m.def("parse_properties", &storm::parsePropertiesForExplicit, "Parse explicit formulas", py::arg("formula_string"), py::arg("property_filter") = boost::none); - m.def("parse_properties_for_prism_program", &storm::parsePropertiesForPrismProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program"), py::arg("property_filter") = boost::none); + m.def("parse_properties", &storm::parsePropertiesForExplicit, R"dox( + + Parse properties given in the prism format. + + :param str formula_str: A string of formulas + :param str property_filter: A filter + )dox", py::arg("formula_string"), py::arg("property_filter") = boost::none); + m.def("parse_properties_for_prism_program", &storm::parsePropertiesForPrismProgram, R"dox( + + Parses properties given in the prism format, allows references to variables in the prism program. + + :param str formula_str: A string of formulas + :param PrismProgram prism_program: A prism program + :param str property_filter: A filter + :return: A list of properties + )dox", py::arg("formula_string"), py::arg("prism_program"), py::arg("property_filter") = boost::none); // Pair py::class_(m, "ModelFormulasPair", "Pair of model and formulas")