diff --git a/lib/stormpy/logic/__init__.py b/lib/stormpy/logic/__init__.py index 8e27dc6..9ab7620 100644 --- a/lib/stormpy/logic/__init__.py +++ b/lib/stormpy/logic/__init__.py @@ -1,13 +1,2 @@ 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 07a39db..25324be 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -49,11 +49,18 @@ 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_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") + .def_property_readonly("threshold", [](storm::logic::OperatorFormula const& f) { + if (!f.getThreshold().hasRationalType()) { + throw std::runtime_error("Can't get non-rational threshold (not implemented)"); + } else { + return f.getThresholdAs(); + } + }, "Threshold of bound (currently only applicable to rational expressions)") + // the above method should be sufficient for now; reinstate the following if needed + //.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]") ; py::class_>(m, "TimeOperator", "The time operator", operatorFormula); py::class_>(m, "LongRunAvarageOperator", "Long run average operator", operatorFormula);