From 86d5ddd8fd750cf6609664ae193cdcbe31b1172a Mon Sep 17 00:00:00 2001
From: Tom Janson <tom.janson@rwth-aachen.de>
Date: Wed, 5 Apr 2017 19:28:43 +0200
Subject: [PATCH] unwrap threshold expressions (2nd Ed.)

simply in C++ this time (I dislike monkey wrenching the Python class in
__init__ -- things are confusing enough already)
---
 lib/stormpy/logic/__init__.py | 11 -----------
 src/logic/formulae.cpp        | 15 +++++++++++----
 2 files changed, 11 insertions(+), 15 deletions(-)

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_<storm::logic::UnaryBooleanStateFormula, std::shared_ptr<storm::logic::UnaryBooleanStateFormula>>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", unaryStateFormula);
     py::class_<storm::logic::OperatorFormula, std::shared_ptr<storm::logic::OperatorFormula>> 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<storm::RationalNumber>, "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<storm::RationalNumber>();
+            }
+        }, "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<storm::RationalNumber>, "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_<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);