diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp index 6040230..e13c0a7 100644 --- a/src/pars/model_instantiator.cpp +++ b/src/pars/model_instantiator.cpp @@ -51,14 +51,24 @@ void define_model_instantiator(py::module& m) { void define_model_instantiation_checker(py::module& m) { - py::class_, double>, std::shared_ptr, double>>> bpdtmcinstchecker(m, "PDtmcInstantiationCheckerBase", "Instantiate pDTMCs to DTMCs (base)"); + py::class_, double>, std::shared_ptr, double>>> bpdtmcinstchecker(m, "_PDtmcInstantiationCheckerBase", "Instantiate pDTMCs to DTMCs and immediately check (base)"); bpdtmcinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a) ; - py::class_, double>, std::shared_ptr, double>>> (m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs", bpdtmcinstchecker) + py::class_, double>, std::shared_ptr, double>>> (m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs and immediately check", bpdtmcinstchecker) .def(py::init>(), "parametric model"_a) .def("check", [](SparseDtmcInstantiationModelChecker, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a); + + + py::class_, double>, std::shared_ptr, double>>> bpmdpinstchecker(m, "_PMdpInstantiationCheckerBase", "Instantiate pMDPs to MDPs and immediately check (base)"); + bpmdpinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a) + ; + py::class_, double>, std::shared_ptr, double>>> (m, "PMdpInstantiationChecker", "Instantiate PMDP to MDPs and immediately check", bpmdpinstchecker) + + .def(py::init>(), "parametric model"_a) + .def("check", [](SparseMdpInstantiationModelChecker, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) + .def("set_graph_preserving", &SparseMdpInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a); ; } \ No newline at end of file