diff --git a/src/core/core.cpp b/src/core/core.cpp index 332aac5..4f9d672 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -11,8 +11,8 @@ void define_core(py::module& m) { void define_parse(py::module& m) { // Parse formulas - m.def("parse_formulas", &storm::parseFormulasForExplicit, "Parse explicit formulas", py::arg("formula_string")); - m.def("parse_formulas_for_prism_program", &storm::parseFormulasForPrismProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program")); + m.def("parse_properties", &storm::parsePropertiesForExplicit, "Parse explicit formulas", py::arg("formula_string"), py::arg("property_filter") = nullptr); + 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") = nullptr); // Pair py::class_(m, "ModelFormulasPair", "Pair of model and formulas") diff --git a/src/core/input.cpp b/src/core/input.cpp index 8c9f915..d83ee93 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -1,5 +1,12 @@ #include "input.h" +void define_property(py::module& m) { + py::class_(m, "Property", "Property") + .def_property_readonly("name", &storm::jani::Property::getName, "Obtain the name of the property") + .def_property_readonly("raw_formula", &storm::jani::Property::getRawFormula, "Obtain the formula directly"); +} + + // Define python bindings void define_input(py::module& m) { diff --git a/src/core/input.h b/src/core/input.h index 304dc9a..636b73a 100644 --- a/src/core/input.h +++ b/src/core/input.h @@ -3,6 +3,8 @@ #include "common.h" +void define_property(py::module& m); void define_input(py::module& m); + #endif /* PYTHON_CORE_INPUT_H_ */ diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 791b6f4..79cd114 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -94,7 +94,7 @@ void define_model_instantiator(py::module& m) { .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>::instantiate, "Instantiate model with given parameter values"); - py::class_,storm::models::sparse::Mdp>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to MDPs") + py::class_,storm::models::sparse::Mdp>>(m, "MdpInstantiator", "Instantiate PDTMCs to MDPs") .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Mdp>::instantiate, "Instantiate model with given parameter values"); -} \ No newline at end of file +}