extended pla bindings for latest additions in PLA and to build PLA checker directly

src/pars/pla.cpp

@@ -3,23 +3,36 @@
 #include "storm/api/storm.h"
 
 
-typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> SparseDtmcRegionChecker;
+typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> DtmcParameterLiftingModelChecker;
+typedef storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double> MdpParameterLiftingModelChecker;
+
 typedef storm::modelchecker::RegionModelChecker<storm::RationalFunction> RegionModelChecker;
 typedef storm::storage::ParameterRegion<storm::RationalFunction> Region;
 
 // Thin wrappers
-std::shared_ptr<RegionModelChecker> createRegionChecker(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const& model, std::shared_ptr<storm::logic::Formula> const& formula) {
-    return storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(env, model, storm::api::createTask<storm::RationalFunction>(formula, true));
+std::shared_ptr<RegionModelChecker> createRegionChecker(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const& model, std::shared_ptr<storm::logic::Formula> const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) {
+    return storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(env, model, storm::api::createTask<storm::RationalFunction>(formula, true), generateSplittingEstimate, allowModelSimplifications);
+}
+
+void specify(std::shared_ptr<RegionModelChecker>& checker, storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const& model, std::shared_ptr<storm::logic::Formula> const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) {
+    return checker->specify(env, model, storm::api::createTask<storm::RationalFunction>(formula, true), generateSplittingEstimate, allowModelSimplifications);
 }
 
 storm::modelchecker::RegionResult checkRegion(std::shared_ptr<RegionModelChecker>& checker, storm::Environment const& env, Region const& region, storm::modelchecker::RegionResultHypothesis const& hypothesis, storm::modelchecker::RegionResult const& initialResult, bool sampleVertices) {
     return checker->analyzeRegion(env, region, hypothesis, initialResult, sampleVertices);
 }
 
-storm::RationalFunction getBound(std::shared_ptr<RegionModelChecker>& checker, storm::Environment const& env, Region const& region, bool maximise) {
+storm::RationalFunction getBoundAtInit(std::shared_ptr<RegionModelChecker>& checker, storm::Environment const& env, Region const& region, bool maximise) {
     return checker->getBoundAtInitState(env, region, maximise ?  storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize);
 }
 
+storm::modelchecker::ExplicitQuantitativeCheckResult<double> getBound_dtmc(std::shared_ptr<DtmcParameterLiftingModelChecker>& checker, storm::Environment const& env, Region const& region, bool maximise) {
+    return res = checker->getBound(env, region, maximise ?  storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult<double>();
+}
+
+std::unique_ptr<storm::modelchecker::QuantitativeCheckResult<double>> getBound_mdp(std::shared_ptr<MdpParameterLiftingModelChecker>& checker, storm::Environment const& env, Region const& region, bool maximise) {
+    return checker->getBound(env, region, maximise ?  storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult<double>();
+}
 
 std::set<storm::Polynomial> gatherDerivatives(storm::models::sparse::Model<storm::RationalFunction> const& model, carl::Variable const& var) {
     std::set<storm::Polynomial> derivatives;
@@ -66,20 +79,22 @@ void define_pla(py::module& m) {
     ;
 
     // RegionModelChecker
-    //py::class_<SparseDtmcRegionChecker, std::shared_ptr<SparseDtmcRegionChecker>>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs")
-    py::class_<RegionModelChecker, std::shared_ptr<RegionModelChecker>>(m, "RegionModelChecker", "Region model checker via paramater lifting")
-/*        .def("__init__", [](std::unique_ptr<SparseDtmcRegionChecker>& instance, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> const& task) -> void {
-                // Better use storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, task);
-                //SparseDtmcRegionChecker tmp;
-                //tmp.specify(model, task);
-                auto tmp = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, task);
-                new (&instance) std::unique_ptr<SparseDtmcRegionChecker>(tmp);
-            }, py::arg("model"), py::arg("task")*/
-        .def("check_region", &checkRegion, "Check region", py::arg("environment"), 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("environment"), py::arg("region"), py::arg("maximise")= true);
+
+    py::class_<RegionModelChecker, std::shared_ptr<RegionModelChecker>> regionModelChecker(m, "RegionModelChecker", "Region model checker via paramater lifting");
+    regionModelChecker.def("check_region", &checkRegion, "Check region", py::arg("environment"), py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false)
+        .def("get_bound", &getBoundAtInit, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true)
+        .def("specify", &specify, "specify arguments",py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true);
     ;
 
-    m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula"));
+
+    py::class_<DtmcParameterLiftingModelChecker, std::shared_ptr<DtmcParameterLiftingModelChecker>>(m, "DtmcParameterLiftingModelChecker", "Region model checker for DTMCs", regionModelChecker)
+            .def(py::init<>())
+            .def("get_bound_all_states", &getBound_dtmc, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true);
+    py::class_<MdpParameterLiftingModelChecker, std::shared_ptr<MdpParameterLiftingModelChecker>>(m, "MdpParameterLiftingModelChecker", "Region model checker for MPDs", regionModelChecker)
+            .def(py::init<>())
+            .def("get_bound_all_states", &getBound_mdp, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true);
+
+    m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true);
     //m.def("is_parameter_lifting_sound", &storm::utility::parameterlifting::validateParameterLiftingSound, "Check if parameter lifting is sound", py::arg("model"), py::arg("formula"));
     m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var"));
 }