Fixed PLA bindings after updates

src/core/pla.cpp

@@ -1,14 +1,14 @@
 #include "pla.h"
 #include "src/helpers.h"
 
-typedef storm::modelchecker::parametric::SparseDtmcParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> PLAChecker;
+typedef storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> SparseDtmcRegionChecker;
 typedef storm::storage::ParameterRegion<storm::RationalFunction> Region;
 
 // Thin wrappers
-void specifyFormula(std::shared_ptr<PLAChecker>& checker, std::shared_ptr<const storm::logic::Formula> const& formula) {
+void specifyFormula(std::shared_ptr<SparseDtmcRegionChecker>& checker, std::shared_ptr<const storm::logic::Formula> const& formula) {
     checker->specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formula, true));
 }
-storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr<PLAChecker>& checker, Region& region, storm::modelchecker::parametric::RegionCheckResult initialResult, bool sampleVertices) {
+storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr<SparseDtmcRegionChecker>& 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<Region::VariableSubstitutionType &, Region::VariableSubstitutionType &>(), py::arg("lowerBounds"), py::arg("upperBounds"))
     ;
 
-    // PLAChecker
-    py::class_<PLAChecker, std::shared_ptr<PLAChecker>>(m, "PLAChecker", "Region model checker for sparse DTMCs")
-        .def("__init__", [](PLAChecker& instance, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model) -> void {
-                new (&instance) PLAChecker(*model);
+    // RegionChecker
+    py::class_<SparseDtmcRegionChecker, std::shared_ptr<SparseDtmcRegionChecker>>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs")
+        .def("__init__", [](SparseDtmcRegionChecker& instance, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> 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)

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