diff --git a/src/core/pla.cpp b/src/core/pla.cpp index 641aa9c..5506f71 100644 --- a/src/core/pla.cpp +++ b/src/core/pla.cpp @@ -1,14 +1,14 @@ #include "pla.h" #include "src/helpers.h" -typedef storm::modelchecker::parametric::SparseDtmcParameterLifting, double> PLAChecker; +typedef storm::modelchecker::parametric::SparseDtmcRegionChecker, double, storm::RationalNumber> SparseDtmcRegionChecker; typedef storm::storage::ParameterRegion Region; // Thin wrappers -void specifyFormula(std::shared_ptr& checker, std::shared_ptr const& formula) { +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, storm::modelchecker::parametric::RegionCheckResult initialResult, bool sampleVertices) { +storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr& checker, Region& region, storm::modelchecker::parametric::RegionCheckResult initialResult, bool sampleVertices) { return checker->analyzeRegion(region, initialResult, sampleVertices); } @@ -47,10 +47,10 @@ void define_pla(py::module& m) { //.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); + // RegionChecker + py::class_>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs") + .def("__init__", [](SparseDtmcRegionChecker& instance, std::shared_ptr> model) -> void { + new (&instance) SparseDtmcRegionChecker(*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 4537d40..0301692 100644 --- a/tests/core/test_pla.py +++ b/tests/core/test_pla.py @@ -13,33 +13,16 @@ class TestModelChecking: assert model.nr_transitions == 803 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters - checker = stormpy.PLAChecker(model) + checker = stormpy.SparseDtmcRegionChecker(model) checker.specify_formula(formulas[0].raw_formula) parameters = model.collect_probability_parameters() assert len(parameters) == 2 - #if str(parameters[0]) == "pL": - # pL = parameters[0] - # pK = parameters[1] - #else: - # pK = parameters[0] - # pL = parameters[1] - #assert str(pL) == "pL" - #assert str(pK) == "pK" - #lowerBounds = {pL: 0.7, pK: 0.75} - #upperBounds = {pL: 0.9, pK: 0.95} - #region = stormpy.ParameterRegion(lowerBounds, upperBounds) region = stormpy.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) result = checker.check_region(region) assert result == stormpy.RegionCheckResult.ALLSAT - #lowerBounds = {pL: 0.4, pK: 0.75} - #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, stormpy.RegionCheckResult.UNKNOWN, True) assert result == stormpy.RegionCheckResult.EXISTSBOTH - #lowerBounds = {pL: 0.1, pK: 0.2} - #upperBounds = {pL: 0.73, pK: 0.715} - #region = stormpy.ParameterRegion(lowerBounds, upperBounds) region = stormpy.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters) result = checker.check_region(region) assert result == stormpy.RegionCheckResult.ALLVIOLATED