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_(m, "OptimizationDirection") + .value("Minimize", storm::solver::OptimizationDirection::Minimize) + .value("Maximize", storm::solver::OptimizationDirection::Maximize) + ; +} + // Thin wrapper for exporting model template void exportDRN(std::shared_ptr> 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, "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_>(m, "TimeOperator", "The time operator", operatorFormula); py::class_>(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);