Merge branch 'master' into develop

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}>")

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"));