property constructor from formula

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

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