diff --git a/lib/stormpy/logic/__init__.py b/lib/stormpy/logic/__init__.py index 9ab7620..8e27dc6 100644 --- a/lib/stormpy/logic/__init__.py +++ b/lib/stormpy/logic/__init__.py @@ -1,2 +1,13 @@ from . import logic from .logic import * + + +# this could be done in C++, but I don't know how to raise a Python error there +@property +def get_rational_threshold(self): + if not self._threshold_expression_has_rational_type: # wait, that's an expression, not formula?? + raise NotImplementedError("Can't get non-rational threshold (not implemented)") + else: + return self._threshold_as_rational + +OperatorFormula.threshold = get_rational_threshold diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 29c3f1a..07a39db 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -49,7 +49,10 @@ void define_formulae(py::module& m) { py::class_>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", unaryStateFormula); py::class_> operatorFormula(m, "OperatorFormula", "Operator formula",unaryStateFormula); operatorFormula.def_property_readonly("has_bound", &storm::logic::OperatorFormula::hasBound, "Flag if formula is bounded") - .def_property("threshold", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold of bound") + .def_property("_threshold_expression", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold expression") + .def_property_readonly("_threshold_as_rational", &storm::logic::OperatorFormula::getThresholdAs, "Rational threshold of bound, if applicable") + .def_property_readonly("_threshold_expression_has_rational_type", [](storm::logic::OperatorFormula const& f) { return f.getThreshold().hasRationalType(); } , "Check expression type [without needing a Python expression object]") + // property "threshold" defined in __init__ and is intended to be safe to use; the above two are for internal use .def_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType, "Comparison type of bound") ; py::class_>(m, "TimeOperator", "The time operator", operatorFormula); diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index f6b38d0..f4cd934 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -41,14 +41,15 @@ class TestFormulas: assert formula.threshold == pycarl.Rational("0.4") assert formula.comparison_type == stormpy.logic.ComparisonType.LESS - def test_set_bounds(self): - prop = "P<0.4 [F \"one\"]" - formula = stormpy.parse_properties(prop)[0].raw_formula - formula.threshold = pycarl.Rational("0.2") - formula.comparison_type = stormpy.logic.ComparisonType.GEQ - assert formula.threshold == pycarl.Rational("0.2") - assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ - assert str(formula) == "P>=1/5 [F \"one\"]" + # setter not currently implemented (non-trivial due to Expression container) + #def test_set_bounds(self): + # prop = "P<0.4 [F \"one\"]" + # formula = stormpy.parse_properties(prop)[0].raw_formula + # formula.threshold = pycarl.Rational("0.2") + # formula.comparison_type = stormpy.logic.ComparisonType.GEQ + # 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\"]"