diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index a92f28d1e..46ccaed61 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -114,4 +114,7 @@ void define_formulae(py::module& m) { py::class_>(m, "MultiObjectiveFormula", "Multi objective formula", formula) .def_property_readonly("subformulas", &storm::logic::MultiObjectiveFormula::getSubformulas, "Get vector of subformulas") .def_property_readonly("nr_subformulas", &storm::logic::MultiObjectiveFormula::getNumberOfSubformulas, "Get number of subformulas"); + + py::class_>(m, "GameFormula", "Game formula", unaryStateFormula) + .def_property_readonly("is_game_formula", &storm::logic::GameFormula::isGameFormula, "is it a game formula"); } diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 209f30e6a..bf9bfb5d8 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -71,3 +71,14 @@ def test_subformula(self): assert type(labelform) == stormpy.logic.AtomicLabelFormula prop = stormpy.core.Property("label-formula", labelform) assert prop.raw_formula == labelform + + def test_game_formula(self): + formula_str = "<<0>> Pmax=? [F \"goal\"]" + properties = stormpy.parse_properties(formula_str) + formula = properties[0].raw_formula + assert type(formula) == stormpy.logic.GameFormula + assert str(formula) == formula_str + assert len(properties) == 1 + formula = formula.subformula + assert type(formula) == stormpy.logic.ProbabilityOperator + assert str(formula) == "Pmax=? [F \"goal\"]"