support for partially observable models, and better model-dependent creation

lib/stormpy/__init__.py

@@ -256,7 +256,7 @@ def perform_symbolic_bisimulation(model, properties):
         return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type)
 
 
-def model_checking(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()):
+def model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()):
     """
     Perform model checking on model for property.
     :param model: Model.
@@ -268,7 +268,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler
     """
     if model.is_sparse_model:
         return check_model_sparse(model, property, only_initial_states=only_initial_states,
-                                  extract_scheduler=extract_scheduler, environment=environment)
+                                  extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment)
     else:
         assert (model.is_symbolic_model)
         if extract_scheduler:
@@ -277,13 +277,14 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler
                               environment=environment)
 
 
-def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()):
+def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()):
     """
     Perform model checking on model for property.
     :param model: Model.
     :param property: Property to check for.
     :param only_initial_states: If True, only results for initial states are computed, otherwise for all states.
     :param extract_scheduler: If True, try to extract a scheduler
+    :param force_fully_observable: If True, treat a POMDP as an MDP
     :return: Model checking result.
     :rtype: CheckResult
     """
@@ -292,6 +293,22 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched
     else:
         formula = property
 
+    if force_fully_observable:
+        if model.is_partially_observable:
+            # Note that casting a model to a fully observable model wont work with python/pybind, so we actually have other access points
+            if model.supports_parameters:
+                raise NotImplementedError("")
+            elif model.is_exact:
+                task = core.ExactCheckTask(formula, only_initial_states)
+                task.set_produce_schedulers(extract_scheduler)
+                return core._exact_model_checking_fully_observable(model, task, environment=environment)
+            else:
+                task = core.CheckTask(formula, only_initial_states)
+                task.set_produce_schedulers(extract_scheduler)
+                return core._model_checking_fully_observable(model, task, environment=environment)
+        else:
+            raise RuntimeError("Forcing models that are fully observable is not possible")
+
     if model.supports_parameters:
         task = core.ParametricCheckTask(formula, only_initial_states)
         task.set_produce_schedulers(extract_scheduler)

lib/stormpy/pomdp/__init__.py

@@ -42,4 +42,30 @@ def apply_unknown_fsc(model, mode):
     if model.supports_parameters:
         return pomdp._apply_unknown_fsc_Rf(model, mode)
     else:
-        return pomdp._apply_unknown_fsc_Double(model, mode)
+        return pomdp._apply_unknown_fsc_Double(model, mode)
+
+
+def create_nondeterminstic_belief_tracker(model):
+    """
+
+    :param model: A POMDP
+    :return:
+    """
+    if model.is_exact:
+        return pomdp.NondeterministicBeliefTrackerExactSparse(model)
+    else:
+        return pomdp.NondeterministicBeliefTrackerDoubleSparse(model)
+
+
+def create_observation_trace_unfolder(model, risk_assessment, expr_manager):
+    """
+
+    :param model:
+    :param risk_assessment:
+    :param expr_manager:
+    :return:
+    """
+    if model.is_exact:
+        return pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager)
+    else:
+        return pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager)

src/storage/model.cpp

@@ -108,6 +108,7 @@ void define_model(py::module& m) {
         .def_property_readonly("supports_parameters", &ModelBase::supportsParameters, "Flag whether model supports parameters")
         .def_property_readonly("has_parameters", &ModelBase::hasParameters, "Flag whether model has parameters")
         .def_property_readonly("is_exact", &ModelBase::isExact, "Flag whether model is exact")
+        .def_property_readonly("is_partially_observable", &ModelBase::isPartiallyObservable, "Flag whether the model has observation labels")
         .def_property_readonly("is_sparse_model", &ModelBase::isSparseModel, "Flag whether the model is stored as a sparse model")
         .def_property_readonly("is_symbolic_model", &ModelBase::isSymbolicModel, "Flag whether the model is stored using decision diagrams")
         .def_property_readonly("is_discrete_time_model", &ModelBase::isDiscreteTimeModel, "Flag whether the model is a discrete time model")