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 "$<$>:${PYBIND11_LTO_CXX_FLAGS}>") + #target_compile_options(${target_name} PRIVATE "$<$>:${PYBIND11_LTO_CXX_FLAGS}>") endif() if (PYBIND11_LTO_LINKER_FLAGS) target_link_libraries(${target_name} PRIVATE "$<$>:${PYBIND11_LTO_LINKER_FLAGS}>") 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_ptranalyzeRegion(region, hypothesis, initialResult, sampleVertices); } +storm::RationalFunction getBound(std::shared_ptr& checker, Region const& region, bool maximise) { + return checker->getBoundAtInitState(region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize); +} + + std::set gatherDerivatives(storm::models::sparse::Dtmc const& model, carl::Variable const& var) { std::set derivatives; for (auto it : model.getTransitionMatrix()) { @@ -70,6 +75,7 @@ void define_pla(py::module& m) { new (&instance) std::unique_ptr(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"));