diff --git a/src/core/pla.cpp b/src/core/pla.cpp index a679deb..f554cd8 100644 --- a/src/core/pla.cpp +++ b/src/core/pla.cpp @@ -8,32 +8,13 @@ typedef storm::storage::ParameterRegion Region; void specifyFormula(std::shared_ptr& checker, std::shared_ptr const& formula) { checker->specifyFormula(storm::modelchecker::CheckTask(*formula, true)); } -storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr& checker, Region& region) { - return checker->analyzeRegion(region, storm::modelchecker::parametric::RegionCheckResult::Unknown, true); +storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr& checker, Region& region, storm::modelchecker::parametric::RegionCheckResult initialResult, bool sampleVertices) { + return checker->analyzeRegion(region, initialResult, sampleVertices); } // Define python bindings void define_pla(py::module& m) { - // PLAChecker - py::class_>(m, "PLAChecker", "Region model checker for sparse DTMCs") - .def("__init__", [](PLAChecker& instance, std::shared_ptr> model) -> void { - new (&instance) PLAChecker(*model); - }) - //.def(py::init>) - .def("specify_formula", &specifyFormula, "Specify formula", py::arg("formula")) - .def("check_region", &checkRegion, "Check region", py::arg("region")) - ; - - // Region - py::class_>(m, "ParameterRegion", "Parameter region") - .def("__init__", [](Region &instance, std::string const& regionString, std::set const& variables) -> void { - new (&instance) Region(Region::parseRegion(regionString, variables)); - }) - //.def(py::init(), py::arg("lowerBounds"), py::arg("upperBounds")) - //.def("result", &Region::getCheckResult, "Get check result") - ; - // RegionCheckResult py::enum_(m, "RegionCheckResult", "Types of region check results") .value("EXISTSSAT", storm::modelchecker::parametric::RegionCheckResult::ExistsSat) @@ -46,4 +27,21 @@ void define_pla(py::module& m) { .value("UNKNOWN", storm::modelchecker::parametric::RegionCheckResult::Unknown) .def("__str__", &streamToString) ; + + // Region + py::class_>(m, "ParameterRegion", "Parameter region") + .def("__init__", [](Region &instance, std::string const& regionString, std::set const& variables) -> void { + new (&instance) Region(Region::parseRegion(regionString, variables)); + }) + //.def(py::init(), py::arg("lowerBounds"), py::arg("upperBounds")) + ; + + // PLAChecker + py::class_>(m, "PLAChecker", "Region model checker for sparse DTMCs") + .def("__init__", [](PLAChecker& instance, std::shared_ptr> model) -> void { + new (&instance) PLAChecker(*model); + }) + .def("specify_formula", &specifyFormula, "Specify formula", py::arg("formula")) + .def("check_region", &checkRegion, "Check region", py::arg("region"), py::arg("initialResult") = storm::modelchecker::parametric::RegionCheckResult::Unknown, py::arg("sampleVertices") = false) + ; } diff --git a/tests/core/test_pla.py b/tests/core/test_pla.py index 03fa2bb..be48f7a 100644 --- a/tests/core/test_pla.py +++ b/tests/core/test_pla.py @@ -35,7 +35,7 @@ class TestModelChecking: #upperBounds = {pL: 0.65, pK: 0.95} #region = stormpy.ParameterRegion(lowerBounds, upperBounds) region = stormpy.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters) - result = checker.check_region(region) + result = checker.check_region(region, stormpy.RegionCheckResult.UNKNOWN, True) assert result == stormpy.RegionCheckResult.EXISTSBOTH #lowerBounds = {pL: 0.1, pK: 0.2} #upperBounds = {pL: 0.73, pK: 0.715}