add init for probability operator

6 years ago · bef0a792d6
1 changed files with 3 additions and 1 deletions
--- 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);