From bef0a792d6e4a2cac12d933e7543a4be169ff7c7 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 21 Aug 2018 10:13:21 +0200
Subject: [PATCH] add init for probability operator

---
 src/logic/formulae.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp
index 90dc80b..31d1e31 100644
--- a/src/logic/formulae.cpp
+++ b/src/logic/formulae.cpp
@@ -80,7 +80,9 @@ void define_formulae(py::module& m) {
     ;
     py::class_<storm::logic::TimeOperatorFormula, std::shared_ptr<storm::logic::TimeOperatorFormula>>(m, "TimeOperator", "The time operator", operatorFormula);
     py::class_<storm::logic::LongRunAverageOperatorFormula, std::shared_ptr<storm::logic::LongRunAverageOperatorFormula>>(m, "LongRunAvarageOperator", "Long run average operator", operatorFormula);
-    py::class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula>>(m, "ProbabilityOperator", "Probability operator", operatorFormula);
+    py::class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula>>(m, "ProbabilityOperator", "Probability operator", operatorFormula)
+            .def(py::init<std::shared_ptr<storm::logic::Formula>>(), "construct probability operator formula", py::arg("subformula"))
+    ;
     py::class_<storm::logic::RewardOperatorFormula, std::shared_ptr<storm::logic::RewardOperatorFormula>>(m, "RewardOperator", "Reward operator", operatorFormula)
             .def("has_reward_name", &storm::logic::RewardOperatorFormula::hasRewardModelName)
             .def_property_readonly("reward_name", &storm::logic::RewardOperatorFormula::getRewardModelName);