From 8db0759f58e13d470a2397a7e14bf8f1e0ddec23 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sat, 27 Jan 2018 19:15:24 +0100
Subject: [PATCH] optimality type for formulae

---
 src/core/core.cpp      | 8 ++++++++
 src/core/core.h        | 1 +
 src/logic/formulae.cpp | 6 ++----
 src/mod_core.cpp       | 1 +
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/core/core.cpp b/src/core/core.cpp
index d5f03be..b4b5de6 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -2,6 +2,7 @@
 #include "storm/utility/initialize.h"
 #include "storm/utility/DirectEncodingExporter.h"
 #include "storm/storage/ModelFormulasPair.h"
+#include "storm/solver/OptimizationDirection.h"
 
 void define_core(py::module& m) {
     // Init
@@ -68,6 +69,13 @@ void define_build(py::module& m) {
 
 }
 
+void define_optimality_type(py::module& m) {
+    py::enum_<storm::solver::OptimizationDirection>(m, "OptimizationDirection")
+            .value("Minimize", storm::solver::OptimizationDirection::Minimize)
+            .value("Maximize", storm::solver::OptimizationDirection::Maximize)
+            ;
+}
+
 // Thin wrapper for exporting model
 template<typename ValueType>
 void exportDRN(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& file) {
diff --git a/src/core/core.h b/src/core/core.h
index b56aa28..51bc696 100644
--- a/src/core/core.h
+++ b/src/core/core.h
@@ -7,5 +7,6 @@ void define_core(py::module& m);
 void define_parse(py::module& m);
 void define_build(py::module& m);
 void define_export(py::module& m);
+void define_optimality_type(py::module& m);
 
 #endif /* PYTHON_CORE_CORE_H_ */
diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp
index e36a28a..d6d2dd8 100644
--- a/src/logic/formulae.cpp
+++ b/src/logic/formulae.cpp
@@ -58,10 +58,8 @@ void define_formulae(py::module& m) {
         .def("set_bound", [](storm::logic::OperatorFormula& f, storm::logic::ComparisonType comparisonType, storm::expressions::Expression const& bound) {
             f.setBound(storm::logic::Bound(comparisonType, bound));
         }, "Set bound", py::arg("comparison_type"), py::arg("bound"))
-        // 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]")
+        .def_property_readonly("has_optimality_type",  &storm::logic::OperatorFormula::hasOptimalityType, "Flag if an optimality type is present")
+        .def_property_readonly("optimality_type", &storm::logic::OperatorFormula::getOptimalityType, "Flag for the optimality type")
     ;
     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);
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 583eff6..615a7ef 100644
--- a/src/mod_core.cpp
+++ b/src/mod_core.cpp
@@ -20,6 +20,7 @@ PYBIND11_MODULE(core, m) {
     define_property(m);
     define_parse(m);
     define_build(m);
+    define_optimality_type(m);
     define_export(m);
     define_result(m);
     define_modelchecking(m);