From 76d22b1afc551c1b78aa76d7cf32ee72bc587922 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 20 Oct 2017 14:17:51 +0200
Subject: [PATCH 1/2] Disabled LTO to avoid segfaults

---
 resources/pybind11/tools/pybind11Tools.cmake | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/resources/pybind11/tools/pybind11Tools.cmake b/resources/pybind11/tools/pybind11Tools.cmake
index 8726ce9..f8d7faf 100755
--- a/resources/pybind11/tools/pybind11Tools.cmake
+++ b/resources/pybind11/tools/pybind11Tools.cmake
@@ -101,7 +101,7 @@ function(_pybind11_add_lto_flags target_name prefer_thin_lto)
 
   # Enable LTO flags if found, except for Debug builds
   if (PYBIND11_LTO_CXX_FLAGS)
-    target_compile_options(${target_name} PRIVATE "$<$<NOT:$<CONFIG:Debug>>:${PYBIND11_LTO_CXX_FLAGS}>")
+    #target_compile_options(${target_name} PRIVATE "$<$<NOT:$<CONFIG:Debug>>:${PYBIND11_LTO_CXX_FLAGS}>")
   endif()
   if (PYBIND11_LTO_LINKER_FLAGS)
     target_link_libraries(${target_name} PRIVATE "$<$<NOT:$<CONFIG:Debug>>:${PYBIND11_LTO_LINKER_FLAGS}>")

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 2/2] 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"));