From d62aac24b12816c52f8937b83e36cd398ec6a226 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Mon, 24 Aug 2020 21:48:53 -0700
Subject: [PATCH] model checking fully observable (due to auto downcasting,
 this needs a separate function

---
 src/core/modelchecking.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

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<storm::modelchecker::CheckResult> modelCheckingSparseEngine(std:
     return storm::api::verifyWithSparseEngine<ValueType>(env, model, task);
 }
 
+template<typename ValueType>
+std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingFullyObservableSparseEngine(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> model, CheckTask<ValueType> const& task, storm::Environment const& env) {
+    return storm::api::verifyWithSparseEngine<ValueType>(env, model->template as<storm::models::sparse::Mdp<ValueType>>(), task);
+}
+
 // Thin wrapper for model checking using dd engine
 template<storm::dd::DdType DdType, typename ValueType>
 std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model, CheckTask<ValueType> 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<double>, py::arg("model"), py::arg("task"), py::arg("environment")  = storm::Environment());
     m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine<double>, "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<storm::RationalFunction>, "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<storm::dd::DdType::Sylvan, double>, "Perform model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());