From ad65f009ad81edb2575d17aeebfbf2bdc545edb1 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 13 Dec 2016 18:05:43 +0100
Subject: [PATCH] Build from prism program has default formulas = []

---
 src/core/core.cpp           | 2 +-
 tests/storage/test_model.py | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/core/core.cpp b/src/core/core.cpp
index 98d74dc..99d01d2 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -43,7 +43,7 @@ void define_build(py::module& m) {
     // Build model
     m.def("_build_model", &buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false);
     m.def("_build_parametric_model", &buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false);
-    m.def("build_model_from_prism_program", &storm::buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false);
+    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>>(), py::arg("onlyInitialRelevant") = false);
     m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false);
     
 }
diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py
index 44a4c9c..5c32826 100644
--- a/tests/storage/test_model.py
+++ b/tests/storage/test_model.py
@@ -4,6 +4,15 @@ from helpers.helper import get_example_path
 
 class TestModel:
     def test_build_dtmc_from_prism_program(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
+        model = stormpy.build_model_from_prism_program(program)
+        assert model.nr_states == 13
+        assert model.nr_transitions == 20
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert not model.supports_parameters
+        assert type(model) is stormpy.SparseDtmc
+ 
+    def test_build_dtmc_from_prism_program_formulas(self):
         program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
         prop = "P=? [F \"one\"]"
         formulas = stormpy.parse_formulas_for_prism_program(prop, program)