From 116245ecbb8fe05044768482a8d2901956d8f714 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 18 Jan 2017 18:21:26 +0100
Subject: [PATCH] property constructor from formula

---
 src/core/input.cpp           |  1 +
 tests/logic/test_formulas.py | 11 +++++++++++
 2 files changed, 12 insertions(+)

diff --git a/src/core/input.cpp b/src/core/input.cpp
index d83ee93..ae986f5 100644
--- a/src/core/input.cpp
+++ b/src/core/input.cpp
@@ -2,6 +2,7 @@
 
 void define_property(py::module& m) {
     py::class_<storm::jani::Property>(m, "Property", "Property")
+    .def(py::init<std::string const&, std::shared_ptr<storm::logic::Formula const> const&, std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("comment") = "")
     .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");
 }
diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py
index ab074d2..dfdc273 100644
--- a/tests/logic/test_formulas.py
+++ b/tests/logic/test_formulas.py
@@ -49,3 +49,14 @@ class TestFormulas:
         assert formula.threshold == pycarl.Rational("0.2")
         assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ
         assert str(formula) == "P>=1/5 [F \"one\"]"
+
+    def test_subformula(self):
+        prop = "P=? [F \"one\"]"
+        formula = stormpy.parse_properties(prop)[0].raw_formula
+        assert type(formula) == stormpy.logic.ProbabilityOperator
+        pathform = formula.subformula
+        assert type(pathform) == stormpy.logic.EventuallyFormula
+        labelform = pathform.subformula
+        assert type(labelform) == stormpy.logic.AtomicLabelFormula
+        prop = stormpy.core.Property("label-formula", labelform)
+        assert prop.raw_formula == labelform