build_model now takes a list of properties, unified the interface around building models

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()

src/core/core.cpp

@@ -41,9 +41,7 @@ std::shared_ptr<storm::models::ModelBase> buildSparseModel(storm::prism::Program
 
 void define_build(py::module& m) {
     // Build model
-    m.def("_build_model", &buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formula"));
-    m.def("_build_parametric_model", &buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"));
-    m.def("build_model_from_prism_program", &storm::buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
-    m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
+    m.def("_build_sparse_model_from_prism_program", &storm::buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
+    m.def("_build_sparse_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
     
 }