diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index e2348ce..f0c24d1 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -14,6 +14,11 @@ std::shared_ptr modelCheckingSparseEngine(std: return storm::api::verifyWithSparseEngine(env, model, task); } +template +std::shared_ptr modelCheckingFullyObservableSparseEngine(std::shared_ptr> model, CheckTask const& task, storm::Environment const& env) { + return storm::api::verifyWithSparseEngine(env, model->template as>(), task); +} + // Thin wrapper for model checking using dd engine template std::shared_ptr modelCheckingDdEngine(std::shared_ptr> model, CheckTask const& task, storm::Environment const& env) { @@ -68,6 +73,7 @@ void define_modelchecking(py::module& m) { ; // Model checking + m.def("model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());