From b649a5c96bdd1f37fbb5ea173fb87092b0a062d8 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 12 Jan 2017 23:05:28 +0100
Subject: [PATCH] build_model now takes a list of properties, unified the
 interface around building models

---
 lib/stormpy/__init__.py | 17 +++++++++++++----
 src/core/core.cpp       |  6 ++----
 2 files changed, 15 insertions(+), 8 deletions(-)

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<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"));
     
 }