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