From fee6da4d30ebbf7e5555580e89fac67a53126eb0 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 23 Oct 2017 12:34:48 +0200
Subject: [PATCH] Get PLA bounds

---
 src/pars/pla.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp
index e2fe24e..3680242 100644
--- a/src/pars/pla.cpp
+++ b/src/pars/pla.cpp
@@ -15,6 +15,11 @@ storm::modelchecker::RegionResult checkRegion(std::shared_ptr<RegionModelChecker
     return checker->analyzeRegion(region, hypothesis, initialResult, sampleVertices);
 }
 
+storm::RationalFunction getBound(std::shared_ptr<RegionModelChecker>& checker, Region const& region, bool maximise) {
+    return checker->getBoundAtInitState(region, maximise ?  storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize);
+}
+
+
 std::set<storm::Polynomial> gatherDerivatives(storm::models::sparse::Dtmc<storm::RationalFunction> const& model, carl::Variable const& var) {
     std::set<storm::Polynomial> derivatives;
     for (auto it : model.getTransitionMatrix()) {
@@ -70,6 +75,7 @@ void define_pla(py::module& m) {
                 new (&instance) std::unique_ptr<SparseDtmcRegionChecker>(tmp);
             }, py::arg("model"), py::arg("task")*/
         .def("check_region", &checkRegion, "Check region", py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false)
+        .def("get_bound", &getBound, "Get bound", py::arg("region"), py::arg("maximise")= true);
     ;
 
     m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("model"), py::arg("formula"));